English

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", 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.

Deutsch

Diese Arbeit beschreibt einen allgemeinen Ansatz zur Validierung von

interprozeduralen 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, 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 Analyseergebnissen 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

Analyseergebnisse sicher, aber der Codeerzeuger kann die komplexe

Analyse auf einer leistungsfähigeren Maschine durchführen.

Der wesentliche Beitrag dieser Arbeit ist die Erweiterung des

Validierungsansatzes 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.