Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities
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 in to 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 infera symbolic state for each p- gram point that describes the possible variable valuations that can arise at that point. The program is correct if the inferred values for array indices and pointer offsets lie within the bounds of the accessed buffer. The symbolic state consists of afinite set of linear inequalities whose feasible points induce a convex polyhedron that represents an approximation to possible variable valuations. The book formally describes how program operations are mapped to operations on polyhedra and details how to limit the analysis to those p- tions of structures and arrays that are relevant for verification. With respect to operations on string buffers, we demonstrate how to analyse C strings whose length is determined by anul character within the string.
1101512166
Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities
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 in to 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 infera symbolic state for each p- gram point that describes the possible variable valuations that can arise at that point. The program is correct if the inferred values for array indices and pointer offsets lie within the bounds of the accessed buffer. The symbolic state consists of afinite set of linear inequalities whose feasible points induce a convex polyhedron that represents an approximation to possible variable valuations. The book formally describes how program operations are mapped to operations on polyhedra and details how to limit the analysis to those p- tions of structures and arrays that are relevant for verification. With respect to operations on string buffers, we demonstrate how to analyse C strings whose length is determined by anul character within the string.
169.99
In Stock
5
1
Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities
302
Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities
302
169.99
In Stock
Product Details
| ISBN-13: | 9781848000162 |
|---|---|
| Publisher: | Springer London |
| Publication date: | 06/19/2008 |
| Edition description: | 2008 |
| Pages: | 302 |
| Product dimensions: | 6.10(w) x 9.25(h) x 0.03(d) |
From the B&N Reads Blog