DeduSec

Program-level Specification and Deductive Verification of Security Properties

The overall goal of the DeduSec project is to apply logic-based techniques and our extensive experience in formal methods for functional properties to specification and verification of security properties of software. We are developing novel methods and tools for deductive reasoning about information flow on the program level. The project is part of the DFG Priority Programme 1496 “Reliably Secure Software Systems – RS³”.

The DeduSec project in Phase 3 (October 2014 onwards) has two major parts:

• Specifying and verifying information flow properties of object-oriented software. We are developing specification languages as well as sound and complete calculi for verifying complex information flows in Java programs. The technical platform is the KeY theorem prover.
• Quantitative information flow analysis (QIF). In realistic scenarios, it may be infeasible to completely prevent information leaks (i.e., undesired flow of confidential information to public ports). We are developing a collection of techniques and tools for measuring the amount of leaked information in order to decide if a leak is tolerable.

News

• September 2017: CombinedApproach (new tool) - First tool that combines fast dependency graph analysis with precise deductive verification for proving non-interference of Java programs (see Software).
• August 2016: CVE-2016-6313 - Critical bug in the GnuPG/Libgcrypt PRNG found with help of Entroposcope.
• February 2016: Entroposcope (new tool) - The first static analysis for finding bugs in PRNGs.
• October 2015: Daniel Grahl successfully defends his PhD thesis, in which he extends the KeY approach to information flow analysis to concurrent Java programs. See the publication list for details.
• February 2015: The newest release of the KeY system includes proof obligations for information flow (see Software).
• October 2014: Third phase of the project is approved. Dr. Vladimir Klebanov has joined the team of the principal investigators of the project. Prof. Schmitt will continue active involvment in the project as emeritus.
• August 2014: The paper 'Information Flow in Object-oriented Software' has been accepted to appear in the post-proceedings of LOPSTR.
• December 2013: Examples for verifying information flow in KeY run fully automatically now (e-voting case study excepted).
• November 2013: New case studies in KeY available via Web Start.
• February 2013: The workshop on information flow in object-oriented systems organized by Daniel Bruns takes place in Darmstadt.