Value-Range Analysis of C Programs

Towards Proving the Absence of Buffer Overflow Vulnerabilities

Häftad, Engelska, 2011

AvAxel Simon

2 029 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt för medlemmar vid köp för minst 249 kr.

Finns i fler format (1)

Inbunden

2 029 kr

Skickas inom 10-15 vardagar

The book formally describes how program operations are mapped to operations on polyhedra and details how to limit the analysis to those p- tionsofstructuresandarraysthatarerelevantforveri?cation.Withrespectto operations on string bu?ers, we demonstrate how to analyse C strings whose length is determined by anul character within the string.

Produktinformation

Utgivningsdatum2011-05-15
Mått155 x 235 x 18 mm
Vikt493 g
FormatHäftad
SpråkEngelska
Antal sidor302
FörlagSpringer London Ltd
ISBN9781849967020

Tillhör följande kategorier

From the Contents: Preface.- Introduction.-Value Range Analysis.- Analysing C.- A Semantics for C.- Core C.- Related Work.- Part 1 Abstracting Soundly.- Abstract State Space.- Points-To Analysis.- Numeric Domains.- Taming Casting and Wrapping.- A Language Featuring Finite Integer Arithmetic.- Implicit Wrapping of Polyhedral Variables.- Explicit Wrapping of Polyhedral Variables.- An Abstract Semantics for SubC.- Discussion.- Overlapping Memory Accesses and Pointers.- Memory as a Set of Fields.- Mixing Values and Pointers.- Abstraction Relation.- Abstract Semantics.- Part II Ensuring Efficiency.- Planar Polyhedra.- Operations on Inequalities.- Operations on Sets of Inequalities.- The TVPI Abstract Domain.- The Integral TVPI Domain.- Interfacing Analysis and Numeric Domain.- Inferring Relevant Fields and Addresses.- Applying Widening in Fixpoint Calculations.- Part III Improving Precision.- Tracking String Lengths.- Widening with Landmarks .- Combining Points-To and Numeric Analysis.- Conclusion and Outlook

From the reviews: "This book describes a static analysis that aims to prove the absence of buffer overflows in C programs. ... The book formally describes how program operations are mapped to operations on polyhedra. ... Many concepts presented here carry over to other languages such as Java or assembler. So it will be useful to any researcher and student with an interest in static analysis of real-world programming languages." (Stefan Meyer, Zentralblatt MATH, Vol. 1155, 2009)