"Brandon S. Allbery KF8NH" <[email protected]> writes:
> [...] given a chunk of C code with a
> proof attached, the proof is untrustworthy (in point of fact, it *lies* if
> it claims there are no buffer overflows, except in degenerate cases that
> only use scalar values --- but the packet itself is not a scalar). You can
> verify that the proof doesn't work, probably, which would be good enough...
> except that (as noted) *no* purported proof will pass this because the
> desired condition is not provable. So proof-carrying code isn't going to
> work here.
This is rubbish. C programs, as well as programs in other languages,
can be proven correct and the proofs can be (machine) verified. It is
only a matter of time, lots of time.
What you are claiming above is (essentially) that all C programs have
buffer overflow. That obviously isn't true. Programs can be *made*
safe by preceding all otherwise unsafe operations by syntactic checks
for bounds. So you would guard all array access with checks that the
index was in the right range, and for all strcpy's you would verify
that the string length was less than the target buffer length. This
is perfectly doable, but might require modification of the program
in question. Programs written this way should be quite easy to prove
free of buffer overflows.
BACK ONTOPIC: code with proofs is interesting for the kernel in the
case of packet filters. You can get very impressive performance that
way. By a rule of thumb, the filtering time should decrease by an
order of magnitude.
Readings: George Necula's and Peter Lee's work on proof-carrying code
"http://www.cs.cmu.edu/~petel/papers/pcc/pcc.html". For a proof of
an interpreter (not a Java interpreter in C, unfortunately), see
[shameless plug] my own Ph.D. thesis which might be found at
"http://www.diku.dk/students/terra/" [slow link].
Morten