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
2017
Do, Quoc Huy; Bubel, Richard; Hähnle, Reiner
Inferring Secrets by Guided Experiments Proceedings Article
In: Hung, Dang Van; Kapur, Deepak (Ed.): Theoretical Aspects of Computing -- ICTAC 2017: 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings, pp. 269–287, Springer International Publishing, Cham, 2017.
@inproceedings{Do2017,
title = {Inferring Secrets by Guided Experiments},
author = {Quoc Huy Do and Richard Bubel and Reiner H\"{a}hnle},
editor = {Dang Van Hung and Deepak Kapur},
url = {https://doi.org/10.1007/978-3-319-67729-3_16},
doi = {10.1007/978-3-319-67729-3_16},
year = {2017},
date = {2017-01-01},
booktitle = {Theoretical Aspects of Computing -- ICTAC 2017: 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings},
pages = {269--287},
publisher = {Springer International Publishing},
address = {Cham},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
2016
Do, Quoc Huy; Kamburjan, Eduard; Wasser, Nathan
Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study Proceedings Article
In: 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.
@inproceedings{DoKW16,
title = {Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study},
author = {Quoc Huy Do and Eduard Kamburjan and Nathan Wasser},
url = {http://dx.doi.org/10.1007/978-3-662-49635-0_6},
doi = {10.1007/978-3-662-49635-0_6},
isbn = {978-3-662-49634-3},
year = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the 5th International Conference on Principles of Security and Trust - Volume 9635},
pages = {97--115},
publisher = {Springer-Verlag New York, Inc.},
address = {New York, NY, USA},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
2015
Beckert, Bernhard; Klebanov, Vladimir; Ulbrich, Mattias
Regression Verification for Java Using a Secure Information Flow Calculus Proceedings Article
In: 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.
@inproceedings{beckert.klebanov.ea:regression,
title = {Regression Verification for Java Using a Secure Information Flow Calculus},
author = {Bernhard Beckert and Vladimir Klebanov and Mattias Ulbrich},
isbn = {978-1-4503-3656-7},
year = {2015},
date = {2015-01-01},
booktitle = {Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs},
pages = {6:1--6:6},
publisher = {ACM},
address = {Prague, Czech Republic},
series = {FTfJP '15},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Do, Quoc Huy; Bubel, Richard; Hähnle, Reiner
Exploit Generation for Information Flow Leaks in Object-Oriented Programs Proceedings Article
In: 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.
@inproceedings{DoBH15,
title = {Exploit Generation for Information Flow Leaks in Object-Oriented Programs},
author = {Quoc Huy Do and Richard Bubel and Reiner H\"{a}hnle},
url = {http://dx.doi.org/10.1007/978-3-319-18467-8_27},
doi = {10.1007/978-3-319-18467-8_27},
year = {2015},
date = {2015-01-01},
booktitle = {ICT Systems Security and Privacy Protection - 30th IFIP TC 11
International Conference, SEC 2015, Hamburg, Germany, May 26-28,
2015, Proceedings},
pages = {401--415},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Kirsten, Michael; Mohr, Martin
A Hybrid Approach for Proving Noninterference of Java Programs Proceedings Article
In: Fournet, Cédric; Hicks, Michael (Ed.): 28th IEEE Computer Security Foundations Symposium (CSF 2015), pp. 305-319, 2015.
@inproceedings{KuestersTruderungBeckertEA2015,
title = {A Hybrid Approach for Proving Noninterference of Java Programs},
author = {Ralf K\"{u}sters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and Michael Kirsten and Martin Mohr},
editor = {C\'{e}dric Fournet and Michael Hicks},
doi = {10.1109/CSF.2015.28},
year = {2015},
date = {2015-01-01},
booktitle = {28th IEEE Computer Security Foundations Symposium (CSF 2015)},
pages = {305-319},
abstract = {Several tools and approaches for proving noninterference properties for Java and other languages exist.
Some of them have a high degree of automation or are even fully automatic, but overapproximate
the actual information flow, and hence, may produce false positives.
Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence,
analysis is time-consuming.
In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches:
We want to use fully automatic analysis as much as possible and only at places in a program where,
due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification of specific functional properties in certain
parts of the program, rather than checking more intricate noninterference properties for the whole
program.
To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully
automatic tool Joana for checking noninterference properties for Java programs and the theorem prover
KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung,
and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an
e-voting system.
The CVJ framework allows one to establish cryptographic indistinguishability properties for Java
programs by checking (standard) noninterference properties for such programs.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Several tools and approaches for proving noninterference properties for Java and other languages exist.
Some of them have a high degree of automation or are even fully automatic, but overapproximate
the actual information flow, and hence, may produce false positives.
Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence,
analysis is time-consuming.
In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches:
We want to use fully automatic analysis as much as possible and only at places in a program where,
due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification of specific functional properties in certain
parts of the program, rather than checking more intricate noninterference properties for the whole
program.
To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully
automatic tool Joana for checking noninterference properties for Java programs and the theorem prover
KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung,
and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an
e-voting system.
The CVJ framework allows one to establish cryptographic indistinguishability properties for Java
programs by checking (standard) noninterference properties for such programs.
Some of them have a high degree of automation or are even fully automatic, but overapproximate
the actual information flow, and hence, may produce false positives.
Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence,
analysis is time-consuming.
In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches:
We want to use fully automatic analysis as much as possible and only at places in a program where,
due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification of specific functional properties in certain
parts of the program, rather than checking more intricate noninterference properties for the whole
program.
To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully
automatic tool Joana for checking noninterference properties for Java programs and the theorem prover
KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung,
and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an
e-voting system.
The CVJ framework allows one to establish cryptographic indistinguishability properties for Java
programs by checking (standard) noninterference properties for such programs.
Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Kirsten, Michael; Mohr, Martin
A Hybrid Approach for Proving Noninterference of Java Programs Journal Article
In: IACR Cryptology ePrint Archive, vol. 2015, pp. 438, 2015.
@article{KuestersTruderungBeckertEA2015b,
title = {A Hybrid Approach for Proving Noninterference of Java Programs},
author = {Ralf K\"{u}sters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and Michael Kirsten and Martin Mohr},
url = {http://eprint.iacr.org/2015/438},
year = {2015},
date = {2015-01-01},
journal = {IACR Cryptology ePrint Archive},
volume = {2015},
pages = {438},
abstract = {Several tools and approaches for proving noninterference properties for Java and other languages exist.
Some of them have a high degree of automation or are even fully automatic, but overapproximate
the actual information flow, and hence, may produce false positives.
Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence,
analysis is time-consuming.
In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches:
We want to use fully automatic analysis as much as possible and only at places in a program where,
due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification of specific functional properties in certain
parts of the program, rather than checking more intricate noninterference properties for the whole
program.
To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully
automatic tool Joana for checking noninterference properties for Java programs and the theorem prover
KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung,
and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an
e-voting system.
The CVJ framework allows one to establish cryptographic indistinguishability properties for Java
programs by checking (standard) noninterference properties for such programs.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Several tools and approaches for proving noninterference properties for Java and other languages exist.
Some of them have a high degree of automation or are even fully automatic, but overapproximate
the actual information flow, and hence, may produce false positives.
Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence,
analysis is time-consuming.
In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches:
We want to use fully automatic analysis as much as possible and only at places in a program where,
due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification of specific functional properties in certain
parts of the program, rather than checking more intricate noninterference properties for the whole
program.
To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully
automatic tool Joana for checking noninterference properties for Java programs and the theorem prover
KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung,
and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an
e-voting system.
The CVJ framework allows one to establish cryptographic indistinguishability properties for Java
programs by checking (standard) noninterference properties for such programs.
Some of them have a high degree of automation or are even fully automatic, but overapproximate
the actual information flow, and hence, may produce false positives.
Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence,
analysis is time-consuming.
In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches:
We want to use fully automatic analysis as much as possible and only at places in a program where,
due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification of specific functional properties in certain
parts of the program, rather than checking more intricate noninterference properties for the whole
program.
To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully
automatic tool Joana for checking noninterference properties for Java programs and the theorem prover
KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung,
and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an
e-voting system.
The CVJ framework allows one to establish cryptographic indistinguishability properties for Java
programs by checking (standard) noninterference properties for such programs.
2014
Bruns, Daniel
Formal Verification of an Electronic Voting System Technical Report
Department of Informatics, Karlsruhe Institute of Technology no. 2014,11, 2014, ISSN: 2190-4782.
@techreport{Bruns14,
title = {Formal Verification of an Electronic Voting System},
author = {Daniel Bruns},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000042284},
issn = {2190-4782},
year = {2014},
date = {2014-01-01},
number = {2014,11},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
abstract = {Electronic voting (e-voting) systems that are used in public elections need to fulfil a broad range of strong requirements concerning both safety and security. Among these requirements are reliability, robustness, privacy of votes, coercion resistance and universal verifiability. Bugs in or manipulations of an e-voting system may have considerable influence on the life of the humans living in a country where such a system is used. Hence, e-voting systems are an obvious target for software verification. In this paper, we report on an implementation of such a system in Java and the formal verification of functional properties thereof in the KeY verification system. Even though the actual components are clearly modularized, the challenge lies in the fact that we need to prove a highly nonlocal property: After all voters have cast their votes, the server calculates the correct votes for each candidate w.r.t. the original ballots. This kind of trace property is difficult to prove with static techniques like verification and typically yields a large specification overhead.},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
Electronic voting (e-voting) systems that are used in public elections need to fulfil a broad range of strong requirements concerning both safety and security. Among these requirements are reliability, robustness, privacy of votes, coercion resistance and universal verifiability. Bugs in or manipulations of an e-voting system may have considerable influence on the life of the humans living in a country where such a system is used. Hence, e-voting systems are an obvious target for software verification. In this paper, we report on an implementation of such a system in Java and the formal verification of functional properties thereof in the KeY verification system. Even though the actual components are clearly modularized, the challenge lies in the fact that we need to prove a highly nonlocal property: After all voters have cast their votes, the server calculates the correct votes for each candidate w.r.t. the original ballots. This kind of trace property is difficult to prove with static techniques like verification and typically yields a large specification overhead.
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 Proceedings Article
In: 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.
@inproceedings{AhrendtBeckertBrunsEtAl14,
title = {The KeY Platform for Verification and Analysis of Java Programs},
author = {Wolfgang Ahrendt and Bernhard Beckert and Daniel Bruns and Richard Bubel and
Christoph Gladisch and Sarah Grebing and Reiner H\"{a}hnle and Martin Hentschel and
Mihai Herda and Vladimir Klebanov and Wojciech Mostowski and Christoph Scheben and
Peter H. Schmitt and Mattias Ulbrich},
editor = {Dimitra Giannakopoulou and Daniel Kroening},
url = {http://link.springer.com/chapter/10.1007/978-3-319-12154-3_4},
doi = {10.1007/978-3-319-12154-3_4},
isbn = {978-3-642-54107-0},
year = {2014},
date = {2014-01-01},
booktitle = {Verified Software: Theories, Tools, and Experiments (VSTTE 2014)},
number = {8471},
pages = {1--17},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
abstract = {The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.
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 no. 2012,8, 2012.
@techreport{BeckertBrunsKuestersEtAl12,
title = {The KeY Approach for the Cryptographic Verification of Java Programs: A Case Study},
author = {Bernhard Beckert and Daniel Bruns and Ralf K\"{u}sters and Christoph Scheben and Peter H. Schmitt and Tomasz Truderung},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000027497},
year = {2012},
date = {2012-01-01},
number = {2012,8},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
abstract = {In this paper, we report on an ongoing case study in which we use the KeY tool, a theorem prover for checking functional correctness and noninterference properties of Java programs, to establish computational indistinguishability for a simple Java program that involves clients sending encrypted messages over an untrusted network to a server. The analysis uses a general framework, recently proposed by K"usters et al., which enables program analysis tools, such as KeY, that can check (standard) noninterference properties for Java programs to establish computational indistinguishability properties.},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
In this paper, we report on an ongoing case study in which we use the KeY tool, a theorem prover for checking functional correctness and noninterference properties of Java programs, to establish computational indistinguishability for a simple Java program that involves clients sending encrypted messages over an untrusted network to a server. The analysis uses a general framework, recently proposed by K"usters et al., which enables program analysis tools, such as KeY, that can check (standard) noninterference properties for Java programs to establish computational indistinguishability properties.
2005
Darvas, Ádám; Hähnle, Reiner; Sands, Dave
A Theorem Proving Approach to Analysis of Secure Information Flow Proceedings Article
In: Hutter, Dieter; Ullmann, Markus (Ed.): Proc. 2nd International Conference on Security in Pervasive Computing, pp. 193–209, Springer-Verlag, 2005.
@inproceedings{DHS05,
title = {A Theorem Proving Approach to Analysis of Secure Information Flow},
author = {\'{A}d\'{a}m Darvas and Reiner H\"{a}hnle and Dave Sands},
editor = {Dieter Hutter and Markus Ullmann},
url = {http://www.springerlink.com/link.asp?id=rdqa8ejctda3yw64},
year = {2005},
date = {2005-01-01},
booktitle = {Proc. 2nd International Conference on Security in Pervasive Computing},
volume = {3450},
pages = {193--209},
publisher = {Springer-Verlag},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
2003
Darvas, Ádám; Hähnle, Reiner; Sands, Dave
A Theorem Proving Approach to Analysis of Secure Information Flow Proceedings Article
In: Gorrieri, Roberto (Ed.): Workshop on Issues in the Theory of Security, WITS, IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS 2003.
@inproceedings{DHS03,
title = {A Theorem Proving Approach to Analysis of Secure Information Flow},
author = {\'{A}d\'{a}m Darvas and Reiner H\"{a}hnle and Dave
Sands},
editor = {Roberto Gorrieri},
year = {2003},
date = {2003-01-01},
booktitle = {Workshop on Issues in the Theory of Security, WITS},
organization = {IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}