Re: Theoretical question about vulnerabilities

[Crispin Cowan <crispin () immunix com>]

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