Formal methods is the use of formal mathematical logic to specify and prove the correctness of software systems.
We are developing mathematical models, software tools and engineering processes that can verify large, interconnected systems at all levels, from the overall design down to the executable code. Our group has demonstrated that the full formal verification of software for complex real-world domains, once thought to be practically impossible, can be achieved in reasonable time and cost.
Our goal is to build verified systems from the ground up; this begins with our formal verification of the seL4 microkernel.
We have proved that seL4's code correctly implements its functional specification, as well as important security properties—both world-first achievements. Today, we continue to extend the proofs to support new seL4 features and hardware platforms.
These are our major developments in progress (also see our seL4 roadmap).
- New kernel features to support mixed-criticality systems.
- Time protection: verification of principled prevention of microarchitectural timing channels
- Concurrent version of seL4 for multi-core processors.
In addition to proving the correctness of seL4's source code, we also verify that it is compiled correctly to ARM and RISC-V machine code.
Our seL4 proofs contain nearly 1 million lines of proof steps, and continue to be expanded. To manage this complexity, we are developing a new systematic discipline of proof engineering.
Verification for user-level software
Using seL4 as a trustworthy base, we are building large-scale software systems with unprecedented reliability and security guarantees. We are developing new programming languages to achieve this goal.
We do research on formal models of concurrency and distributed systems. We also use these models to specify, analyse and verify concurrent software and network protocols.
Our past projects
- Clustered Multikernel — verification of an early version of the multiprocessor seL4 kernel
- Proof measurement and estimation — metrics and estimation methods, to help planning and management of large-scale verification projects
- RISC-V — implementation and verification of seL4 on the 64-bit RISC-V architecture
- Termite — automatic synthesis of device drivers
- TLB — verification of the kernel's management of the translation-lookaside buffer
- Trustworthy component framework — automatic verification of CAmkES component assemblies
- Verification-enhanced compiler optimisation — optimising code based on formally proven properties
- Whole-system assurance — an experiment in verifying user-level system properties over a low-level ARM model
Gernot Heiser, firstname.lastname@example.org
Browse our FM research publications.