Search

There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a program graph rather than in terms of its unfoldings is a useful strategy for making analyses more tractable. This paper presents a characterisation of behavioural program properties through sets of structural properties by means of a translation. The characterisation is given in the context of a program model based on control flow graphs of sequential programs with possibly recursive procedures, and properties expressed in a fragment of the modal \mu-calculus with boxes and greatest fixed-points only. The property translation is based on a tableau construction that conceptually amounts to symbolic execution of the behavioural formula, collecting structural constraints along the way. By keeping track of the subformulae that have been examined, recursion in the structural constraints can be identified and captured by fixed-point formulae. The tableau construction terminates, and the characterisation is exact, i.e., the translation is sound and complete. A prototype implementation has been developed. We discuss several applications of the characterisation, in particular compositional verification for behavioural properties, based on maximal models.

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