David Crocker wrote:
Proving that all array accesses are within bounds would seem to be Turing undecidable. Either you are not proving what you way you are proving, or your programs are not full Turing machines.Well, that approach is certainly better than not guarding against buffer overflows at all. However, I maintain it is grossly inferior to the approach we use, which is to prove that all array accesses are within bounds.
Proof: <insert diagonalization argument here :>
Issue: Some people may regard diagonalized programs are a contrivance, and are only interested in correctness proofs for real programs (for some value of "real").
Crispin's rebuttal: Suppose I want to prove that your program checker does not have any illegal array references ...
What exactly is your program going to do when it detects an array bound violation at run-time?
Hermes' kludge to address this was two-fold:
1. There are no arrays. Rather, there are relational tables, and you
can extract a row based on a field value. You can programatically
get a table to act much like an array by having a field with a
unique index number, 1, 2, 3, etc.
2. If you try to extract a row from a table that does not have a
matching value, then you get an exception. Exceptions are thrown
and caught up the call chain the way most modern (Java etc.)
languages do it.Yes, this is a kludge because it ultimately means a run-time exception, which is just a pretty way of handling a seg fault.
Crispin
-- Crispin Cowan, Ph.D. http://immunix.com/~crispin/ CTO, Immunix http://immunix.com
