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:
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.
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.