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, 2009
Datum 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 Paderborn
Dr. Mathias Fischer, Universität Paderborn
II
Abstract
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 afford 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 different 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 Datenflussergebnissen 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 verschiedene
Softwaremodule 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 offered 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.
Loading more pages...