Alleged "microkernel mathematically proven to be bug free"

Ted Smith tedks at riseup.net
Wed Jul 30 15:13:54 PDT 2014


On Tue, 2014-07-29 at 19:14 +0300, Georgi Guninski 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?

In short, as others have said, you're wrong about the lack of
dependency. See: http://www.nicta.com.au/pub?doc=7371



-- 
Sent from Ubuntu
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: This is a digitally signed message part
URL: <https://lists.cpunks.org/pipermail/cypherpunks/attachments/20140730/23f68825/attachment-0002.sig>


More information about the cypherpunks mailing list