Value-Range Analysis of C Programs

Towards Proving the Absence of Buffer Overflow Vulnerabilities

Reference: Bibtex

The book describes a how to statically analyse C programs by defining the semantics of C at the level of bits and bytes before approximating each operation using polyhedral, congruence, and points-to abstractions. An efficient implementation of polyhedral operations is presented as well as an extension to the analysis that tracks the position of zero characters in strings. This book will be interesting for anyone interested in program analysis, in particular:

• Researchers interested in the analysis of higher-level program properties such as shape analysis of heap and array contents. The bit-level abstraction relation presented in this book provides a framework and a justification for defining analyses that omits the treatment of low-level details such as pointer arithmetic and casting.
• Ph.D. students and other researchers who aim to prove the partial correctness of source code. While the book presents an analysis of C, many concepts presented carry over to the analysis of e.g. Java or even machine code.
• Students attending compiler construction/optimisation courses or courses on verification. The analysis defined in this book provides additional motivation by presenting an analysis defined on a full programming language, thereby enforcing the message that a fully formal approach is possible, even for real-world problems.
• Anyone interested in source code analysis. The formal yet concise definition of an analysis of a real-world programming language can help to define a simiar description for the purpose of slicing, taint analysis, calculating metrics and many other application areas.
• Anyone interesting in building tools to eliminate buffer overflow vulnerabilities. The book presents a sound and precise model for tracking the zero character in C strings.

If you have any questions about this book, please feel free to email me.