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.

We present a new approach to program testing which enables the programmer to specify test suites in terms of a versatile query language. Our query language subsumes standard coverage criteria ranging from simple basic block coverage all the way to predicate complete coverage and multiple condition coverage, but also facilitates on-the-fly requests for test suites specific to the code structure, to external requirements, or to ad hoc needs arising in program understanding/exploration. The query language is supported by a model checking backend which employs the CBMC framework. Our main algorithmic contribution is a method called iterative constraint strengthening which enables us to solve a query for an arbitrary coverage criterion by a single call to the model checker and a novel form of incremental SAT solving: Whenever the SAT solver finds a solution, our algorithm compares this solution against the coverage criterion, and strengthens the clause database with additional clauses which exclude redundant new solutions. We demonstrate the scalability of our approach and its ability to compute compact test suites with experiments involving device drivers, automotive controllers, and open source projects. © 2009 Springer Berlin Heidelberg.

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.