Secure Type Systems and Deduction

Affiliated institutions and people

This is a joint project between Technische Universität München and the Max-Planck-Institut für Informatik Saarbrücken. It is part of part of the DFG priority program Reliably Secure Software Systems (RS3).

Topic and objectives

The project focuses on the interactive and automatic verification of methods for information flow analysis in the context of language-based security. Its two main objectives are:

  1. Formalization in Isabelle of language-based security results, with an emphasis on security type systems
  2. Improvement of the integration of Isabelle and SPASS

Work done in phase 1 of the project (Sept. 2010 - Sept. 2012)

1. We have considered a while-language with parallel composition under a shared-memory interleaving semantics. For the probabilistic case, the language has been extended with probabilistic choice and the parallel threads have been assumed as either managed by the uniform scheduler or by an unspecified scheduler. We have not targeted isolated results in language-based security, but have aimed at providing a formalized framework that captures existing results from the literature in a uniform way and is in principle able to accommodate others. Besides the intrinsic interest in unifying scattered results, this unification effort has paid off with revealing novel noniterference results, both in a possibilistic and a probabilistic setting.

2. The integration of our main collaborating tools, Isabelle and SPASS, has been significantly improved. The overall performance of the new SPASS improved by almost 16% over the old SPASS on non-trivial goals from a broad set of Isabelle theories - i.e. where at the beginning of the project Isabelle’s Sledgehammer (the tool that connects Isabelle to SPASS and other ATPs) combined with SPASS found 100 proofs, the improved link now finds 116 proofs—and the current Isabelle-SPASS integration has become the most powerful automated theorem prover integration today.

Relevant publications

  1. Andrei Popescu, Johanes Hölzl, Tobias Nipkow. Proving concurrent noninterference. Certified Programs and Proofs (CPP) 2012, to appear.
  2. Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach. More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. Interactive Theorem Proving (ITP) 2012, 345-360