"seL4 co-habitating the hardware" with untrustworthy firmware: Roman from ETH at the #seL4Summit about real-world hardware

Rob from Trustworthy Systems at the #seL4Summit talks about TS verification work aiming for whole system security

Incremental cyber retrofit at work: Nathan from DornerWorks talks at the #seL4Summit about running ROS on seL4

Clearly, more students need to take UNSW's Advanced Operating Systems course!

Miki from Trustworthy Systems at the #seL4Summit presenting Pancake, our new systems language with verified compiler, which we're using to implement and verify LionsOS components

Courtney from Trustworthy Systems at the #seL4Summit talking about optimising the synchronisation messages between the asynchronous components of the seL4 device driver framework

Leigha VanderKlok from DornerWorks reports on experience with the Microkit VMM at the #seL4Summit - tl;dr mostly good, few more things to do

Proud as a peacock watching TSer Ivan delivering his #LionsOS talk at the #seL4Summit from an Arm board running LionsOS

Happy seL4 Day everyone!

The GoFetch attack demonstrates (yet again) that trying to combat microarchitectural attacks leads nowhere, other than making the hardware more complex (and thus buggy).
In contrast, we have demonstrated years ago time protection as a principled pervention of such attacks. Needless to say, time protection defeats GoFetch.
Read more on my blog: https://microkerneldude.org/2024/04/18/gofetch-will-people-ever-learn/