Formal methods

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.

• seL4 verification
• Verification for user-level software
• Concurrency and protocol verification
• Past projects
• Publications

seL4 verification

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.

New features

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.

Proving compilation correctness

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.

Proof engineering

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.

Concurrency and protocol verification

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.