HackerTube / Video
seL4 Is Free – What Does This Mean For You?
Linux.conf.au 2015 -- Auckland, New Zealand
Gernot Heiser presents seL4, a microkernel with a mathematical proof connecting security properties to the binary code, and explains what its open-sourcing means for users. It covers its roles as a microkernel, separation kernel and hypervisor.
Cited to explain what formal verification of seL4 guarantees, such as ruling out whole classes of bugs like buffer overflows.
3 Hacker News mentions · 2015–2019