2015
|
Bruns, Daniel; Mostowski, Wojciech; Ulbrich, Mattias Implementation-level Verification of Algorithms with KeY Journal Article Software Tools for Technology Transfer, 17 (6), pp. 729–744, 2015, ISSN: 1433-2779. Abstract | Links | BibTeX @article{bruns.mostowski.ea:implementation-level,
title = {Implementation-level Verification of Algorithms with KeY},
author = {Daniel Bruns and Wojciech Mostowski and Mattias Ulbrich},
url = {http://link.springer.com/article/10.1007/s10009-013-0293-y},
doi = {10.1007/s10009-013-0293-y},
issn = {1433-2779},
year = {2015},
date = {2015-01-01},
journal = {Software Tools for Technology Transfer},
volume = {17},
number = {6},
pages = {729--744},
publisher = {Springer},
abstract = {We give an account on the authors' experience and results from the software verification competition held at the Formal Methods~2012 conference. Competitions like this are meant to provide a benchmark for verification systems. It consisted of three algorithms which the authors have implemented in Java, specified with the Java Modeling Language, and verified using the KeY system. Building on our solutions, we argue that verification systems which target implementations in real-world programming languages are required to have powerful capabilities for abstraction. Regarding the KeY tool, we explain features which, driven by the competition, have been freshly implemented to accommodate for these demands.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
We give an account on the authors' experience and results from the software verification competition held at the Formal Methods~2012 conference. Competitions like this are meant to provide a benchmark for verification systems. It consisted of three algorithms which the authors have implemented in Java, specified with the Java Modeling Language, and verified using the KeY system. Building on our solutions, we argue that verification systems which target implementations in real-world programming languages are required to have powerful capabilities for abstraction. Regarding the KeY tool, we explain features which, driven by the competition, have been freshly implemented to accommodate for these demands. |
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 @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. |
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 @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. |
Wasser, Nathan Generating Specifications for Recursive Methods by Abstracting Program States Inproceedings SETTA, pp. 243–257, Springer, 2015. BibTeX @inproceedings{DBLP:conf/setta/Wasser15,
title = {Generating Specifications for Recursive Methods by Abstracting Program States},
author = {Nathan Wasser},
year = {2015},
date = {2015-01-01},
booktitle = {SETTA},
volume = {9409},
pages = {243--257},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2014
|
Ghazi, Aboubakr Achraf El; Ulbrich, Mattias; Gladisch, Christoph; Tyszberowicz, Shmuel; Taghdiri, Mana JKelloy: A Proof Assistant for Relational Specifications of Java Programs Inproceedings NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, pp. 173–187, 2014. Links | BibTeX @inproceedings{nfm2014JKelloy,
title = {JKelloy: A Proof Assistant for Relational Specifications of Java Programs},
author = {Aboubakr Achraf El Ghazi and Mattias Ulbrich and Christoph Gladisch and Shmuel Tyszberowicz and Mana Taghdiri},
url = {http://dx.doi.org/10.1007/978-3-319-06200-6_13},
doi = {10.1007/978-3-319-06200-6_13},
year = {2014},
date = {2014-01-01},
booktitle = {NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings},
pages = {173--187},
crossref = {DBLP:conf/nfm/2014},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
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 @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. |
2013
|
Kirsten, Michael Proving Well-Definedness of JML Specifications with KeY Masters Thesis ITI Schmitt, Karlsruhe Institute of Technology, 2013. Abstract | BibTeX @mastersthesis{KirstenStA2013,
title = {Proving Well-Definedness of JML Specifications with KeY},
author = {Michael Kirsten},
year = {2013},
date = {2013-01-01},
school = {ITI Schmitt, Karlsruhe Institute of Technology},
abstract = {Specification methods in formal program verification enable the enhancement of source
code with formal annotations as to formally specify the behaviour of a program. This is
a popular way in order to subsequently prove software to be reliable and meet certain
requirements, which is crucial for many applications and gains even more importance in
modern society. The annotations can be taken as a contract, which then can be verified
guaranteeing the specified program element \textendash as a receiver \textendash to fulfil this contract with
its caller. However, these functional contracts can be problematic for partial functions,
e.g. a division, as certain cases may be undefined, as in this example a division by zero.
Modern programming languages such as Java handle undefined behaviour by casting an exception.
There are several approaches to handle a potential undefinedness of specifications. In
this thesis, we chose one which automatically generates formal proof obligations ensuring
that undefined specification expressions will not be evaluated.
Within this work, we elaborate on so-called Well-Definedness Checks dealing with undefinedness
occurring in specifications of the modelling language JML/JML* in the
KeY System, which is a formal software development tool providing mechanisms to
deductively prove the before mentioned contracts. Advantages and delimitations are
discussed and, furthermore, precise definitions as well as a fully functional implementation
within KeY are given. Our work covers the major part of the specification elements
currently supported by KeY, on the higher level including class invariants, model fields,
method contracts, loop statements and block contracts. The process of checking the
well-definedness of a specification forms a preliminary step before the actual proof and
rejects undefined specifications. We further contribute by giving a choice between two
different semantics, both bearing different advantages and disadvantages. The thesis also
includes an extensive case study analysing many examples and measuring the performance
of the implemented Well-Definedness Checks.},
type = {Studienarbeit},
keywords = {},
pubstate = {published},
tppubtype = {mastersthesis}
}
Specification methods in formal program verification enable the enhancement of source
code with formal annotations as to formally specify the behaviour of a program. This is
a popular way in order to subsequently prove software to be reliable and meet certain
requirements, which is crucial for many applications and gains even more importance in
modern society. The annotations can be taken as a contract, which then can be verified
guaranteeing the specified program element – as a receiver – to fulfil this contract with
its caller. However, these functional contracts can be problematic for partial functions,
e.g. a division, as certain cases may be undefined, as in this example a division by zero.
Modern programming languages such as Java handle undefined behaviour by casting an exception.
There are several approaches to handle a potential undefinedness of specifications. In
this thesis, we chose one which automatically generates formal proof obligations ensuring
that undefined specification expressions will not be evaluated.
Within this work, we elaborate on so-called Well-Definedness Checks dealing with undefinedness
occurring in specifications of the modelling language JML/JML* in the
KeY System, which is a formal software development tool providing mechanisms to
deductively prove the before mentioned contracts. Advantages and delimitations are
discussed and, furthermore, precise definitions as well as a fully functional implementation
within KeY are given. Our work covers the major part of the specification elements
currently supported by KeY, on the higher level including class invariants, model fields,
method contracts, loop statements and block contracts. The process of checking the
well-definedness of a specification forms a preliminary step before the actual proof and
rejects undefined specifications. We further contribute by giving a choice between two
different semantics, both bearing different advantages and disadvantages. The thesis also
includes an extensive case study analysing many examples and measuring the performance
of the implemented Well-Definedness Checks. |
2012
|
Beckert, Bernhard; Bruns, Daniel Formal Semantics of Model Fields in Annotation-based Specifications Inproceedings Glimm, Birte; Krüger, Antonio (Ed.): KI 2012: Advances in Artificial Intelligence, pp. 13–24, Springer-Verlag, 2012, ISBN: 978-3-642-33346-0. Abstract | Links | BibTeX @inproceedings{BeckertBruns12,
title = {Formal Semantics of Model Fields in Annotation-based Specifications},
author = {Bernhard Beckert and Daniel Bruns},
editor = {Birte Glimm and Antonio Kr\"{u}ger},
url = {http://link.springer.com/chapter/10.1007/978-3-642-33347-7_2},
isbn = {978-3-642-33346-0},
year = {2012},
date = {2012-01-01},
booktitle = {KI 2012: Advances in Artificial Intelligence},
volume = {7526},
pages = {13--24},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
abstract = {It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification and verification, model fields are a common means for those goals. However, it remains a challenge to provide a well-founded formal semantics for the general case in which the abstraction relation defining a model field is non-functional. In this paper, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is based on a generalization of Hilbert's $varepsilon$~terms.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification and verification, model fields are a common means for those goals. However, it remains a challenge to provide a well-founded formal semantics for the general case in which the abstraction relation defining a model field is non-functional. In this paper, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is based on a generalization of Hilbert's $varepsilon$~terms. |
Beckert, Bernhard; Bruns, Daniel Dynamic Trace Logic: Definition and Proofs Technical Report Department of Informatics, Karlsruhe Institute of Technology (2012,10), 2012, ISSN: 2190-4782, (A revised version replacing an unsound rule is available at
http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf). Abstract | Links | BibTeX @techreport{BeckertBruns12a,
title = {Dynamic Trace Logic: Definition and Proofs},
author = {Bernhard Beckert and Daniel Bruns},
url = {http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf,
http://digbib.ubka.uni-karlsruhe.de/volltexte/1000028184},
issn = {2190-4782},
year = {2012},
date = {2012-01-01},
number = {2012,10},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
abstract = {Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic~(DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for functional verification of concurrent programs and for proving information-flow properties among other applications.},
note = {A revised version replacing an unsound rule is available at
http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic~(DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for functional verification of concurrent programs and for proving information-flow properties among other applications. |
2011
|
Ulbrich, Mattias; Geilmann, Ulrich; Ghazi, Aboubakr Achraf El; Taghdiri, Mana On Proving Alloy Specifications using KeY Technical Report Karlsruhe Institute of Technology (2011-37), 2011. BibTeX @techreport{ulbrich-geilmann-elghazi-taghdiri-techrep2011,
title = {On Proving Alloy Specifications using KeY},
author = {Mattias Ulbrich and Ulrich Geilmann and Aboubakr Achraf El Ghazi and Mana Taghdiri},
year = {2011},
date = {2011-01-01},
number = {2011-37},
institution = {Karlsruhe Institute of Technology},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
|
Proving the Correctness of Program Transformations with Abstract Execution and REFINITY - Summary. Abstract Execution (AE) is a new program analysis technique for automatically proving second-order properties about programs. It is based on the symbolic execution of abstract programs with second-order symbolic stores.
Proving JDK’s Dual Pivot Quicksort Correct - by Bernhard Beckert, Jonas Schiffl, Peter H. Schmitt and Mattias Ulbrich Sorting is a fundamental functionality in libraries, for which efficiency is crucial. Correctness of the highly optimized implementations is often taken for granted. De Gouw et al. have shown that this certainty is deceptive by revealing a bug in the Java Development Kit (JDK) […]
New Feature: State Merging in KeY - Current nightly builds of KeY contain a new feature called state merging, a technique to decrease the size of proof trees arising from the symbolic execution of large programs.