Alleged "microkernel mathematically proven to be bug free"
Georgi Guninski
guninski at guninski.com
Tue Jul 29 09:14:18 PDT 2014
>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?
More information about the cypherpunks
mailing list