Trustworthy Systems

Verified seL4 on secure RISC-V processors

Authors

Gernot Heiser

DATA61

UNSW Sydney

Abstract

RISC-V has many attractions, ranging from the openness of the architecture, its clean-slate design based on simplicity and scalability, as well as the RISC-V Foundation's strong commitment to security from the ground up. As such, RISC-V is an extremely attractive platform for the open-source seL4 microkernel with its unrivalled verification and security story. This has led industry players, especially Germany-based HENSOLDT Cyber, making a major bet on the combination of RISC-V and seL4, resulting in them funding the formal verification (implementation correctness proof) of seL4 on RISC-V. I will discuss our experience with implementing and verifying seL4 on the RISC-V architecture, and related open-source technologies we are employing to allow us to build secure systems. This includes the CAmkES component framework that supports a security-by-architecture approach, and the Cogent systems language that is designed to reduce the cost of verified system components such as file systems and device drivers. One interesting aspect are timing channels. We have been working for a number of years on *time protection*, the temporal equivalent of memory protection, as a systematic timing-channel prevention. Our experience on x86 and ARM processors is that they lack the mechanisms to do this completely. RISC-V presents an opportunity to get this right, and I will report on my experience working with the RISC-V Foundation's Security Standing Committee to get the required mechanisms into the processor specification.

BibTeX Entry

  @misc{Heiser_20,
    address          = {Gold Coast},
    author           = {Heiser, Gernot},
    booktitle        = {Linux.conf.au},
    date             = {2020-1-17},
    keywords         = {operating systems; verification; cyber security; safety-critical systems; {RISC}-{V}},
    month            = jan,
    note             = { at linux.conf.au},
    numpages         = {online},
    publisher        = {Online},
    slides           = {https://ts.data61.csiro.au/publications/papers/Heiser_20.slides.pdf},
    title            = {Verified {seL4} on secure {RISC}-{V} processors},
    video            = {https://youtu.be/wJ96s3pNtI0},
    year             = {2020}
  }

Download