Who we areThis 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:
- Jasmin Christian Blanchette (externally funded researcher, München)
- Johannes Hölzl (externally funded researcher, München)
- Peter Lammich (externally funded researcher, München)
- Tobias Nipkow (principal investigator, München)
- Andrei Popescu (funded researcher, München)
- Daniel Wand (funded researcher, Saarbrücken)
- Christoph Weidenbach (principal investigator, Saarbrücken)
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 securityWe 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 securityWhereas 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 itWe 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.
Sudeep Kanav, Peter Lammich, Andrei Popescu A Conference Management System with Verified Document Confidentiality To be presented at CAV 2014
Andrei Popescu, Johannes Hölzl, Tobias Nipkow Formal Verification of Language-Based Concurrent Noninterference Journal of Formalized Reasoning 6(1) 2013.
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
Andrei Popescu, Peter Lammich Bounded-Deducibility Security Archive of Formal Proofs (2014)
Markus N. Rabe, Peter Lammich, Andrei Popescu A shallow embedding of HyperCTL* Archive of Formal Proofs (2014)
Andrei Popescu, Johannes Hölzl Probabilistic Noninterference Archive of Formal Proofs (2014)
Jasmin Christian Blanchette, Andrei Popescu Sound and Complete Sort Encodings for First-Order Logic Archive of Formal Proofs (2013)
Andrei Popescu, Johannes Hölzl Possibilistic Noninterference Archive of Formal Proofs (2012)