Who we are

This is a joint project between Technische Universität München and the Max-Planck-Institut für Informatik Saarbrücken. The project is part a larger family: the DFG priority program Reliably Secure Software Systems (RS3). The main participants in the project are:

What we do

We design formal reasoning methods and tools for the verification of information-flow security, including language-based and system security. We are concerned with both fundamental research and the practical realization of our results.

Language-based security

We focus on a while-language with parallel composition, for which we formalize and systematize security type systems proposed in the literature over the years, known under the umbrella term ''Volpano-Smith systems''. Such systems provide syntactic conditions ensuring that programs satisfy one or another variant of noninterference: information does not leak from confidential sources (e.g., designated variables or inputs to the program) to public sinks (e.g., other designated variables or outputs of the program).

We show that most of these type systems and their soundness theorems emerge from the interplay and iteration of two simple principles: ordering and compositionality. We also discover optimized combinations of these principles, leading to novel type systems with better tradeoffs between requirements and guarantees. Please see our conference paper on the topic or its journal version.

The above results cover the so-called possibilistic noninterference, where the observer/attacker is assumed to be unaware of possible resolutions of the program's nondeterminism. With a few granes of salt the results can be extended to probablistic noninterference (as we show in this paper) and to threads run under a class of well-behaved schedulers (as we show in this other paper).

System security

Whereas language-based security focuses on programs written in a programming language and its methods operate on program syntax, system security covers general automata (or state-event systems) and its methods are mainly semantic.

The information-flow security models proposed by theoreticians are typically not confronted with the complexity of a realistic application, and therefore fail to address, or abstract away from, important aspects concerning the conditions for information release or restraint. In our work, we take a different, bottom-up approach: we first formalize the functionality of a realistic system in such a way that we can automatically synthesize an implementation; then we identify, formulate and verify confidentiality properties.

The result is CoCon, a verified realistic conference management system that provably does not leak confidential information. This experience, together with a screening of the theoretical literature, led to the design of a flexible verification infrastructure for restricted information flow in IO automata. More details can be found in this paper.

How we do it

We believe that the best environment to represent a complex system for precisely formulating and fully verifying its security properties is an interactive theorem prover, in our case Isabelle/HOL. If the representation is carefully designed, then code extraction and refinement technology can be used to automatically produce an implementation in an actual programming language. (This is exactly what we did for CoCon.)

However, everybody knows interactive verification involves a lot of work. Yet, with judicious automation support, the boring details of the proof development could in principle be delegated to the machine, with the human only ''intervening'' in the critical/interesting aspects of the verification.

To achieve this, Isabelle teams up with the automatic first-order theorem prover SPASS: Isabelle's Sledgehammer tool translates higher-order logic goals into first-order logic and asks SPASS and other external automatic tools to prove the translated goal. We design the translations to be sound and complete, yet efficient (as we discuss in this paper), and we verify their soundness and completeness in Isabelle itself (as we discuss in this other paper).

We also take several steps to leverage the translations from the other side, by integrating in SPASS features inspired by Isabelle's infrastructure, including specific simplification-rule orientation and clause-selection strategies. The main challenge was of course to do this without compromising completeness, which would be a mortal sin for a first-order automatic prover. The sinless integration and its consequences for the automation of security proofs are discussed in this paper.

Relevant Publications

  1. Draft Sudeep Kanav, Peter Lammich, Andrei Popescu A Conference Management System with Verified Document Confidentiality To be presented at CAV 2014

  2. Draft Slides Andrei Popescu, Johannes Hölzl, Tobias Nipkow Formalizing Probabilistic Noninterference CPP 2013, LNCS 8307, 259-275, Springer

  3. Draft Andrei Popescu, Johannes Hölzl, Tobias Nipkow Formal Verification of Language-Based Concurrent Noninterference Journal of Formalized Reasoning 6(1) 2013.

  4. Preprint Slides Jasmin Christian Blanchette, Andrei Popescu Mechanizing the metatheory of Sledgehammer FroCoS 2013, LNCS 8152, 245-260, Springer

  5. Preprint Slides Andrei Popescu, Johannes Hölzl, Tobias Nipkow Noninterfering Schedulers: When Possibilistic Noninterference Implies Probabilistic Noninterference CALCO 2013, LNCS 8089, 236-252, Springer

  6. Preprint Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone Encoding Monomorphic and Polymorphic Types TACAS 2013, LNCS 7795, 493-507, Springer

  7. Preprint Andrei Popescu, Johannes Hölzl, Tobias Nipkow Proving Concurrent Noninterference CPP 2012, LNCS 7795, 109-125, Springer, Proud receiver of the RS3 best paper award for 2012-2013

  8. Preprint Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification ITP 2012, LNCS 7406, 345-360, Springer

Relevant Isabelle Developments

  1. Andrei Popescu, Peter Lammich Bounded-Deducibility Security Archive of Formal Proofs (2014)

  2. Markus N. Rabe, Peter Lammich, Andrei Popescu A shallow embedding of HyperCTL* Archive of Formal Proofs (2014)

  3. Andrei Popescu, Johannes Hölzl Probabilistic Noninterference Archive of Formal Proofs (2014)

  4. Jasmin Christian Blanchette, Andrei Popescu Sound and Complete Sort Encodings for First-Order Logic Archive of Formal Proofs (2013)

  5. Andrei Popescu, Johannes Hölzl Possibilistic Noninterference Archive of Formal Proofs (2012)