seL4 on RISC-V is verified to the binary

2021-05-05 – The seL4 Foundation and RISC-V International announced that the verified seL4 microkernel on the RV64 architecture has been proved down to the executable code by the Trustworthy Systems group, thanks to funding provided by HENSOLDT Cyber GmbH. This guarantees that the seL4 microkernel on RV64 will operate to specification even when built with an untrusted C compiler, GCC. For more details on binary verification of seL4 on RISC-V see Gernot's blog: seL4 on RISC-V Verified to Binary Code (and seL4 and RISC-V Foundations form an alliance).

Gernot has been appointed as one of ACM’s Distinguished Speakers
2021-05-04 Professor Gernot Heiser has been appointed as one of ACM's Distinguished Speakers, "Renowned International Thought Leaders Speaking on the Most Important Topics in Computing Today"! You can see the full list of speakers here. Congratulations to Gernot for joining this illustrious group!

Gernot Heiser named ICT Researcher of the Year
2021-04-20 Congratulations goes to Gernot Heiser on receiving the 2015 Digital Disruptor - ICT Researcher of the Year in what was an extremely competitive category..more

seL4 is verified on RISC-V

2020-06-09 – Trustworthy Systems is extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible. We now have the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future. You can find more details about the verification of seL4 on RISC-V on Gernot's blog

seL4 teaching videos available

2020-06-02 – Yet another contribution of UNSW Sydney to the seL4 community: This year Gernot Heiser is making the seL4-related videos from his UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel. At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site.