Announce

Download

announce@sel4.systems

June 2020

1 participants
2 discussions

UNSW seL4 teaching videos available
by Announcements about seL4 -- low volume list 02 Aug '20

02 Aug '20

Dear seL4 community, I’m pleased to announce yet another contribution of UNSW Sydney to the seL4 community: This year I’m making the seL4-related videos from my UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel: https://www.youtube.com/playlist?list=PLbSaCpDlfd6qLbEsKquVo3--0gwYBmrUV 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: https://www.cse.unsw.edu.au/~cs9242/current/ Enjoy, Gernot

1 1

RISC-V (RV64) is the third ISA with verified seL4
by Announcements about seL4 -- low volume list 09 Jun '20

09 Jun '20

Dear seL4 community, I’m 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. My blog discusses provides a bit more context for this announcement: https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/ What we have now is 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. Gernot for the Trustworthy Systems team and the seL4 Foundation

1 0