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

Sujets

• Wissenschaft

Informations

• Publié par: universitat_paderborn
• Publié le: 01 janvier 2010
• Nombre de lectures: 44
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

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 an