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
