Suchen und Finden
Mehr zum Inhalt
Value-Range Analysis of C Programs - Towards Proving the Absence of Buffer Overflow Vulnerabilities
Preface
6
Target Audience
7
Acknowledgments
8
Contents
9
Contributions
14
List of Figures
16
1 Introduction
20
1.1 Technical Background
21
1.2 Value-Range Analysis
23
1.3 Analysing C
25
1.4 Soundness
26
1.5 Efficiency
30
1.6 Completeness
34
1.7 Related Tools
37
2 A Semantics for C
41
2.1 Core C
41
2.2 Preliminaries
46
2.3 The Environment
46
2.4 Concrete Semantics
50
2.5 Collecting Semantics
55
2.6 Related Work
60
Abstracting Soundly
62
3 Abstract State Space
63
3.1 An Introductory Example
64
3.2 Points-to Analysis
67
3.3 Numeric Domains
72
4 Taming Casting and Wrapping
87
4.1 Modelling the Wrapping of Integers
88
4.2 A Language Featuring Finite Integer Arithmetic
90
4.3 Polyhedral Analysis of Finite Integers
92
4.4 Implicit Wrapping of Polyhedral Variables
93
4.5 Explicit Wrapping of Polyhedral Variables
94
4.6 An Abstract Semantics for Sub C
99
4.7 Discussion
102
5 Overlapping Memory Accesses and Pointers
104
5.1 Memory as a Set of Fields
104
5.2 Access Trees
108
5.3 Mixing Values and Pointers
115
5.4 Relating Concrete and Abstract Domains
121
6 Abstract Semantics
126
6.1 Expressions and Simple Assignments
131
6.2 Assigning Structures
133
6.3 Casting, &-Operations, and Dynamic Memory
136
6.4 Inferring Fields Automatically
138
Ensuring Efficiency
140
7 Planar Polyhedra
141
7.1 Operations on Inequalities
143
7.2 Operations on Sets of Inequalities
145
8 The TVPI Abstract Domain
161
8.1 Principles of the TVPI Domain
162
8.2 Reduced Product between Bounds and Inequalities
166
8.3 Related Work
177
9 The Integral TVPI Domain
178
9.1 The Merit of Z-Polyhedra
179
9.2 Harvey’s Integral Hull Algorithm
181
9.3 Planar Z-Polyhedra and Closure
190
9.4 Related Work
195
10 Interfacing Analysis and Numeric Domain
197
10.1 Separating Interval from Relational Information
197
10.2 Inferring Relevant Fields and Addresses
199
10.3 Applying Widening in Fixpoint Calculations
204
Improving Precision
207
11 Tracking String Lengths
208
11.1 Manipulating Implicitly Terminated Strings
209
11.2 Incorporating String Buffer Analysis
220
11.3 Related Work
224
12 Widening with Landmarks
227
12.1 An Introduction to Widening/Narrowing
227
12.2 Revisiting the Analysis of String Buffers
230
12.3 Acquiring Landmarks
236
12.4 Using Landmarks at a Widening Point
237
12.5 Extrapolation Operator for Polyhedra
239
12.6 Related Work
241
13 Combining Points-to and Numeric Analyses
244
13.1 Boolean Flags in the Numeric Domain
246
13.2 Incorporating Boolean Flags into Points-to Sets
250
13.3 Practical Implementation
259
14 Implementation
268
14.1 Technical Overview of the Analyser
269
14.2 Managing Abstract Domains
271
14.3 Calculating Fixpoints
273
14.4 Limitations of the String Buffer Analysis
280
14.5 Proposed Future Refinements
285
15 Conclusion and Outlook
286
Conclusion
286
Outlook
287
A Core C Example
289
References
292
Index
304
Alle Preise verstehen sich inklusive der gesetzlichen MwSt.