3 Years After L.4 Verified

Presented as part of the 2012 HCSS conference.

In 2009, the L4.verified project delivered a machine-checked, formal proof that the C code of the seL4 microkernel correctly implements its abstract specification. This proof measured roughly 200,00 lines of proof script in the interactive theorem prover Isabelle/HOL. In the years since then, the kernel has been publicly released for evaluation and teaching, has undergone API evolution, and has been even more deeply analyzed, including:

• Security properties such as integrity and authority confinement
• Further specification layers, such as formal capability distribution language that can be used to automatically set up larger user-level systems
• Progress on elminating assumptions of the earlier proof such as extending the formal verification of the kernel to the binary level, and formal verification of the kernel boot process
• Substantial progress on a non-interference/confidentiality proof for seL4
• A process-engineering analysis of how the verification was performed
• Demonstrators showing how to use seL4 in a varity of systems
• The first sound full worst-case execution time profile of any protected OS kernel

The talk will present an overview of the current state of the formal and informal analysis around the seL4 kernel, and will summarize the experience on keeping this large formal proof up-to-date under API evolution and further analysis.

Biography:

Gerwin Klein is Principal Researcher at NICTA, Australia's National Centre of Excellence for ICT Research, and Conjoint Associate Professor at the University of New South Wales in Sydney, Australia. He is leading NICTA's Formal Methods research discipline and was the leader of the L4.verified project that created the world's first formal, machine-checked proof of functional correctness of the C implementation of a general-purpose microkernel in 2009. He joined NICTA in 2003 after receiving his PhD from Technische Universitat Munchen, Germany, where he formally proved type-safety of the Java Bytecode Verifier in the theorem prover Isabelle/HOL. Gerwin has won a number of awards together with his team, among them the 2011 MIT TR-10 award for the top ten emerging technologies world-wide, NICTA's Richard E. Newton impact award for the kernel verification work, the best paper award from SOSP'09 for the same, and an award for the best PhD thesis in Germany in 2003 for his work on bytecode verification.

Acknowledgements: NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program.

This material is in part based on research sponsored by the Air Force Research Laboratory under agreement numbers FA2386-10-1-4105 and FA2386-11-1-4070. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the Air Force Research Laboratory or the U.S. Government.