seL4
Mer info
- Skapad av
- NICTA (numera CSIRO Data61)
- År
- Typ
- Mikrokärna
- Licens
- GPLv2
- Officiell sajt
- sel4.systems
En mikrokärna ur L4-familjen med ett maskinkontrollerat bevis för att C-koden gör exakt vad specifikationen säger.
Forskargruppen vid australiska NICTA publicerade beviset 2009: omkring 8 700 rader C, verifierade i bevisassistenten Isabelle/HOL mot en formell specifikation. Det tog runt 20 personår, ungefär tjugo gånger mer än att skriva koden. Senare bevis visade att den kompilerade binären motsvarar källkoden och att kärnan upprätthåller isolering mellan komponenter.
Kärnan gör nästan ingenting själv — trådar, adressrymder, IPC och kapabiliteter — och resten körs som isolerade processer. Det gör den lämpad för system där en bugg kostar mer än verifieringen: i DARPA:s HACMS-program kördes den i en obemannad helikopter som ett rött team inte lyckades ta över. Koden släpptes som öppen källkod 2014.