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 and platforms

These are our major developments in progress (also see our seL4 roadmap).

New kernel features to support mixed-criticality systems.
Concurrent version of seL4 for multi-core processors.
seL4 port to the RISC-V processor architecture.
Verification for translation lookaside buffer management.

Proving compiler 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.

Cogent

Our Cogent language aims to simplify the verification of the device drivers and services that are needed in a modern operating system. Cogent has a formally verified toolchain, covering the entire compilation process from type-checking to low-level code output.

CakeML

CakeML is a verified compiler for a high-level functional language, suitable for application-level software.

CakeML is a collaborative project by researchers at multiple institutions. Here at Trustworthy Systems, our work focuses on applying CakeML to systems programming, and verifying the behaviour of CakeML programs in the context of larger systems.

Trustworthy component framework

It is not enough to prove the correctness of individual components in a software system; the overall system configuration and connections also need to be correct. We are implementing automatic verification tools for our CAmkES component framework.

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.

Smart contracts verification

Smart contracts are blockchain-based programs that carry out business or financial processes; errors in these programs can lead to disastrous losses that are difficult to recover. Formal verification can provide the highest level of confidence in the correct behaviour of smart contracts.

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
Termite — automatic synthesis of device drivers
Verification-enhanced compiler optimisation — optimising code based on formally proven properties
Verified garbage collector — verifying a fast garbage collector on modern processors
Whole-system assurance — an experiment in verifying user-level system properties over a low-level ARM model

Contact

Gerwin Klein, gerwin.klein@data61.csiro.au

Publications

Browse our FM research publications.