Trustworthy Systems

UNSW Sydney
Our Partners HENSOLDT Cyber GmbH
ETH Zurich
RISC-V logo

seL4 on the RISC-V Architecture

The open RISC-V architecture has become an important target for seL4, both for research and real-world adoption. Its openness make it an ideal platform for this.

seL4 runs as a supervisor-mode kernel on RISC-V platforms. We track the draft hypervisor-extensions specification to provide virtualisation support. More excitingly, we are working on verifying the RISC-V port of seL4, with proof of functional correctness (to the binary) expected to complete in Q1'20.

Besides that, the availability of open-source FPGA implementations allow us to experiment with hardware improvements. We use this opportunity extensively in our work on time protection.




  • Amirreza Zarrabi
  • Anna Lyons
  • Curtis Millar
  • Ed Pierzchalski
  • Gerwin Klein
  • Hesham Almatary
  • Kent Mcleod
  • Matthew Brecknell
  • Rafal Kolanski
  • Siwei Zhuang
  • Victor Phan
  • Yanyan Shen


Abstract PDF Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser
Microarchitectural timing channels and their prevention on an open-source 64-bit RISC-V core
Design, Automation and Test in Europe (DATE), virtual, February, 2021
Best Paper Award
Abstract PDF
Presentation Video
Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser
Prevention of microarchitectural covert channels on an open-source 64-bit RISC-V core
Valencia, Spain, May, 2020
Abstract PDF Gernot Heiser, Gerwin Klein and June Andronick
seL4 in Australia: From research to real-world trustworthy systems
Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020
Abstract Slides
Gernot Heiser
Verified seL4 on secure RISC-V processors
at, Gold Coast, January, 2020