Proving Safety of Array Accesses in C Programs

Simon Goldsmith
(Professor Alexander Aiken)

Writing outside the bounds of arrays causes security problems and memory corruption bugs in C programs. CCured is a system that addresses this class of bugs by guarding potentially unsafe memory accesses with run-time safety checks. In the presence of these checks, buffer overruns and insidious memory corruption bugs become simple crashes. The cost of these checks is decreased performance. Our research uses a flow sensitive type-inference system to prove statically that some of the array bound checks inserted by CCured will always succeed and thus can be eliminated. Future work may investigate using our type-inference system as a tool to find array access bugs statically.

Send mail to the author : (

Edit this abstract