Skip to content

Details

Save the date for SecTalks 10th Year Anniversary Summit. 11 Nov 2023.

# Presentation: seL4: Provable Security for the Real World

The seL4 microkernel, developed by the Trustworthy Systems group at UNSW Sydney, is the world’s first operating system (OS) kernel with a formal, machine-checked proof of implementation correctness. This strong properties allows reasoning about security properties at the level of the mathematical model of the kernel, and was used to prove that seL4 can enforce the “CIA triad” of confidentiality, integrity and availability. While some such proof artefacts now exist for other kernels, seL4 still has the most comprehensive verification story, which applies across three processor architectures, and is still the only verified kernel with fine-grained access control based on object capabilities. seL4 and all its proofs are open-source, available on GitHub under the GPLv2 license. There is a growing open-source ecosystem backed by the neutral and open seL4 Foundation.

by Prof. Gernot Heiser

Gernot Heiser is Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney and Chief Research Scientist at CSIRO’s Data61. His research interest are in operating systems, real-time systems, security and safety. He is the founder and past leader of Data61’s Trustworthy Systems group, which pioneered large-scale formal verification of systems code, specifically the design, implementation and formal verification of the seL4 microkernel; seL4 is now being used in real-world security- and safety-critical systems. Heiser's former company Open Kernel Labs, acquired by General Dynamics in 2012, marketed the OKL4 microkernel, which shipped on billions of mobile wireless chips and more recently ships on the secure enclave of all iOS devices. He presently serves as Chief Scientist, Software, of HENSOLDT Cyber, a Munich-based company providing a secure hardware-software stack for embedded and cyber-physical systems. Gernot is a Fellow of the ACM, the IEEE and the Australian Academy of Technology and Engineering (ATSE) and an ACM Distinguished Lecturer

# Sponsors

# Notes

Events in Barangaroo
Cloud Security
Cybersecurity
Network Security
Penetration Testing
Web Security

Members are also interested in