RE: Theoretical question about vulnerabilities

["David Crocker" <dcrocker () eschertech com>]

Crispin Cowan wrote:

> >
Precisely because statically proven array bounds checking is Turing Hard, that
is not how such languages work.

Rather, languages that guarantee array bounds insert dynamic checks on every
array reference, and then use static checking to remove all of the dynamic
checks that can be proven to be unnecessary. For instance, it is often the case
that a tight inner loop has hard-coded static bounds, and so a static checker
can prove that the dynamic checks can be removed from the inner loop, hoisting
them to the outer loop and saving a large proportion of the execution cost of
dynamic array checks.
<<

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. What exactly
is your program going to do when it detects an array bound violation at
run-time? You can program it to take some complicated recovery action; but how
are you going to test that? You can abort the program (and restart it if it is a
service); but then all you have done is to turn a potential security
vulnerability into a denial of service vulnerability.

So the better approach is to design the program so that there can be no buffer
overflows; and then verify through proof (backed up by testing) that you have
achieved that goal.

David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com