DeduSec

Program-level Specification and Deductive Verification of Security Properties

In recent years tremendous progress has been achieved in formal verification of functional properties of computer programs. At the same time seminal papers have been published showing that it is in principle possible to formulate information-flow problems as proof obligations in program logics. The overall goal of the project is to leverage these advances together with our own experience in formal methods for functional properties in order to specify and verify security properties.

The project will make the following contributions to the first two guiding themes of DFG Priority Programme 1496 “Reliably Secure Software Systems – RS³”, the formalization of and the verification of security properties:

1. We will define syntax and semantics of a specification and program annotation language for information-flow properties of computer programs.
2. We will design and implement a deductive verification system that allows to prove formally that programs satisfy their information-flow specification and that meets the requirements of soundness, precision, scalability, and usability set forth in the Priority Programme. The system will be based on the KeY tool.

News

• October 2010: Official project start