Simplifying Buffer Overflow Detection Using Site-Safe Expressions

We present a highly automated technique to identify buffer overflows in C source code, and implement the approach in our prototype cboc. It is a sound tool, and of particular significance is its ability to easily deal with pointer expressions and dynamic memory allocations, which are integral parts of the buffer overflow problem. Our implementation hinges on a key design consideration: introducing the notion of site-safe expression allows us to manage pointer de-reference expediently, and the expense is that it may yield some false alarms. Fortunately, only a small number of false alarms are reported, and all probable false alarms belong to a special alarm type non-site-safe. Experiments show that cboc is competitive with state-of-the-art model checker CBMC.