Computer Science and Engineering
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. TS is presently developing Lions OS, using the same, highly-modular design as the seL4 Device Driver framework (sDDF).
Lions OS is designed for simplicity and strong separation of concerns. This means that many of the components making up the OS have very simple implementation, which should enable their formal verification, ideally using proof techniques based on SMT solvers, which were already successfully used in the verification of the Microkit.
This project is to investigate the use of SMT solvers to specify and verify the enforcement of per-component security subpolicies. Here, a subpolicy is what a trusted component must adhere to in order to enable verification of enforcement of a system-wide policy.
School
Research Area
Formal methods | Operating systems
- 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.
- Formal specification of a security subpolicy for one Lions OS component;
- Successful verification of the subpolicy for at least a subset of the anticipated cases;
- Report describing experience verifying security subpolicies for an OS component using SMT solvers;
- Potentially pull requests against the Lions OS implementation.
