der Mouse wrote:
[B]uffer overflows can always be avoided, because if there is ANY
input whatsoever that can produce a buffer overflow, the proofs will
fail and the problem will be identified.
Then either (a) there exist programs which never access out-of-bounds
but which the checker incorrectly flags as doing so, or (b) there exist
programs for which the checker never terminates (quite possibly both).
(This is simply the Halting Theorem rephrased.)
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.
How much of this optimization can be done is arguable:
* The Jones&Kelly GCC enhancement that does full array bounds
checking makes (nearly?) no attempt at this optimization, and
suffers slowdowns of 10X to 30X on real applications.
* The Bounded Pointers GCC enhancement that does full array bounds
checking but with a funky incompatible implementation that makes
pointers bigger than a machine word, does some of these
optimizations and suffers a slowdown of 3X to 5X. Some have argued
that it can be improved from there, but "how much" remains to be seen.
* Java compilers get the advantage of a language that was actually
designed for type safety, in contrast with C that aggressively
makes static type checking difficult. The last data I remember on
Java is that turning array bounds checking on and off makes a 30%
difference in performance.
Crispin
--
Crispin Cowan, Ph.D. http://immunix.com/~crispin/
CTO, Immunix http://immunix.com
