Skip to main content

Our Partners
HENSOLDT Cyber GmbH
The University of New South Wales
ETH Zurich

seL4 on the RISC-V Architecture

RISC-V logo

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.

People

Publications

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
Video
Gernot Heiser
Verified seL4 on secure RISC-V processors
at linux.conf.au, Gold Coast, January, 2020
Served by Apache on Linux on seL4.