seL4 is the world's first operating system (OS) kernel with a proof of implementation correctness, followed by proofs of security enforcement; it is at the same time the benchmark for microkernel performance. The seL4 Microkit is a minimal seL4-based OS framework aimed at embedded and cyberphysical systems.
Since verifying the key functionality of the Microkit's original C implementation using an in-house SMT solver-based framework, research at TS has been exploring the use of a new SMT solver-based automated deductive verification workflow based on transpilation to Viper to verify new Pancake language implementations of the Microkit library and Microkit-based OS components in a more scalable manner.
This project is to continue bringing the verification of the seL4 Microkit library up to date using this workflow and integrate them into the Microkit's continuous integration testing framework.
School
Computer Science and Engineering
Research Area
Formal methods | Formal verification | Operating systems
Suitable for recognition of Work Integrated Learning (industrial training)?
Yes
- Research environment
- Expected outcomes
- Supervisory team
- Reference material/links
The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security and safety critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
- Report describing experience verifying the latest Pancake language version of the seL4 Microkit library using the Viper-based workflow;
- Pull requests against the seL4 Microkit library's implementation and continuous integration testing framework;
- Verification of some simple Microkit-based example systems added to the CI testing framework if time allows.
