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.
|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
||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
|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
Verified seL4 on secure RISC-V processors
at linux.conf.au, Gold Coast, January, 2020