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

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Simon, Axel (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: London : Springer London, 2008.
• Θέματα: Computer science.; Software engineering.; Programming languages (Electronic computers).; Computer logic.; Numerical analysis.; Computer Science.; Programming Languages, Compilers, Interpreters.; Logics and Meanings of Programs.; Software Engineering.; Numeric Computing.

The use of static analysis techniques to prove the partial correctness of C code has recently attracted much attention due to the high cost of software errors - particularly with respect to security vulnerabilities. However, research into new analysis techniques is often hampered by the technical di...

Πίνακας περιεχομένων:

• 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.