Fwd: seL4 is going open source
Toby Murray <tobycmurray-gM/[email protected]>
| Newsgroups | gmane.comp.capabilities.general |
|---|---|
| Message-ID | <CAB_O7MJNhYOaH0uE+1TzP+t_w5cBOFEwy3W-S5MZairV9uWhww@mail.gmail.com> |
cap-talkers: seL4, a capability-based microkernel whose implementation has been comprehensively formally verified, is soon to be open source along with its formal proofs and associated tools. If you're interested, you can find out more at http://sel4.systems For those who like academic papers, an overview of seL4 and its verification is described in the following paper (which I can assure you is readable without a strong background in formal methods): Comprehensive formal verification of an OS microkernel Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser ACM Transactions on Computer Systems, vol. 32, no. 1, pp. 2:1--2:70, Feb. 2014 http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml Cheers Toby