Gerwin Klein is a Senior 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 first machine-checked proof of functional correctness of a general-purpose microkernel in 2009. He joined NICTA in 2003 after receiving his PhD from Technische Universität München, Germany, where he formally proved type-safety of the Java Bytecode Verifier in the theorem prover Isabelle/HOL.
His research interests are in formal verification, programming languages, and low-level systems. 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. When he is not proving theorems and working on trustworthy software, he enjoys travelling and dabbling in martial arts and photography. Together with Tobias Nipkow he has just published an online draft of the text book Concrete Semantics that teaches programming language semantics using the Isabelle theorem prover.
Highlights of Klein’s thoughts, from the interview below:
- Verifying code not designed for verification is very difficult and costly. Such “post-mortem verification” has other disadvantages as well.
- Program designers can use abstraction, modularity, and explicit architecture choices to help make complex systems transparent to humans.
- There are two ways probability can play a role in verification: (1) direct probabilistic reasoning, in the logic or in a setting where the program itself is probabilistic, or (2) standard non-probabilistic reasoning paired with subjectively uncertain reasoning about what a guarantee means for the overall probability that the system will work as intended.
- Truly autonomous systems seem to be a long ways off, but if you could make a system with truly unexpected behavior, then you couldn’t make it safe.
Luke Muehlhauser: In your forthcoming paper “Comprehensive Formal Verification of an OS Microkernel,” you and your co-authors describe the kernel design (seL4) you used to ensure its verification would be tractable. You also discuss the process of keeping the formal proof current “as the requirements, design and implementation of the system [changed] over almost a decade.”
How “micro” is the seL4 microkernel? That is, what standard functionality does it provide, and what functionality (that is common in larger OS kernels) does it not provide?
Gerwin Klein: It is pretty micro: it is a true micro-kernel in the L4 tradition. This means it is very small compared to traditional monolithic OS kernels: Linux has on the order of a few million lines of code, seL4 has on the order of 10,000 lines of C. seL4 provides only the core mechanisms that you need to build an OS. These include threads and scheduling, virtual memory, interrupts and asynchronous signals, as well as synchronous message passing. The maybe most important feature of seL4 is its strong access control mechanism that can be used together with the rest to build isolated components with controlled communication between them. These components could be small isolated device drivers or an entire Linux guest OS, the developer can choose the granularity.
The philosophy is: if a mechanism strictly needs privileged hardware access to be implemented, it is in the kernel, but if it can be implemented using the other mechanisms as a user-level task, it is outside the kernel. A surprising amount of features can be outside: device drivers, for instance, graphics, files and file systems, network stacks, even disk paging is not provided by seL4, but can be implemented on top of it. What you (hopefully) get is that tricky complexity is concentrated in the kernel, and user-level OS components become more modular.
Read more »