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

Preface

Target Audience

Acknowledgments

Contents

Contributions

List of Figures

1 Introduction

1.1 Technical Background

1.2 Value-Range Analysis

1.3 Analysing C

1.4 Soundness

1.5 Efficiency

1.6 Completeness

1.7 Related Tools

2 A Semantics for C

2.1 Core C

2.2 Preliminaries

2.3 The Environment

2.4 Concrete Semantics

2.5 Collecting Semantics

2.6 Related Work

Abstracting Soundly

3 Abstract State Space

3.1 An Introductory Example

3.2 Points-to Analysis

3.3 Numeric Domains

4 Taming Casting and Wrapping

4.1 Modelling the Wrapping of Integers

4.2 A Language Featuring Finite Integer Arithmetic

4.3 Polyhedral Analysis of Finite Integers

4.4 Implicit Wrapping of Polyhedral Variables

4.5 Explicit Wrapping of Polyhedral Variables

4.6 An Abstract Semantics for Sub C

4.7 Discussion

5 Overlapping Memory Accesses and Pointers

5.1 Memory as a Set of Fields

5.2 Access Trees

5.3 Mixing Values and Pointers

5.4 Relating Concrete and Abstract Domains

6 Abstract Semantics

6.1 Expressions and Simple Assignments

6.2 Assigning Structures

6.3 Casting, &-Operations, and Dynamic Memory

6.4 Inferring Fields Automatically

Ensuring Efficiency

7 Planar Polyhedra

7.1 Operations on Inequalities

7.2 Operations on Sets of Inequalities

8 The TVPI Abstract Domain

8.1 Principles of the TVPI Domain

8.2 Reduced Product between Bounds and Inequalities

8.3 Related Work

9 The Integral TVPI Domain

9.1 The Merit of Z-Polyhedra

9.2 Harvey’s Integral Hull Algorithm

9.3 Planar Z-Polyhedra and Closure

9.4 Related Work

10 Interfacing Analysis and Numeric Domain

10.1 Separating Interval from Relational Information

10.2 Inferring Relevant Fields and Addresses

10.3 Applying Widening in Fixpoint Calculations

Improving Precision

11 Tracking String Lengths

11.1 Manipulating Implicitly Terminated Strings

11.2 Incorporating String Buffer Analysis

11.3 Related Work

12 Widening with Landmarks

12.1 An Introduction to Widening/Narrowing

12.2 Revisiting the Analysis of String Buffers

12.3 Acquiring Landmarks

12.4 Using Landmarks at a Widening Point

12.5 Extrapolation Operator for Polyhedra

12.6 Related Work

13 Combining Points-to and Numeric Analyses

13.1 Boolean Flags in the Numeric Domain

13.2 Incorporating Boolean Flags into Points-to Sets

13.3 Practical Implementation

14 Implementation

14.1 Technical Overview of the Analyser

14.2 Managing Abstract Domains

14.3 Calculating Fixpoints

14.4 Limitations of the String Buffer Analysis

14.5 Proposed Future Refinements

15 Conclusion and Outlook

Conclusion

Outlook

A Core C Example

References

Index