Information Flow Control with System Dependence Graphs - Improving Modularity, Scalability and Precision for Object Oriented Languages

Die vorliegende Arbeit befasst sich mit dem Gebiet der statischen Programmanalyse
— insbesondere betrachten wir Analysen, deren Ziel es ist,
bestimmte Sicherheitseigenschaften, wie etwa Integrität und Vertraulichkeit,
für Programme zu garantieren. Hierfür verwenden wir sogenannte
Abhängigkeitsgraphen, welche das potentielle Verhalten des Programms
sowie den Informationsfluss zwischen einzelnen Programmpunkten
abbilden. Mit Hilfe dieser Technik können wir sicherstellen, dass z.B. ein
Programm keinerlei Information über ein geheimes Passwort preisgibt.
Im Speziellen liegt der Fokus dieser Arbeit auf Techniken, die das
... mehr
Erstellen des Abhängigkeitsgraphen verbessern, da dieser die Grundlage
für viele weiterführende Sicherheitsanalysen bildet. Die vorgestellten
Algorithmen und Verbesserungen wurden in unser Analysetool Joana
integriert und als Open-Source öffentlich verfügbar gemacht. Zahlreiche
Kooperationen und Veröffentlichungen belegen, dass die Verbesserungen
an Joana auch in der Forschungspraxis relevant sind.
Diese Arbeit besteht im Wesentlichen aus drei Teilen. Teil 1 befasst sich
mit Verbesserungen bei der Berechnung des Abhängigkeitsgraphen, Teil 2
stellt einen neuen Ansatz zur Analyse von unvollständigen Programmen
vor und Teil 3 zeigt aktuelle Verwendungsmöglichkeiten von Joana an
konkreten Beispielen.
Im ersten Teil gehen wir detailliert auf die Algorithmen zum Erstellen
eines Abhängigkeitsgraphen ein, dabei legen wir besonderes Augenmerk
auf die Probleme und Herausforderung bei der Analyse von Objektorientierten
Sprachen wie Java. So stellen wir z.B. eine Analyse vor,
die den durch Exceptions ausgelösten Kontrollfluss präzise behandeln
kann. Hauptsächlich befassen wir uns mit der Modellierung von
Seiteneffekten, die bei der Kommunikation über Methodengrenzen hinweg
entstehen können. Bei Abhängigkeitsgraphen werden Seiteneffekte, also
Speicherstellen, die von einer Methode gelesen oder verändert werden,
in Form von zusätzlichen Knoten dargestellt. Dabei zeigen wir, dass die
Art und Weise der Darstellung, das sogenannte Parametermodel, enormen
Einfluss sowohl auf die Präzision als auch auf die Laufzeit der gesamten
Analyse hat. Wir erklären die Schwächen des alten Parametermodels,
das auf Objektbäumen basiert, und präsentieren unsere Verbesserungen
in Form eines neuen Modells mit Objektgraphen. Durch das gezielte
Zusammenfassen von redundanten Informationen können wir die Anzahl
der berechneten Parameterknoten deutlich reduzieren und zudem
beschleunigen, ohne dabei die Präzision des resultierenden Abhängigkeitsgraphen
zu verschlechtern. Bereits bei kleineren Programmen im
Bereich von wenigen tausend Codezeilen erreichen wir eine im Schnitt
8-fach bessere Laufzeit — während die Präzision des Ergebnisses in der
Regel verbessert wird. Bei größeren Programmen ist der Unterschied
sogar noch deutlicher, was dazu führt, dass einige unserer Testfälle und
alle von uns getesteten Programme ab einer Größe von 20000 Codezeilen
nur noch mit Objektgraphen berechenbar sind. Dank dieser Verbesserungen
kann Joana mit erhöhter Präzision und bei wesentlich größeren
Programmen eingesetzt werden.
Im zweiten Teil befassen wir uns mit dem Problem, dass bisherige,
auf Abhängigkeitsgraphen basierende Sicherheitsanalysen nur vollständige
Programme analysieren konnten. So war es z.B. unmöglich,
Bibliothekscode ohne Kenntnis aller Verwendungsstellen zu betrachten
oder vorzuverarbeiten. Wir entdeckten bei der bestehenden Analyse
eine Monotonie-Eigenschaft, welche es uns erlaubt, Analyseergebnisse
von Programmteilen auf beliebige Verwendungsstellen zu übertragen.
So lassen sich zum einen Programmteile vorverarbeiten und zum anderen
auch generelle Aussagen über die Sicherheitseigenschaften von
Programmteilen treffen, ohne deren konkrete Verwendungsstellen zu
kennen. Wir definieren die Monotonie-Eigenschaft im Detail und skizzieren
einen Beweis für deren Korrektheit. Darauf aufbauend entwickeln
wir eine Methode zur Vorverarbeitung von Programmteilen, die es uns
ermöglicht, modulare Abhängigkeitsgraphen zu erstellen. Diese Graphen
können zu einem späteren Zeitpunkt der jeweiligen Verwendungsstelle
angepasst werden. Da die präzise Erstellung eines modularen Abhängigkeitsgraphen
sehr aufwendig werden kann, entwickeln wir einen
Algorithmus basierend auf sogenannten Zugriffspfaden, der die Skalierbarkeit
verbessert. Zuletzt skizzieren wir einen Beweis, der zeigt, dass
dieser Algorithmus tatsächlich immer eine konservative Approximation
des modularen Graphen berechnet und deshalb die Ergebnisse darauf
aufbauender Sicherheitsanalysen weiterhin gültig sind.
Im dritten Teil präsentieren wir einige erfolgreiche Anwendungen
von Joana, die im Rahmen einer Kooperation mit Ralf Küsters von der
Universität Trier entstanden sind. Hier erklären wir zum einen, wie
man unser Sicherheitswerkzeug Joana generell verwenden kann. Zum
anderen zeigen wir, wie in Kombination mit weiteren Werkzeugen und
Techniken kryptographische Sicherheit für ein Programm garantiert
werden kann - eine Aufgabe, die bisher für auf Informationsfluss basierende
Analysen nicht möglich war. In diesen Anwendungen wird
insbesondere deutlich, wie die im Rahmen dieser Arbeit vereinfachte
Bedienung die Verwendung von Joana erleichtert und unsere Verbesserungen
der Präzision des Ergebnisses die erfolgreiche Analyse erst
ermöglichen.

