Then David Wragg wrote:
| These wouldn't be general proofs of just anything - they would
| naturally refer to the subject of the proof (i.e. the code), so that
| altering the code automatically invalidates the proof.
Brandon responded:
> That's the "spoofing" scenario, which as I implied above isn't
> "interesting".
No, David probably doesn't mean the spoofing scenario, and the proofs as
I understand them have nothing to do with digital signatures.
> The point where it falls apart is that a "proof" that some piece of C
> code doesn't have any buffer overflows *cannot* be verified.
That's not true. A trivial example: a program that has no pointer or
array dereferences -> no buffer overflows. Less trivial: a program in
which every pointer or array dereference is immediately preceded by a
bounds check and branch -> no buffer overflows. Less trivial again: the
C program is a Java bytecode interpreter with accompanying bytecode and
bytecode proofs. Even less trivial: real programs.
If you can supply the program, for some programs you can also supply a
proof that there are no buffer overruns. Similarly for other exception
conditions.
> Type validation is useful, but only when the types themselves prevent
> invalid accesses. C types don't insure that you can't write past the
> limits of the typed address range (scalar variable, structure, array,
> etc.), so it doesn't accomplish anything useful in practice.
When we talk about proofs of not crashing for C programs, we're
obviously thinking something more sophisticated than C's normal type
system. In fact it goes beyond types -- type checking a program doesn't
require an accompanying proof script, it's so well defined and fast.
A proof script essentially details the results of a search by a theorem
prover (or sophisticated type checker, if you like). Verification is
simply application of each step of the proof, without the time consuming
search. These steps refer to the code of the program that is being
reasoned about. If the code is wrong, the results of applying the proof
steps won't produce the result "safe".
For some languages (the packet filter code was mentioned), finding the
proofs in the first place is quite reasonably easy. Sometimes so easy
that it can be done as the verification step, or even skipped if all
programs in the language are safe. For more difficult things like
proving a C program doesn't access an array beyond its bounds, generally
an accompanying proof is required because searching for the proof is too
time consuming to do each time you need to verify the code. In fact for
the latter problem, it's too difficult to do even once in practice. But
people are working on that sort of problem.
-- Jamie
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.tux.org/lkml/faq.html