Trustworthy Systems

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

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).

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.

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

Contact

Gernot Heiser, gernot@unsw.edu.au

Publications

Browse our FM research publications.