Alleged "microkernel mathematically proven to be bug free"

Lodewijk andré de la porte l at odewijk.nl
Tue Jul 29 09:36:19 PDT 2014


On Jul 29, 2014 6:14 PM, "Georgi Guninski" <guninski at guninski.com> wrote:
>
> >These proofs tie a meta-specification to the actual code. Look into the
> >sort of proofs they use. Basically they're saying "the code does what we
> >said it has to. Only if we accidentally told it to go skynet on us, it
will
> >work perfectly". Things like segfaults would be pretty clearly not as
> >specified.
>
> By browsing the proofs, I have the impression
> they don't depend on the C code (and Isabelle
> parsing C appears not very trivial, though
> possible).
>
> If I backdoor the C code of the kernel, will
> the proof fail?

Isn't that the whole idea? It would really change the thing up if there's a
backdoor!
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/html
Size: 939 bytes
Desc: not available
URL: <http://lists.cpunks.org/pipermail/cypherpunks/attachments/20140729/a8dd3c4c/attachment-0001.txt>


More information about the cypherpunks mailing list