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
- Smart contracts 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 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 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.