Skip to main content

Our Partners
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.



Abstract Slides
Gernot Heiser
Verified seL4 on secure RISC-V processors
at, Gold Coast, January, 2020
Served by Apache on Linux on seL4.