Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities

Introduction .- Technical Background.- Value Range Analysis.- Analysing C.- Soundness.- An abstraction of C.- Combining Value and Content Abstraction.- Combining Pointer and Value-Range Analysis.- Efficiency.- Completeness.- Analysing String Buffers.- Widening with Landmarks.- Further Refinements.- Related Tools.- The Astrée Anlyser.- SLAM and ESPX.- CCured.- Other Approaches.- Contributions.- A Semantics for C .- Core C.- Preliminaries.- The Environments.- Concrete Semantics.- Collecting Semantics.- Related Work.- Abstracting Soundly .- Abstract State Space .- An Introductory Example.- Points-To Analysis.- The Points-To Abstract Domain.- Related Work.- Numeric Domains.- The Domain of Convex Polyhedra.- Operations on Polyhedra.- Multiplicity Domain.- Combining the Polyhedral and Multiplicity Domain.- Related Work.- Taming Casting and Wrapping .- Modelling the Wrapping of Integers.- A Language Featuring Finite Integer Arithmetic.- The Syntax of SubC.- The Semantics of SubC.- Polyhedral Analysis of Finite Integers.- Revisiting the Domain of Convex Polyhedra.- Implicit Wrapping of Polyhedral Variables.- Explicit Wrapping of Polyhedral Variables.- Wrapping Variables with a Finite Range.- Wrapping Variables with Infinite Ranges.- Wrapping Several Variables.- An Algorithm for Explicit Wrapping.- An Abstract Semantics for SubC.- Discussion.- Related Work.- Overlapping Memory Accesses and Pointers .- Memory as a Set of Fields.- Memory Layout for Core C.- Access Trees.- Related Work.- Mixing Values and Pointers.- Abstraction Relation.- Abstract Semantics .- Expressions and Simple Assignments.- Assigning Structures.- Casting, &-Operations and Dynamic Memory.- Discussion and Related Work.- Ensuring Efficiency .- Planar Polyhedra.- Operations on Inequalities.- Entailment on Single Inequalities.- Operations on Sets of Inequalities.- Entailment Checking.- Removing Redundancies.- Convex Hull.- Linear Programming and Planar Polyhedra.- Widening Planar Polyhedra.- The TVPI Abstract Domain .- Principles of the TVPI Domain.- Entailment Check.- Convex Hull.- Projection.- Reduced Product Between Bounds and Inequalities.- Incremental Closure.- Approximating General Inequalities.- Linear Programming in the TVPI Domain.- Widening of TVPI Polyhedra.- Related Work.- The Integral TVPI Domain .- The Merit of Z-Polyhedra.- Improving Precision.- Limiting the Growth of Coefficients.- Harvey's Integral Hull Algorithm.- Calculating Cuts Between Two Inequalities.- Integer Hull in the Reduced Product Domain.- Planar Z-Polyhedra and Closure.-Possible Implementations of a Z-TVPI Domain.- Tightening Bpunds Across Projections.- Discussion and Implementation.- Related Work.- Interfacing Analysis and Numeric Domain .- Separating Interval from Relational Information.- Inferring Relevant Fields and Addresses.- Typed Abstract Variables.- Populating the Field Map.- Applying Widening in Fixpoint Calculations.- Improving Precision .- Tracking String Lengths .- Manipulating Implicitly Terminated Strings.- Analysing the String Loop.- Calculating a Fixpoint of the Loop.- Prerequisites for String Buffer Analysis.- Incorporating String Buffer Analysis.- Extending the Abstraction Relation.- Related Work.- Widening with Landmarks .- An Introduction to Widening/Narrowing.- The Limitations of Narrowing.- Improving Widening and Removing Narrowing.- Revisiting the Analysis of String Buffers.- Applying the Widening/Narrowing Approach.- The Rationale Behind Landmarks.- Creating Landmarks for Widening.- Using Landmarks in Widening.- Acquiring Landmarks.- Using Landmarks at a Widening Point.- Extrapolation Operator for Polyhedra.- Related Work.- Combining Points-To and Numeric Analysis .- Boolean Flags in the Numeric Domain.- Incoporating Noolean Flags into Points-To Sets.- Practical Implementation.- Implementation .- Technical Overview at the Anlyser.- Calculating Fixpoints.- Scheduling of Code without Loops.- Scheduling in the Presence of Loops.- Related Work.- Limitations of Strin