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

Current

Past

  • Amirreza Zarrabi
  • Anna Lyons
  • Ed Pierzchalski
  • Hesham Almatary
  • Kent Mcleod
  • Yanyan Shen

Publications

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
Workshop on Computer Architecture Research with RISC-V (CARRV), 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
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.