Value-Range Analysis of C Programs
Based on the analysis of a standard mail-forwarding program, necessary refinements of the basic analysis are examined, thereby paving the way for an analysis that is precise enough to prove the absence of buffer overflows in legacy C code.
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
- Autor: Axel Simon
- 2008, 302 Seiten, Maße: 16,5 x 24,3 cm, Gebunden, Englisch
- Verlag: Springer, London
- ISBN-10: 1848000162
- ISBN-13: 9781848000162
From the reviews:
Zustand | Preis | Porto | Zahlung | Verkäufer | Rating |
---|
Schreiben Sie einen Kommentar zu "Value-Range Analysis of C Programs".
Kommentar verfassen