ENSURING SAFE USAGE OF BUFFERS IN PROGRAMMING LANGUAGE C
Milena Vujošević Janičić · 2008
Abstract: We consider the problem of buffer overows in C programs. This problem is very important because buffer overows are suitable targets for security attacks and sources of serious programs ' misbehavior. Buffer over-ow bugs can be detected at run-time by dynamic analysis, and before run-time by static analysis. In this paper we present a new static, modular approach for automated detection of buffer overows. Our approach is ow-sensitive and inter-procedural, and it deals with both statically and dynamically allocated buffers. Its architecture is exible and pluggable for instance, for checking generated correctness and incorrectness conditions, it can use any external automated theorem prover that follows SMT-LIB standards. The system uses an external and easily extendable knowledge database that stores all the reasoning rules so they are not hard-coded within the system. We also report on our prototype implementation, the FADO tool, and on its experimental results. 1