Search

Das Gebiet der Informationsflusskontrolle beschaeftigt sich mit dem Problem sicherzustellen, dass ein Programm das vertrauliche Daten verarbeitet keine Informationen ueber diese Daten an nicht vertrauenswuerdige Kanaele preisgibt. Diese Arbeit praesentiert einen Ansatz zur statischen Informationsflusskontrolle, der es ermoeglicht die Praezision moderner Programmanalysen, die auf die Verifikation von Erreichbarkeitseigenschaften spezialisiert sind, zur Verifikation von Informationsflusssicherheit zu nutzen. Der Ansatz basiert auf einer Charakterisierung von Paaren von Ausfuehrungen eines gegebenen Programms, die eine Informationsflusssicherheitseigenschaft verletzten. Aus dieser Charakterisierung werden approximierende Erreichbarkeitseigenschaften abgeleitet, welche die Informationsflusssicherheit des Programms implizieren und mit Hilfe existierender Programmanalysen verifiziert werden koennen. Die Korrektheit des Ansatzes wird formal bewiesen und an mehreren Anwendungen illustriert., Information flow control is concerned with ensuring that a program which receives confidential input does not leak information about this input to untrusted channels. We present a novel approach for static information flow control that can harness the power of modern safety analyses. The approach is based on a characterisation of pairs of executions which break a security property. From the characterisation approximating safety properties are derived which ensure the security of the program. The development utilises a simple yet versatile program model that is not limited to finite control or data and targets a semantic security property which is termination insensitive but still gives some guarantees for non-terminating executions by allowing for observations throughout the execution of a program. We provide rigorous soundness proofs that have also been machine checked and describe multiple instantiations of the approach including a fixed point-based approach targeting abstract interpretation-like safety analyses and a regular approximation that is the basis for a prototypical implementation., 1 Introduction 1 2 Related Work 5 3 Preliminaries 9 4 Program Model and Security Property 13 4.1 Security Property . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.2 Program Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.3 Command Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 5 Characterisation of Information Flows 27 6 Correctness 47 6.1 Properties of Paths . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6.2 Insecurity Contradicts . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 6.3 Contradictions are Critical . . . . . . . . . . . . . . . . . . . . . . . . . . 66 6.4 Critical Reaching Executions . . . . . . . . . . . . . . . . . . . . . . . . 71 7 Applications for Information Flow Control 73 7.1 Relation to Program Dependence Graphs . . . . . . . . . . . . . . . . . 74 7.2 Fixed Point Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 7.2.1 Top Level Information Flow Abstraction . . . . . . . . . . . . . . 77 7.2.2 Abstract Location Based Instantiation . . . . . . . . . . . . . . . 79 7.2.3 Optimising the Instantiation for Efficiency . . . . . . . . . . . . . 89 7.3 Regular Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 7.3.1 Information Flow Automaton . . . . . . . . . . . . . . . . . . . . 96 7.3.2 Precision Compared to the PDG . . . . . . . . . . . . . . . . . . 100 7.3.3 Security Program . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 7.3.4 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 8 Conclusion 109 Bibliography 113

"Lock sensitive analysis of parallel programs" (Lock-Sensitive Analyse nebenläufiger Programme) Diese Dissertation behandelt einen Modellprüfungsalgorithmus für dynamische Pushdown-Netzwerke mit Monitoren (Monitor-DPNs). Monitor-DPNs sind ein Modell für parallele Programme mit rekursiven Prozeduren, Thread-Erzeugung, und wechselweisem Ausschluss durch Monitore. Betrachtet werden Vorgängermengenberechnungen, mit denen man viele interessante Eigenschaften ausdrücken kann, unter Anderem Race-Conditions, Bitvektoranalysen und das (EF,EX)-Fragment der branching-time Logik CTL.