Trustworthy Systems

Updating L4v invariants to aid time protection proofs

Authors

Sai Nair

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

Abstract

Microarchitectural timing channels threaten the security of computers across the globe. Recently, a set of operating system mechanisms, collectively called time protection, was proposed by Qian Ge as a way to close these channels, and was implemented and demonstrated to work correctly in an experimental version of seL4. A follow-up paper by Buckley, Sison et al. described a potential workflow for formalising time protection in seL4 by linking these mechanisms to existing proofs about the flow of information between security domains.

This report discusses a modified approach to formalising time protection in seL4, and details the efforts made to add an invariant on top of seL4’s abstract specification. The invariant specifies that any kernel objects accessible to a security domain may only reference other memory regions accessible to that domain. This report also discusses the process through which this result can be utilised in more concrete specifications of seL4 to show that it partitions kernel memory in accordance with time protection.

BibTeX Entry

  @mastersthesis{Nair:bsc,
    address          = {Sydney, Australia},
    author           = {Sai Nair},
    keywords         = {L4v, time protection, micro-architectural timing channels, seL4, covert channels, isabelle/hol,
                        invariance proofs, refinement},
    month            = nov,
    paperUrl         = {https://trustworthy.systems/publications/theses_public/25/Nair%3Absc.pdf},
    school           = {School of Computer Science and Engineering},
    title            = {Updating {L4v} Invariants to Aid Time Protection Proofs},
    year             = {2025}
  }

Download