Information Flow Analysis

This page is under construction

Secure information flow implies that an attacker cannot learn confidential data (secrets) by observing public output. We use KeY to verify that a program adheres to a specified information flow policy (project DeduSec) and to generate test cases that show the existence of an information leak or even extract the actual secret (project ALBIA).

Projects

  • Go here for DeduSec: Program-level Specification and Deductive Verification of Security Properties

  • Go here for ALBIA: Fully Automatic Logic-Based Information Flow Analysis

Literature

2016

Do, Quoc Huy; Kamburjan, Eduard; Wasser, Nathan

Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study Inproceedings

Proceedings of the 5th International Conference on Principles of Security and Trust - Volume 9635, pp. 97–115, Springer-Verlag New York, Inc., New York, NY, USA, 2016, ISBN: 978-3-662-49634-3.

Links | BibTeX

2015

Beckert, Bernhard; Klebanov, Vladimir; Ulbrich, Mattias

Regression Verification for Java Using a Secure Information Flow Calculus Inproceedings

Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, pp. 6:1–6:6, ACM, Prague, Czech Republic, 2015, ISBN: 978-1-4503-3656-7.

BibTeX

Do, Quoc Huy; Bubel, Richard; Hähnle, Reiner

Exploit Generation for Information Flow Leaks in Object-Oriented Programs Inproceedings

ICT Systems Security and Privacy Protection - 30th IFIP TC 11 International Conference, SEC 2015, Hamburg, Germany, May 26-28, 2015, Proceedings, pp. 401–415, 2015.

Links | BibTeX

Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Kirsten, Michael; Mohr, Martin

A Hybrid Approach for Proving Noninterference of Java Programs Inproceedings

Fournet, Cédric; Hicks, Michael (Ed.): 28th IEEE Computer Security Foundations Symposium (CSF 2015), pp. 305-319, 2015.

Abstract | Links | BibTeX

Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Kirsten, Michael; Mohr, Martin

A Hybrid Approach for Proving Noninterference of Java Programs Journal Article

IACR Cryptology ePrint Archive, 2015 , pp. 438, 2015.

Abstract | Links | BibTeX

2014

Bruns, Daniel

Formal Verification of an Electronic Voting System Technical Report

Department of Informatics, Karlsruhe Institute of Technology (2014,11), 2014, ISSN: 2190-4782.

Abstract | Links | BibTeX

Ahrendt, Wolfgang; Beckert, Bernhard; Bruns, Daniel; Bubel, Richard; Gladisch, Christoph; Grebing, Sarah; Hähnle, Reiner; Hentschel, Martin; Herda, Mihai; Klebanov, Vladimir; Mostowski, Wojciech; Scheben, Christoph; Schmitt, Peter H; Ulbrich, Mattias

The KeY Platform for Verification and Analysis of Java Programs Inproceedings

Giannakopoulou, Dimitra; Kroening, Daniel (Ed.): Verified Software: Theories, Tools, and Experiments (VSTTE 2014), pp. 1–17, Springer-Verlag, 2014, ISBN: 978-3-642-54107-0.

Abstract | Links | BibTeX

2012

Beckert, Bernhard; Bruns, Daniel; Küsters, Ralf; Scheben, Christoph; Schmitt, Peter H; Truderung, Tomasz

The KeY Approach for the Cryptographic Verification of Java Programs: A Case Study Technical Report

Department of Informatics, Karlsruhe Institute of Technology (2012,8), 2012.

Abstract | Links | BibTeX

2005

Darvas, Ádám; Hähnle, Reiner; Sands, Dave

A Theorem Proving Approach to Analysis of Secure Information Flow Inproceedings

Hutter, Dieter; Ullmann, Markus (Ed.): Proc. 2nd International Conference on Security in Pervasive Computing, pp. 193–209, Springer-Verlag, 2005.

Links | BibTeX

2003

Darvas, Ádám; Hähnle, Reiner; Sands, Dave

A Theorem Proving Approach to Analysis of Secure Information Flow Inproceedings

Gorrieri, Roberto (Ed.): Workshop on Issues in the Theory of Security, WITS, IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS 2003.

BibTeX