This work is concerned with the field of static program analysis — in
particular with analyses aimed to guarantee certain security properties
of programs, like confidentiality and integrity. Our approach uses so called
dependence graphs to capture the program behavior as well as the
information flow between the individual program points. Using this
technique, we can guarantee for example that a program does not reveal
any information about a secret password.
In particular we focus on techniques that improve the dependence
graph computation —the basis for many advanced security analyses.
... mehr
We incorporated the presented algorithms and improvements into our
analysis tool Joana and published its source code as open source. Several
collaborations with other researchers and publications using Joana
demonstrate the relevance of these improvements for practical research.
This work consists essentially of three parts. Part 1 deals with improvements
in the computation of the dependence graph, Part 2 introduces a
new approach to the analysis of incomplete programs and Part 3 shows
current use cases of Joana on concrete examples.
In the first part we describe the algorithms used to compute a dependence
graph, with special attention to the problems and challenges
that arise when analyzing object-oriented languages such as Java. For
example we present an analysis that improves the precision of detected
control flow by incorporating the effects of exceptions. The main improvement
concerns the way side effects —caused by communication
over methods boundaries— are modelled. Dependence graphs capture
side effects —memory locations read or changed by a method— in the
form of additional nodes called parameter nodes. We show that the
structure and computation of these nodes have a huge impact on both
the precision and scalability of the entire analysis. The so-called parameter
model describes the algorithms used to compute these nodes. We explain
the weakness of the old parameter model based on object-trees and present
our improvements in form of a new model using object-graphs. The new
graph structure merges redundant information of multiple nodes into a
single node and thus reduces the number of overall parameter nodes
significantly — which in turn speeds up the analysis without sacrificing
the precision of the resulting dependence graph. These changes are
already visible when analyzing smaller programs with a few thousand
lines of code: We achieve on average a 8 times faster runtime while
the precision of the result remains intact and is usually even enhanced.
The differences are even more pronounced for larger programs. Some of
our test cases and all tested programs larger than 20,000 lines of code
could only be analyzed with the object-graph parameter model. Due to
these enhancements Joana is now able to analyze much larger programs
and also profits from enhanced precision with smaller programs.
In the second part we tackle the problem that security analyses based
on dependence graphs previously required a whole program in order to
compute. For example, it was impossible to preprocess or analyze program
parts like library code without knowledge of the application code using
it. We discovered a monotonicity property in the current analysis that
allows us to reuse analysis results from a program part at a given usage
point to conservatively approximate the expected results at another point
without the need to reanalyze the program part. Due to monotonicity
we are able to make valid statements about the security properties of a
program part in general, without knowledge of its usage points. It also
allows us to preprocess program parts in form of a modular dependence
graph in a way that can be adjusted later on to a concrete usage point.
We define the monotonicity property in detail and outline a proof of
its correctness. Based on this observation, we develop an approach to
preprocess program parts with modular dependence graphs. As the
precise computation of modular dependence graphs can become very
costly, we developed an algorithm based on so-called access paths to
improve scalability. Finally, we sketch a proof showing the presented
algorithm in fact always computes a conservative approximation of
the modular graph and therefore any security analysis performed on a
modular graph remains sound.
The third part contains successful applications of Joana. We present
the results of a cooperation with Ralf Küsters from the University of
Trier. We explain how our security tool Joana is used in general and also
how —in combination with other security tools and techniques— we
were able to proof cryptographic security properties for Java programs
—a task previously not possible for tools based purely on information
flow control. These applications show how the usability improvements
of Joana —developed in the context of this work— considerably reduce
the effort required to setup the analysis. We also explain how our
precision enhancements were crucial for the successful analysis of these
applications.