hackertube.io

seL4 Is Free – What Does This Mean For You?

Linux.conf.au 2015 -- Auckland, New Zealand · talk · Watch on YouTube

Operating systems & kernelsLogic & formal methodsSecurity & hacking

What it is

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.

Why Hacker News recommends it

Cited to explain what formal verification of seL4 guarantees, such as ruling out whole classes of bugs like buffer overflows.

  • 1 people recommended it
  • 1 different months
  • 0 strong recommendations
  • first 2015, last 2019

What HN commenters said

  1. “The whole talk is well worth a watch.”

    Talk on building actual systems with seL4.

    rodgerd, 2019-08 · Recommendation · in “10 Years SeL4: Still the Best, Still Getting Better”

Excerpts from Hacker News comments, linked to the originals. Summaries and labels were written by a language model from those comments.

Topics: sel4, microkernel, formal verification, security, linux.conf.au

Also recommended by the same people