This book describes a static analysis that aims to prove the absence of buffer overflows in C programs. The analysis is conservative in the sense that it locates every possible overflow. Furthermore, it is fully automatic in that it requires no user annotations in the input program.

-

A buffer overflow occurs when input is written into a memory buffer that is not large enough to hold the input. Buffer overflows may allow a malicious person to gain control over a computer system in that a crafted input can trick the defective program into executing code that is encoded in the input itself. They are recognised as one of the most widespread forms of security vulnerability,and many workarounds, including new processor features, have been proposed to contain the threat. This book describes a static analysis that aims to prove the absence of buffer overflows in C programs. The analysis is conservative in the sense that it locates every possible overflow. Furthermore, it is fully automatic in that it requires no user annotations in the input program.



The key idea of the analysis is to infer a symbolic state for each program point that describes the possible variable valuations that can arise at that point. The program is correct if the inferred values for array indic