30 Jul
2014
30 Jul
'14
10:13 p.m.
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