Compositional and Scheduler-Independent Information Flow Security

Sudbrock, Henning (2013)
Compositional and Scheduler-Independent Information Flow Security.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

URL / URN: http://tuprints.ulb.tu-darmstadt.de/3884

Kurzbeschreibung (Abstract)

Software pervades our society deeper with every year. This trend makes software security more and more important. For instance, software systems running critical infrastructures like power plants must withstand criminal or even terrorist attacks, but also smartphone apps used by consumers in their daily routine are usually expected to operate securely.

In particular, before entrusting a program with confidential information (such as, e.g., image or audio data recorded by a smartphone), one wants to be sure that the program is trustworthy and does not leak the secrets to untrusted sinks (such as, e.g., an untrusted server on the Internet). Information flow properties characterize such confidentiality requirements by restricting the flow of confidential information, and an information flow analysis permits to check that a program respects those restrictions.

The problem of information flow in multi-threaded programs is particularly challenging, because information flows can originate in subtle ways from the interplay between threads. Moreover, the existence of such information flows depends on the scheduler, which might not even be known when analyzing a program. To obtain high assurance that no leak is overlooked in an information flow analysis, formally well-founded analyses provide a rigorous solution. Such analyses are proven sound with respect to formal information flow properties that specify precisely what restrictions on information flow mean.

In this thesis, we develop two novel information flow properties for multi-threaded programs, FSI-security and SIFUM-security. These properties are scheduler-independent, i.e., they characterize secure information flow for different schedulers simultaneously. Moreover, they are compositional, i.e., they permit to break down the analysis of a multi-threaded program to single threads. For both properties we develop a security analysis based on a security type system that is proven sound with respect to the property.

Compared to existing scheduler-independent information flow properties, FSI-security is less restrictive. In particular, FSI-security is the first scheduler-independent information flow property that permits programs with nondeterministic behavior and programs whose control flow depends on secrets. The security analysis based on SIFUM-security is the first provably sound flow-sensitive information flow analysis for multi-threaded programs in the form of a security type system. Flow-sensitivity results in increased analysis precision by taking the order of program statements into account. The key in our development of SIFUM-security and the corresponding flow-sensitive analysis for multi-threaded programs was to adopt assumption-guarantee style reasoning to information flow security.

We integrate FSI-security and SIFUM-security into the novel property FSIFUM-security, and we integrate the security analyses for FSI- and SIFUM-security into a security analysis for FSIFUM-security. Thereby, FSIFUM-security and the corresponding analysis inherit the advantages of both FSI- and SIFUM-security.

In addition to developing novel type-based information flow analyses we also explore information flow analysis for multi-threaded programs with program dependence graphs (PDGs) which is used successfully to analyze sequential programs. To this end, we develop a formal connection between PDG-based and type-based information flow analysis for sequential programs. We exploit the connection to transfer concepts from our type-based analysis for multi-threaded programs to PDGs, resulting in a provably sound PDG-based information flow analysis for multi-threaded programs. Beyond this, we also use the connection to transfer concepts from PDGs to type systems and to precisely compare the precision of a type-based and a PDG-based information flow analysis.

Our results provide foundations for more precise and more widely applicable information flow analysis for multi-threaded programs, and we hope that they contribute to a more wide-spread certification of information flow security for concurrent programs.

Typ des Eintrags:

Dissertation

Erschienen:

2013

Autor(en):

Sudbrock, Henning

Art des Eintrags:

Erstveröffentlichung

Titel:

Compositional and Scheduler-Independent Information Flow Security

Sprache:

Englisch

Referenten:

Mantel, Prof. Dr. Heiko ; Schmitt, Prof. Dr. Peter H.

Publikationsjahr:

24 März 2013

Datum der mündlichen Prüfung:

12 Juni 2013

URL / URN:

http://tuprints.ulb.tu-darmstadt.de/3884

Kurzbeschreibung (Abstract):

Alternatives oder übersetztes Abstract:

Alternatives Abstract

Sprache

Software durchdringt unsere Gesellschaft immer tiefer. Dadurch wird Softwaresicherheit immer wichtiger. Beispielsweise müssen Softwaresysteme in kritischen Infrastrukturen kriminellen oder gar terroristischen Attacken standhalten, aber auch von Smartphone-Apps wird ein bestimmtes Sicherheitsniveau erwartet.

