Skip to content

Details

# Presentation: The seL4 microkernel: Mathematical proof of security

The seL4 microkernel was the world’s first operating system (OS) kernel with a formal, machine-checked proof of implementation correctness. It is still the only capability-based kernel with such a proof, and meanwhile has further proofs about its ability to enforce security, and the proof chain has been extended to the binary code. The functional correctness proof now exists for the Armv7, x86-64 and RISC-V RV64 architectures, and the kernel and its ecosystem is now supported by the seL4 Foundation. In this talk I will provide an overview of seL4 and its verification story and what it means and doesn’t mean, discuss real-world deployments, as well as on-going research on the principled prevention of timing channels.

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

PWC (https://pwc.to/2FcpqF4)
Atlassian (https://j.mp/313gJJZ)
Google (https://bit.ly/2IiKrCm)
SecDim (https://j.mp/1qgPo0a)
Amazon Information Security (https://j.mp/3eiTfEC)

For sponsoring SecTalks Sydney, Please contact sydney@sectalks.org for more detail.

You may also like