Description of field of research
Microarchitectural timing channels are a serious security threat, that can be used to steal critical secrets, such as the encryption keys of web servers. We have recently developed mechanisms, collectively referred to as time protection in the seL4 microkernel that aim to prevent timing channels being exploited across security boundaries. These mechanisms have been formalised and are now being formally verified.
This project is to contribute to updating the proof base for seL4 to account for changes made to seL4's abstract specification to incorporate the time-protection mechanisms. seL4's proof base is a significant piece of proof engineering, and making core changes to the specification results in significant work updating these proofs. While frameworks to perform such proof updates have been developed, much proof work remains to be completed.
School
Research Area
Formal methods | Operating systems
- Research Environment
- Expected Outcomes
- Reference Material/Links
- Our Team
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.
- completing the time protection breakages in the abstract specification proofs for seL4.
- written report describing the types of breakages caused by the time protection changes to seL4's abstract specification, and the approach taken to repair these breakages.
