Microarchitectural timing channels are a serious security threat: they 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 seL4's refinement proofs from the abstract specification (ASpec) to the (Haskell-derived) executable specification (ESpec), in particular, the addition of key assertions to ensure that the memory addresses accessed by the seL4 kernel are safely overapproximated. As all such assertions are checked by proof obligations that are part of the proof that seL4's ASpec is refined by the ESpec (an intermediate part of its full C refinement proofs), this work will involve both updating the (informal) Haskell specification to make repair to these proofs possible, and carrying out these repairs.

School

Computer Science and Engineering

Research Area

Formal methods | Operating systems

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.

  1. Updates to the ESpec refinement proofs for seL4 where time protection invalidates existing proofs;
  2. A written report describing:

    • The changes made to the ESpec to reflect the time protection changes to the ASpec;
    • The approach taken to repair breakages to the proof of refinement between the updated ASpec and ESpec.