Trustworthy Systems

Refining seL4's accounting of touched addresses for time protection

Authors

Thomas Liang

    School of Computer Science and Engineering
    UNSW,
    Sydney 2052, Australia

Abstract

Given that a Haskell program and a C program have the same behaviour, and the knowledge that the Haskell program only accesses addresses in a certain partition, how can you prove that the C program does also? Time Protection is a recently proposed and implemented set of mechanisms for the seL4 microkernel. It eliminates microarchitectural timing channels, the leaking of information through the timing of hardware events and also a major threat to computer security. To verify Time Protection, we must take the existing refinement proof—from seL4’s intermediate Haskell implementation to its true C implementation—and extend it to show that its touched addresses set does not stray from a defined partition. I give a summary of the verification of seL4 and Time Protection so far, give a formalisation of touched addresses, and then demonstrate a proof method on a small part of the kernel. Finally, I give an argument that the methods can be scaled to verify the rest of the kernel.

BibTeX Entry

  @mastersthesis{Liang:bsc,
    address          = {Sydney, Australia},
    author           = {Thomas Liang},
    month            = nov,
    paperUrl         = {https://trustworthy.systems/publications/theses_public/25/Liang%3Absc.pdf},
    school           = {School of Computer Science and Engineering},
    title            = {Refining {seL4}'s Accounting of Touched Addresses for Time Protection},
    type             = {{BSc(Hons)} Thesis},
    year             = {2025}
  }

Download