Apress NBA

Value-Range Analysis of C Programs

Towards Proving the Absence of Buffer Overflow Vulnerabilities

By Axel Simon

  • eBook Price: $119.00
Buy eBook Buy Print Book

Value-Range Analysis of C Programs Cover Image

Value-Range Analysis of C Programs describes a static analysis for detecting buffer overflows. While the book focuses on a sound analysis of C, it will be useful to researchers and students interested in static analysis of real-world programming languages.

Full Description

  • Add to Wishlist
  • ISBN13: 978-1-8480-0016-2
  • 324 Pages
  • User Level: Science
  • Publication Date: March 10, 2010
  • Available eBook Formats: PDF
Full Description
Value-Range Analysis of C Programs describes a static analysis for detecting buffer overflows. A buffer overflow in a C program occurs when input is read into a memory buffer whose length exceeds that of the buffer. Overflows usually lead to crashes and may even enable a malicious person to gain control over a computer system. They are recognised as one of the most widespread forms of computer vulnerability. 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.
Table of Contents

Table of Contents

  1. From the Contents: Preface.
  2. Introduction.
  3. Value Range Analysis.
  4. Analysing C.
  5. A Semantics for C.
  6. Core C.
  7. Related Work.
  8. Part 1 Abstracting Soundly.
  9. Abstract State Space.
  10. Points
  11. To Analysis.
  12. Numeric Domains.
  13. Taming Casting and Wrapping.
  14. A Language Featuring Finite Integer Arithmetic.
  15. Implicit Wrapping of Polyhedral Variables.
  16. Explicit Wrapping of Polyhedral Variables.
  17. An Abstract Semantics for SubC.
  18. Discussion.
  19. Overlapping Memory Accesses and Pointers.
  20. Memory as a Set of Fields.
  21. Mixing Values and Pointers.
  22. Abstraction Relation.
  23. Abstract Semantics.
  24. Part II Ensuring Efficiency.
  25. Planar Polyhedra.
  26. Operations on Inequalities.
  27. Operations on Sets of Inequalities.
  28. The TVPI Abstract Domain.
  29. The Integral TVPI Domain.
  30. Interfacing Analysis and Numeric Domain.
  31. Inferring Relevant Fields and Addresses.
  32. Applying Widening in Fixpoint Calculations.
  33. Part III Improving Precision.
  34. Tracking String Lengths.
  35. Widening with Landmarks .
  36. Combining Points
  37. To and Numeric Analysis.
  38. Conclusion and Outlook

If you think that you've found an error in this book, please let us know by emailing to editorial@apress.com . You will find any confirmed erratum below, so you can check if your concern has already been addressed.
No errata are currently published


    1. Formal Techniques for Safety-Critical Systems


      View Book