Interprocedural bounds checker for C programs using symbolic constraints and slicing
Edvin Török
Abstract:
We describe a tool for finding out-of-bounds memory access bugs in C programs,
which can be used to check programs with more than 100 000 lines of source code
in time comparable to compilation time.
Our tool doesn't search for out-of-bounds pointers, but only for dereferences of
out-of-bounds pointers (not including NULL dereferences).
An interprocedural analysis marks the variables that influence the validity of the accesses,
and by using slicing we reduce the program to only the code corresponding to these.
Afterwards, by using a variety of code optimization techniques, we obtain a code based on which
we create symbolic expressions, and using them we check whether accesses are within bounds using them.
If this is undecidable based purely on the symbolic expressions, we take into account
the predicates that dominate these memory accesses, and query a solver to determine the validity
of the access.
We eliminate the accesses we could prove, and repeat the above steps until we either prove all
accesses, or we reach the inlining limit.
The tool is successful in catching simple cases of common bugs encountered during application development
such as off-by-one bugs.
BibTeX:
@unpublished{ETOROK:BOUNDS,
author = {Edvin T\"{o}r\"{o}k},
title = {Interprocedural bounds checker for C programs using symbolic
constraints and slicing},
note = {final year thesis},
school = {"Politehnica" University of Timisoara},
year = {2009},
month = {June}
}
Paper:
Slides (in Romanian):
