We would like to acknowledge the help and support that we received
from our research partners and collaborators during this project.
In particular, we thank the development team of the Isabelle theorem prover for their
help and support. Isabelle is the main verification tool used in this
project and without its maturity success would not have been possible.
We thank the folks at Galois
Inc who have worked with us to develop an open source proof
library and theory for fixed-size machine words (e.g. 32 bit
We also would like to acknowledge the contribution of our friendly
competition, the German Verisoft
project with whom we share some verification technology. In particular
we would like to thank Norbert Schirmer whose verification framework
for imperative programs we instantiate to the C language.
On the kernel side, the OS hackers at Open Kernel Labs have kept us
on track and in connection with real-world customer requirements.
Finally, we thank (and you don't see that often in a research institution)
the NICTA executive team who saw through our strange formulas, believed in the
project and supported it from the beginning.
Dramatis Personae (aka The Team)
The L4.verified team over time included the following persons (in alphabetical order).
- June Andronick
Software certification and C verification expert and our team spirit. Yes, we can!
- Timothy Bourke
Invaluable Isabelle tools, security proofs, and a true engineer.
- Andrew Boyton
PhD student, security models and proofs.
- David Cock
The ARM hardware model expert, hardware simulator generator generator, performance tuner, and Research Engineer gone PhD student.
- Jeremy Dawson
Proof libraries and word arithmetic. Proof automation.
- Philip Derrin
Kernel design, implementation, verification. You name it, he can do it.
- Kai Engelhardt
The man for refinement. Keeping us on the
right track and preventing us from re-inventing too many wheels in
- Kevin Elphinstone
Senior kernel expert and lead designer. Chief OS hacker who had to bear with all the strange formulas on our whiteboards.
- Gernot Heiser
Chief visionary and our most demanding customer. Also NICTA ERTOS group leader, John Lion's Professor at UNSW, CTO and co-founder of Open Kernel Labs.
Project leader, management, leadership, proofs, and chief optimist.
- Rafal Kolanski
IPC modelling, Virtual Memory modelling, the man for Separation Logic.
- Jia Meng
The connection to the world of first-order and automated proof. Automated termination proofs.
- Catherine Menon
Refinement proofs and C state relation.
- Michael Norrish
The C expert. Making Isabelle read messy low-level C programs without disappearing in a cloud of logic.
- Thomas Sewell
Chief verification engineer. Haskell refinement framework. Tools, models, proofs, ideas, insight: ask Thomas.
- David Tsai
ARM11 machine and instruction model. Handwritten and generated.
- Harvey Tuch
The foundation. The C memory model on which everything rests. CISRA PhD prize winner.
- Simon Winwood
Kernel objects, Types and Retypes. C refinement framework. Who's afraid of an evil proof?