29 Jul
2014
29 Jul
'14
4:36 p.m.
On Jul 29, 2014 6:14 PM, "Georgi Guninski" <guninski@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!