1 HN user recommended this talk1 month2015–2019score 1
Years with an HN recommendation, 2007–2026
Cited to explain what formal verification of seL4 guarantees, such as ruling out whole classes of bugs like buffer overflows.
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.
“The whole talk is well worth a watch.” (HN, 2019)
> This is a great view on history of seL4. Is there a list of use cases where seL4 is being used outside academia? "Can you build actual systems with it?" [this video] The whole talk is well worth a watch.
[this video] The implementation is correct against this abstract specification ... so bug-free, etc. The implications, there's many of them, but just a few obvious ones: it's not possible for this kernel to have a buffer overflow; it cannot - it provably does not use uninitialized variables or dereference null pointers, there's no stack smashing, you can't have code injection, there's no return oriented programming. Any of that stuff is just not possible - provably. So that's nice!
seL4 proofs rule out whole classes of memory bugs.
Spent a while on the weekend reading about the seL4 kernel, which uses capability based security and has end to end mathematical proofs of correctness on the compiler and underlying kernel. Its predecessors are used in Apple's A7 and Qualcomm's chips. Watching [this video] and it says that it's mathematically impossible for seL4 to suffer from things such as buffer overflows. I'm faaaaaar out of my field here... but this sounds as like a far better improvement in security compared to running things in a chroot. Apart from it being really new (there's just a kernel with a C compiler), would this be a good route to head down for improving security? Why aren't we writing a linux port on this? Kernel info here: [link]
Video list and Hacker News comment labels from HackerTube (prompted by @karpathy), released under ODC-By 1.0, built on the open-index/hacker-news archive. Hacker News data is provided by Y Combinator; comments remain the work of their authors. Video titles, channel names and thumbnails belong to their creators and are shown via YouTube. HackerTube Watch is an unofficial edition. Data export of 2026-10-31.
Plays via YouTube's privacy-enhanced embed
3 Hacker News comments
From the HN archive; up to 20 kept per video, favoring different commenters. Recommendations first.
Citations, criticism and jokes
Read more