Timing Sensitive Dependency Analysis and its Application to Software Security

Ich präsentiere neue Verfahren zur statischen Analyse von
Ausführungszeit-sensitiver Informationsflusskontrolle in Softwaresystemen.
Ich wende diese Verfahren an zur Analyse nebenläufiger Java
Programme, sowie zur Analyse von Ausführungszeit-Seitenkanälen in
Implementierungen kryptographischer Primitive.

Methoden der Informationsflusskontrolle zielen darauf ab, Fluss von
Informationen (z.B.: zwischen verschiedenen externen Schnittstellen
einer Software-Komponente) anhand expliziter Richtlinien einzuschränken.
Solche Methoden können daher zur Einhaltung sowohl
... mehr
von Vertraulichkeit als auch Integrität eingesetzt werden. Der Ziel korrekter
statischer Programmanalysen in diesem Umfeld ist der Nachweis,
dass in allen Ausführungen eines gegebenen Programms die zugehörigen
Richtlinien eingehalten werden. Ein solcher Nachweis erfordert
ein Sicherheitskriterium, welches formalisiert, unter welchen
Bedingungen dies der Fall ist.

Jedem formalen Sicherheitskriterium entspricht implizit ein
Programm- und Angreifermodell. Einfachste Nichtinterferenz-Kriterien
beschreiben beispielsweise nur nicht-interaktive Programme. Dies
sind Programme die nur bei Beginn und Ende der Ausführung Ein- und
Ausgaben erlauben. Im zugehörigen Angreifer-Modell kennt der
Angreifer das Programm, aber beobachtet nur bestimmte (öffentliche)
Aus- und Eingaben oder stellt diese bereit. Ein Programm ist nichtinterferent,
wenn der Angreifer aus seinen Beobachtungen keinerlei
Rückschlüsse auf geheime Aus- und Eingaben terminierender Ausführungen
machen kann. Aus nicht-terminierenden Ausführungen
hingegen sind dem Angreifer in diesem Modell Schlussfolgerungen
auf geheime Eingaben erlaubt.

Seitenkanäle entstehen, wenn einem Angreifer aus Beobachtungen realer
Systeme Rückschlüsse auf vertrauliche Informationen ziehen kann,
welche im formalen Modell unmöglich sind. Typische Seitenkanäle
(also: in vielen formalen Sicherheitskriterien unmodelliert) sind neben
Nichttermination beispielsweise auch Energieverbrauch und die Ausführungszeit
von Programmen. Hängt diese von geheimen Eingaben
ab, so kann ein Angreifer aus der beobachteten Ausführungszeit auf
die Eingabe (z.B.: auf den Wert einzelner geheimer Parameter) schließen.
In meiner Dissertation präsentiere ich neue Abhängigkeitsanalysen,
die auch Nichtterminations- und Ausführungszeitkanäle berücksichtigen.
In Hinblick auf Nichtterminationskanäle stelle ich neue Verfahren
zur Berechnung von Programm-Abhängigkeiten vor. Hierzu entwickle
ich ein vereinheitlichendes Rahmenwerk, in welchem sowohl
Nichttermination-sensitive als auch Nichttermination-insensitive Abhängigkeiten
aus zueinander dualen Postdominanz-Begriffen resultieren.
Für Ausführungszeitkanäle entwickle ich neue Abhängigkeitsbegriffe
und dazugehörige Verfahren zu deren Berechnung. In zwei Anwendungen
untermauere ich die These:

Ausführungszeit-sensitive Abhängigkeiten ermöglichen korrekte statische
Informationsfluss-Analyse unter Berücksichtigung von Ausführungszeitkanälen.

Basierend auf Ausführungszeit-sensitiven Abhängigkeiten entwerfe
ich hierfür neue Analysen für nebenläufige Programme.
Ausführungszeit-sensitive Abhängigkeiten sind dort selbst für
Ausführungszeit-insensitive Angreifermodelle relevant, da dort interne
Ausführungszeitkanäle zwischen unterschiedlichen Ausführungsfäden
extern beobachtbar sein können. Meine Implementierung für
nebenläufige Java Programme basiert auf auf dem Programmanalyse-
System JOANA.

Außerdem präsentiere ich neue Analysen für Ausführungszeitkanäle
aufgrund mikro-architektureller Abhängigkeiten. Exemplarisch untersuche
ich Implementierungen von AES256 Blockverschlüsselung. Bei einigen
Implementierungen führen Daten-Caches dazu, dass die Ausführungszeit
abhängt von Schlüssel und Geheimtext, wodurch diese
aus der Ausführungszeit inferierbar sind. Für andere Implementierungen
weist meine automatische statische Analyse (unter Annahme
einer einfachen konkreten Cache-Mikroarchitektur) die Abwesenheit
solcher Kanäle nach.

I present new methods for the static analysis of timing sensitive information
flow control in software systems. I apply these methods in the
analysis of concurrent Java programs, as well as the analysis of timing
side-channels in implementations of cryptographic primitives.

Methods for information flow control aim to control the flow of information
(e.g.: between different external interfaces of a software
component) with respect to explicit flow policies. Such methods can
protect confidentiality as well as integrity of information. In this setting,
the goal of sound static program analysis is to proof that in all
... mehr
executions of a given program, a corresponding flow policy is respected.
Such a proof requires a security criterion which formalizes
under which condition this is indeed the case.

Every formal security criterion implicitly corresponds to a program
and attacker model. Simple non-interference criteria, for example, apply
only to non-interactive programs. These are programs which allow
input and output only at the beginning and the end of the execution.
In the corresponding attacker model, the attacker does know the
program, but observes only certain (public) output and input, or provides
those. A program is non-interferent if from these observations
the attacker cannot infer any properties of secret input and output
of terminating executions. From non-terminating executions in this
model, the attacker is allowed to infer properties of secret input.

Side channels occur if an attacker can infer properties of secret information
from observations of real systems which are impossible to
infer in the formal model. Typical side channels include (i.e., typically
unmodeled are): nontermination as well as energy consumption and timing
channels: By observing the program’s execution time, the attacker
(partially or completely) infers the program’s secret input on
which the execution time depends.

In my dissertation I present new dependency analysis sensitive to both
nontermination and timing channels. With respect to nontermination,
I introduce new methods for the computation of control dependencies.
For this purpose, I develop a generalized framework in which
nontermination-sensitive as well as nontermination-insensitive control
dependencies result from (mutually dual) postdominance notions. For
timing channels, I develop new notions of control dependencies, and
corresponding methods for their computation. In two applications, I
substantiate my thesis:

Timing sensitive control dependencies facilitate sound static information flow
control in the presence of timing channels.

For this purpose, I develop new analysis for concurrent programs,
based on timing sensitive control dependencies. In this setting, timing
sensitive control dependencies are relevant even for timing insensitive
attacker models, since there internal timing channels between concurrent
threads of execution may become observable externally. My implementation
for concurrent Java programs is based on the JOANA
program analysis framework.

I also present new analysis for timing channels caused by microarchitectural
dependencies. I illustrate these by a study of AES256
block cipher implementations. For some implementations, data caches
cause the execution time to depend on key and plaintext, making them
inferrable from the execution time. For other implementations, my
automatic static analysis proves (assuming a simple concrete cache
micro-architecture) the absence of such timing channels.