Alleged "microkernel mathematically proven to be bug free"

Cathal Garvey cathalgarvey at cathalgarvey.me
Tue Jul 29 06:03:28 PDT 2014


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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0x988B9099.asc
Type: application/pgp-keys
Size: 6176 bytes
Desc: not available
URL: <https://lists.cpunks.org/pipermail/cypherpunks/attachments/20140729/655ff37e/attachment-0002.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 901 bytes
Desc: OpenPGP digital signature
URL: <https://lists.cpunks.org/pipermail/cypherpunks/attachments/20140729/655ff37e/attachment-0002.sig>


More information about the cypherpunks mailing list