Bevor man einem Programm vertrauliche Informationen wie beispielsweise Telefonats-Daten anvertraut möchte man insbesondere sicher sein, dass das Programm die Geheimnisse nicht ungefragt an Dritte beispielsweise im Internet weitergibt. Informationsflusseigenschaften beschreiben solche Vertraulichkeitsanforderungen, indem sie den Fluss vertraulicher Informationen einschränken. Informationsflussanalysen ermöglichen die Überprüfung von Programmen bezüglich dieser Einschränkungen.

Die Informationsflussanalyse nebenläufiger Programme ist besonders schwierig, da durch das Zusammenspiel nebenläufiger Programmteile auf subtile Art und Weise Informationsflüsse entstehen können. Darüber hinaus hängt die Existenz solcher Flüsse vom Scheduler ab, der bei der Analyse möglicherweise unbekannt ist. Um Gewissheit zu erlangen, dass kein Fluss übersehen wird, bieten formal fundierte Analysen eine rigorose Lösung. Solche Analysen garantieren beweisbar sicher, dass Programme einer formalen Informationsflusseigenschaft genügen welche Informationsfluss präzise spezifiziert.

In dieser Arbeit entwickeln wir zwei neue Informationsflusseigenschaften für nebenläufige Programme, FSI-Security und SIFUM-Security. Diese Eigenschaften sind scheduler-unabhängig, d.h., sie beschreiben Informationsflusssicherheit für verschiedene Scheduler gleichzeitig. Außerdem sind sie kompositional, d.h., sie erlauben es, die Analyse eines Programms auf kleinere Teilprogramme herunterzubrechen. Für beide Eigenschaften entwickeln wir eine Sicherheitsanalyse basierend auf einem Sicherheitstypsystem und beweisen die Korrektheit der Analyse gegenüber der jeweiligen Sicherheitseigenschaft.

FSI-Security ist die erste scheduler-unabhängige Informationsflusseigenschaft die nicht-deterministische Programme sowie Programme mit geheimen Kontrollbedingungen erlaubt. Die Analyse für SIFUM-Security ist die erste beweisbar sichere flusssensitive Informationsflussanalyse für nebenläufige Programme in Form eines Sicherheitstypsystems. Flusssensitivität ermöglicht höhere Präzision indem die Reihenfolge von Programmanweisungen berücksichtigt wird. Der Schlüssel für die Entwicklung von SIFUM-Security war die Verwendung von 'Annahmen und Garantien' ('assumptions and guarantees').

Wir integrieren FSI-Security und SIFUM-Security zur neuen Eigenschaft FSIFUM-Security, und wir integrieren die Sicherheitsanalysen für FSI-Security und SIFUM-Security zu einer Sicherheitsanalyse für FSIFUM-Security. Dadurch erben FSIFUM-Security und die zugehörige Analyse die Vorteile von sowohl FSI- als auch SIFUM-Security.

Neben der Entwicklung typ-basierter Analysen betrachten wir auch Analysen für nebenläufige Programme mittels Programmabhängigkeitsgraphen (PDGs), die erfolgreich zur Analyse sequentieller Programme eingesetzt werden. Wir entwickeln eine formale Verbindung zwischen PDG-basierter und typ-basierter Informationsflussanalyse für sequentielle Programme. Darauf basierend überführen wir Konzepte der typ-basierten Analysen für nebenläufige Programme in die Welt der PDGs, was in einer beweisbar korrekten PDG-basierten Informationsflussanalyse für nebenläufige Programme resultiert. Wir nutzen die Verbindung auch, um Konzepte von PDGs in einer typ-basierten Analyse zu verwenden, und um die Präzision einer typ- und einer PDG-basierten Analyse präzise zu vergleichen.

Unsere Resultate bieten die formalen Grundlagen für präzisere und weitreichender einsetzbare Informationsflussanalysen für nebenläufige Programme. Wir hoffen, damit zu einer weiter verbreiteten Zertifizierung von Informationsflusssicherheit nebenläufiger Programme beizutragen.

Deutsch

Freie Schlagworte:

information flow security, compositionality, scheduler-independence, security type system, language-based security, program dependence graph

URN:

urn:nbn:de:tuda-tuprints-38843

Sachgruppe der Dewey Dezimalklassifikatin (DDC):

000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik

Fachbereich(e)/-gebiet(e):

20 Fachbereich Informatik > Modellierung und Analyse von Informationssystemen (MAIS)
20 Fachbereich Informatik

Hinterlegungsdatum:

11 Mai 2014 19:55

Letzte Änderung: