La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

Validation of data flow results for program modules [Elektronische Ressource] / vorgelegt von Karsten Klohs

299 pages
Validation of Data Flow Results forProgram ModulesDissertationSchriftliche Arbeit zur Erlangung des akademischen Grades„Doktor der Naturwissenschaften“an der Fakultät für Elektrotechnik, Informatik und Mathematikder Universität Paderbornvorgelegt vonKarsten KlohsPaderborn, 2009Datum der mündlichen Prüfung:03.04.2009Gutachter:Prof. Dr. Uwe Kastens, Universität PaderbornProf. Dr. Jens Knoop, Technische Universität WienPromotionskommision:Prof. Dr. Uwe Kastens, Universität PaderbornProf. Dr. Jens Knoop, Technische Universität WienProf. Dr. Heike Wehrheim, Universität PaderbornProf. Dr. Heiko Platzner, Universität PnDr. Mathias Fischer, Universität PaderbornIIAbstractThis thesis presents a general approach to the validation of interprocedural dataflow results for separated software modules, in order to enable the safe use of dataflow results on devices which cannot aord to run the data flow analysis on theirown. The underlying idea stems from the “Proof-Carrying-Code Principle”[Nec97], which utilises that it is easier to check the correctness of a given solutionof a problem than to solve the problem.The requirement to validate analysis results originally arose for Java BytecodeVerification on Smart Cards.
Voir plus Voir moins

Validation of Data Flow Results for
Program Modules
Dissertation
Schriftliche Arbeit zur Erlangung des akademischen Grades
„Doktor der Naturwissenschaften“
an der Fakultät für Elektrotechnik, Informatik und Mathematik
der Universität Paderborn
vorgelegt von
Karsten Klohs
Paderborn, 2009Datum der mündlichen Prüfung:
03.04.2009
Gutachter:
Prof. Dr. Uwe Kastens, Universität Paderborn
Prof. Dr. Jens Knoop, Technische Universität Wien
Promotionskommision:
Prof. Dr. Uwe Kastens, Universität Paderborn
Prof. Dr. Jens Knoop, Technische Universität Wien
Prof. Dr. Heike Wehrheim, Universität Paderborn
Prof. Dr. Heiko Platzner, Universität Pn
Dr. Mathias Fischer, Universität Paderborn
IIAbstract
This thesis presents a general approach to the validation of interprocedural data
flow results for separated software modules, in order to enable the safe use of data
flow results on devices which cannot aord to run the data flow analysis on their
own. The underlying idea stems from the “Proof-Carrying-Code Principle”
[Nec97], which utilises that it is easier to check the correctness of a given solution
of a problem than to solve the problem.
The requirement to validate analysis results originally arose for Java Bytecode
Verification on Smart Cards. The generalisation of this specific application to the
validation of interprocedural data flow results enables advanced optimisations
or security checks on limited devices in a scenario where the mobile code is
transmitted via an inherently insecure transport media like the Internet. The
validation ensures the correctness of the results but the code producer can
perform the complex analysis on a more powerful machine.
The central contribution of this thesis is the extension of the validation approach
to the interprocedural analyses and to separated software modules. This is vital
in a mobile code scenario where dierent software modules can be dynamically
loaded to the target device and where the potential interactions between the
software modules and the runtime environment have to be considered.
Zusammenfassung
Diese Arbeit beschreibt einen allgemeinen Ansatz zur Validierung von interproze-
duralen Analyseergebnissen für einzelne Softwaremodule, um die sichere Nutzung
von Datenflusser auf Zielplattformen zu ermöglichen, die die Analyse
nicht eigenständig durchführen können. Die zugrunde liegende Idee entstammt
der “Proof-Carrying Code”-Methodik [Nec97], die sich zu Nutze macht, dass
es einfacher ist, die Korrektheit der Lösung eines Problems zu überprüfen als
das eigentliche Problem zu lösen.
Die Notwendigkeit, Datenflussergebnisse zu prüfen, entstand ursprünglich bei
der Java Bytecode Verfikation auf Smard Cards. Die Verallgemeinerung dieses
speziellen Ansatzes auf die Validierung von interprozeduralen Analyseergeb-
nissen ermöglicht erweiterte Optimierungen oder Sicherheitsüberprüfungen in
einem Umfeld in dem mobiler Code über ein unsicheres Transportmedium wie
dem Internet übertragen wird. Die Validierung stellt die Korrektheit der Anal-
yseergebnisse sicher, aber der Codeerzeuger kann die komplexe Analyse auf
einer leistungsfähigeren Maschine durchführen.
Der wesentliche Beitrag dieser Arbeit ist die Erweiterung des Vali-
dierungsansatzes auf interprozedurale Analysen und auf die Analyse einzelner
Softwaremodule. Dies ist entscheidend in einem Umfeld, in dem verschiedeneemodule zur Laufzeit auf eine Zielplattform geladen werden können
und wo die möglichen Wechselwirkungen zwischen Softwaremodulen und der
Laufzeitumgebung berücksichtigt werden müssen..Acknowledgements
First of all, I wish to thank Uwe Kastens, my advisor. His keen sense of
interesting directions of research and his stance on science in general has shaped
this thesis - and me - in many ways. The freedom of research is something
which I learned to appreciate progressively during the years. His comments
on the early versions of this thesis had sometimes been extensive, but always
constructive and helpful.
I am also grateful to Jens Knoop who has oered me the opportunity to discuss
the fundamental concepts of my thesis with a broader audience. I’ll always
remember the hospitality I experienced in Vienna and the admirable precision
with which Jens Knoop is able to pinpoint the challenging parts of a problem.
Additionally, I’d also like to thank my colleagues for many interesting discus-
sions - especially Michael Thies for his remarkable ability to give me the feeling
that at least someone understands nascent ideas even before they have been
fully developed.
However, I am most grateful to my beloved wife Monika - her calm and serene
support kept me grounded even in the stressful phases of the thesis..Contents
1 Introduction 1
1.1 Methodical Contributions . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.3 Road Map . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2 Application Scenarios 11
2.1 Security Policies and Mobile Code . . . . . . . . . . . . . . . . . . 13
2.2 Program Optimisation and Partial Analyses . . . . . . . . . . . . . 14
2.3 Modular Results and Partial Analysis . . . . . . . . . . . . . . . . 15
2.4 Validation of Data Flow Results as an Assisting Technique . . . . 17
3 Foundations 21
3.1 Iterative Data Flow Analysis and Equation Systems . . . . . . . . 21
3.1.1 Elements of Data Flow Problems . . . . . . . . . . . . . . . 21
3.1.2 The Flow Graph Model and Equation Systems . . . . . . . 26
3.1.3 The Iterative Worklist Algorithm . . . . . . . . . . . . . . . 27
3.1.4 Elimination Methods . . . . . . . . . . . . . . . . . . . . . . 29
3.1.5 Advanced Scenarios of Program Analysis . . . . . . . . . . 31
3.2 Model Checking and Abstract Interpretations . . . . . . . . . . . . 32
3.2.1 Model Checking and the Relationship to Program Analysis 33
3.2.2 Validation of Program Analysis Results . . . . . . . . . . . 34
4 Fundamental Validation Principles 37
4.1 Intraprocedural Validation . . . . . . . . . . . . . . . . . . . . . . . 38
4.1.1 The General Validation Principle . . . . . . . . . . . . . . . 38
4.1.2 The Intentional Under-Approximation Principle . . . . . . 42
4.2 Interprocedural Validation . . . . . . . . . . . . . . . . . . . . . . 43
4.2.1 Review of Interprocedural Analysis . . . . . . . . . . . . . 44
4.2.2 Validation of Summary Functions . . . . . . . . . . . . . . 49
4.2.3 Validation of Data Flow Values . . . . . . . . . . . . . . . . 50
4.2.4 Method Invocation Semantics . . . . . . . . . . . . . . . . . 51
4.2.5 The Interprocedural Validation Principle . . . . . . . . . . 55
4.3 Program Modules and Sophisticated Validation Scenarios . . . . . 56
4.3.1 The Safe Lower Bound Principle . . . . . . . . . . . . . . . 57
4.3.2 Incremental Validation . . . . . . . . . . . . . . . . . . . . . 60
4.3.3 Partial Validation . . . . . . . . . . . . . . . . . . . . . . . . 61
4.4 Summary and Comparison . . . . . . . . . . . . . . . . . . . . . . 62
5 A Generic Model for Summary Functions 65
iContents
5.1 Summary Function Definition . . . . . . . . . . . . . . . . . . . . . 68
5.1.1 Summary Functions and Data Flow Expressions . . . . . . 69
5.1.2 Function Operations . . . . . . . . . . . . . . . . . . . . . . 71
5.1.3 Specification of Instruction-Level Summary Functions . . 74
5.1.4 Relationship to IDFS-problems . . . . . . . . . . . . . . . . 76
5.2 Function Application Expressions and Elementary Transfer Func-
tions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
5.2.1 Properties of Function Application Expressions . . . . . . 78
5.2.2 Nesting Depth and Fix-Point Properties . . . . . . . . . . . 80
5.2.3 Relationship to IDE-problems . . . . . . . . . . . . . . . . . 82
5.3 Normalisation and Properties of Summary Functions . . . . . . . 84
5.3.1 Normalisation of Data Flow Expressions . . . . . . . . . . 86
5.3.2 Properties of Data Flow Expressions . . . . . . . . . . . . . 90
5.3.3 Pr of the Summary Function Model . . . . . . . . . 94
5.3.4 Summary Functions and the Inducing Data Flow Problem 97
5.4 Modular Results and Incremental Validation . . . . . . . . . . . . 98
5.4.1 Invocation Contexts and Data Flow Variables . . . . . . . . 100
5.4.2 External Callees and Function Variables . . . . . . . . . . . 103
5.4.3 Intraprocedural Analysis is an Application of the Safe
Lower Bound Principle . . . . . . . . . . . . . . . . . . . . 107
5.4.4 Open Summary Functions and the Incremental Validation
Scenario . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
5.4.5 Properties of Open Summary Functions . . . . . . . . . . . 109
5.4.6 Function Variables in the Expression Model . . . . . . . . . 112
5.5 Method Invocation and Parameter Passing . . . . . . . . . . . . . 115
5.5.1 Local Variables, Parameters, and Global Variables . . . . . 115
5.5.2 Parameter Passing and the Call-Function . . . . . . . . . . 117
5.5.3 Method Return . . . . . . . . . . . . . . . . . . . . . . . . . 118
5.5.4 Properties of Call- and Return-Function . . . . . . . . . . . 120
5.5.5 Related Approaches . . . . . . . . . . . . . . . . . . . . . . 121
5.6 Summary and Comparison . . . . . . . . . . . . . . . . . . . . . . 122
5.6.1 Capabilities of the Summary Function Model . . . . . . . . 123
5.6.2 Limitations of the . . . . . . . . 127
6 Optimisation of the Validation Process 133
6.1 Reduction of the Certificate . . . . . . . . . . . . . . . . . . . . . . 134
6.1.1 The KVM Approach . . . . . . . . . . . . . . . . . . . . . . 135
6.1.2 The Dierence Certificate Approach . . . . . . . . . . . . . 136
6.2 Lifetime of Data Flow Facts in the Validation Process . . . . . . . 139
6.2.1 Dependency Model . . . . . . . . . . . . . . . . . . . . . . . 139
6.2.2 Reuse and Check . . . . . . . . . . . . . . . . . . . . . . . . 141
6.2.3 Optimisation Goals . . . . . . . . . . . . . . . . . . . . . . . 143
6.3 Safe Lower Bounds . . . . . . . . . . . . . . . . . . . . . . . . . . . 146
6.3.1 Lattice Strength Reduction . . . . . . . . . . . . . . . . . . 146
6.3.2 Intentional Under-Approximation and Demand-Driven
Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147
6.4 Reinterpretation in the Interprocedural Scenario . . . . . . . . . . 148
iiContents
6.4.1 Dependencies in the Interprocedural Result . . . . . . . . . 149
6.4.2 Dierence Certificates . . . . . . . . . . . . . . . . . . . . . 150
6.4.3 Intermediate Results . . . . . . . . . . . . . . . . . . . . . . 151
6.4.4 Modular Results and the Dependence Graph . . . . . . . . 152
6.5 Summary and Related Work . . . . . . . . . . . . . . . . . . . . . . 154
7 Validatable Program Analyses 157
7.1 Bit-Vector Analyses and the Power-Set Lattice . . . . . . . . . . . 159
7.1.1 Separable Bit-Vector Analyses: Reaching Definitions . . . 160
7.1.2 Non-Separable Bit-Vector Analyses: Faint Variables . . . . 162
7.2 Constant Propagation . . . . . . . . . . . . . . . . . . . . . . . . . . 164
7.2.1 Arbitrary Lattices: Copy Constant Propagation . . . . . . 165
7.2.2 Elementary Functions: Linear Constant Propagation . . . 166
7.3 Object Oriented Aspects: Type Inference and Call Graph Con-
struction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171
7.3.1 Data Flow Based Type Inference . . . . . . . . . . . . . . . 173
7.3.2 Type Inference and Flow Graph Construction . . . . . . . 181
7.3.3 Validation of Interprocedural Flow Graphs . . . . . . . . . 182
7.3.4 Type Inference for Software Modules . . . . . . . . . . . . 184
7.3.5 Summary and Comparison to Existing Algorithms . . . . 189
8 LUPUS - A Framework for Validatable Data Flow Analysis 193
8.1 System Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . 194
8.2 Implementation of Data Flow Problems . . . . . . . . . . . . . . . 196
8.2.1 Elements of a Data Flow Problem . . . . . . . . . . . . . . 197
8.2.2 Specification of a Concrete Analysis . . . . . . . . . . . . . 198
8.2.3 Flow Graphs and Program Points . . . . . . . . . . . . . . 200
8.2.4 Data Flow Values, Data Flow Expressions and Environments202
8.2.5 Summary Function Implementation . . . . . . . . . . . . . 203
8.3 The Program Analysis Framework . . . . . . . . . . . . . . . . . . 205
8.3.1 Intraprocedural Analysis . . . . . . . . . . . . . . . . . . . 206
8.3.2 Interprocedural . . . . . . . . . . . . . . . . . . . 207
8.3.3 Solution Analysis and Preparation of the Certificate . . . . 208
8.4 LUPULUS - An Ecient and Flexible Validator . . . . . . . . . . 211
8.4.1 Reusable Infrastructure . . . . . . . . . . . . . . . . . . . . 213
8.4.2 Complete Result Validator . . . . . . . . . . . . . . . . . . . 216
8.5 Summary and Comparison to Existing Frameworks . . . . . . . . 217
8.5.1 SOOT and INDUS . . . . . . . . . . . . . . . . . . . . . . . 220
8.5.2 PAG . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 220
8.5.3 SafeTSA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
8.5.4 Code Surfer . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
8.5.5 Abstraction Carrying Code . . . . . . . . . . . . . . . . . . 222
9 Evaluation 223
9.1 Evaluation Setting . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224
9.1.1 Evaluated Analysis . . . . . . . . . . . . . . . . . . . . . . . 225
9.1.2 Analysed Software . . . . . . . . . . . . . . . . . . . . . . . 226
iiiContents
9.2 Evaluation of the Analysis Phase . . . . . . . . . . . . . . . . . . . 229
9.2.1 Intraprocedural Summary Computation . . . . . . . . . . . 231
9.2.2 Interpr . . . . . . . . . . . 240
9.2.3 Invocation Context Computation . . . . . . . . . . . . . . . 245
9.3 Size of the Certificate . . . . . . . . . . . . . . . . . . . . . . . . . . 250
9.3.1 Interprocedural Summary Functions . . . . . . . . . . . . . 250
9.3.2 Size of the Program State . . . . . . . . . . . . . . . . . . . 255
9.4 Evaluation of the Validation Phase . . . . . . . . . . . . . . . . . . 256
9.4.1 Memory Requirements . . . . . . . . . . . . . . . . . . . . . 257
9.4.2 Runtime . . . . . . . . . . . . . . . . . . . . . 258
9.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 263
10 Conclusion 267
10.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267
10.2 Future Directions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 269
A Proofs 275
B Bibliography 282
iv

Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin