That seems suspect. Most obvious security flaws in C are due to misimplemented C, right? Not the algorithms themselves? So the kernel can be theoretically secure but still be packed with buffer overflows and pointer errors?
I'll wait until someone redoes it in a language designed for safe systems programming, like Rust. :) On 29/07/14 13:41, Georgi Guninski wrote: > I didn't spend much time on this, just browsed > some proofs. The proofs appear to not depend to > on the C code AFAICT. Would trojanizing the C > code invalidate the proofs? > > The haskell stuff appear to not contain all > info about the C code. > > On Mon, Jul 28, 2014 at 06:26:50PM +0300, Georgi Guninski wrote: >> news: >> http://www.theregister.co.uk/2014/07/28/aussie_droneprotecting_hackerdetecting_kernel_goes_open_source/ >> site: >> http://sel4.systems/ >> >> AFAICT they used Isabelle for the proofs. >> >> Coq sucks much (not counting its developers). -- T: @onetruecathal, @IndieBBDNA P: +353876363185 W: http://indiebiotech.com
0x988B9099.asc
Description: application/pgp-keys
signature.asc
Description: OpenPGP digital signature
