L4 microkernels: The lessons from 20 years of research and deployment

Re:L4 microkernels: The lessons from 20 years of research an... by TheMagicHorsey on Tuesday September 20, 2016 @11:00AM (#12540012)

If the goal is to provide a verifiably correct kernel, why not build that kernel in something like OCAML so you can leverage a better type system and use the existing verification infrastructure in that language?

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by wyager on Tuesday September 20, 2016 @12:59PM (#12541024)

They did. There's an Isabelle spec, a Haskell implementation, and a C implementation which I believe is mechanically generated from the Haskell implementation.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by cmrx64 on Tuesday September 20, 2016 @01:55PM (#12541611)

The C code is manually written.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by jkot on Tuesday September 20, 2016 @11:09AM (#12540086)

I think you would also have to verify resulting binary, compiler, libraries...

It seems more manageable to verify a few KB of assembly or C

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by nickpsecurity on Tuesday September 20, 2016 @01:10PM (#12541114)

It would seem but it's actually the opposite with existing tooling thanks to COGENT. Amateurs did a filesystem with a fraction of the work that pro's did the kernel:

https://ts.data61.csiro.au/projects/TS/cogent.pml

Note: See "Cogent: Verifying high-assurance file system..."

They leverage the same tools used for seL4 verification. Also worth noting that Myreen et al's toolkit basically converts HOL specifications to machine code without need for an external compiler. The "C" that was compiled was an embedding of it in HOL called Simpl which the aforementioned process verifies and converts to verified code. This is called translation validation. That's my non-specialist understanding of what the papers said. COGENT builds on this process to convert functional language and easier specs into that form which gets trans-validated into machine code. With less effort. :)

Note: Myreen et al are doing both verifications of HOL itself and HOL to hardware translation next. These further reduce the TCB of provers and hardware respectively to almost nothing but the specs.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by pjmlp on Tuesday September 20, 2016 @12:09PM (#12540601)

Not really, to verify C code you need to set the compiler and its corresponding version in stone for the verification process, as UB can change even between versions of the same compiler.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by cmrx64 on Tuesday September 20, 2016 @12:11PM (#12540630)

Not really true. See https://www.nicta.com.au/publications/research-publications/... for how the compiler and its internal semantics are completely removed from the chain for l4v.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by pjmlp on Wednesday September 21, 2016 @02:57AM (#12545977)

Thanks for the link, I will have a look into it.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by felixk42 on Wednesday September 21, 2016 @10:20PM (#12553870)

Exactly, and then one has to deal with the runtime and GC.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by ynniv on Tuesday September 20, 2016 @11:52AM (#12540454)

sel4 was specified in Haskell and then converted to C

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by cmrx64 on Tuesday September 20, 2016 @12:12PM (#12540640)

The "real" specification (if it can be said to exist) is the abstract spec, in Isabelle/HOL.

[ Parent | on HN ]