If you want to cite KeY, we recommend to cite the following publication:
Ahrendt, Wolfgang, Beckert, Bernhard, Bubel, Richard, Hähnle, Reiner, Schmitt, Peter, Ulbrich, Mattias (Ed.): Deductive Software Verification - The KeY Book - From Theory to Practice. Springer, 2016, ISBN: 978-3-319-49811-9.
(BibTeX)
BibTeX (Download)
@book{KeYBook2016,
title = {Deductive Software Verification - The KeY Book - From Theory to Practice},
editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H\"{a}hnle and Peter H. Schmitt and Mattias Ulbrich},
url = {http://dx.doi.org/10.1007/978-3-319-49812-6},
doi = {10.1007/978-3-319-49812-6},
isbn = {978-3-319-49811-9},
year = {2016},
date = {2016-12-16},
volume = {10001},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {book}
}
You can also download a BibTeX file with all entries.
2016 |
Hentschel, Martin; Hähnle, Reiner; Bubel, Richard The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts Inproceedings Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 846–851, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5. @inproceedings{ HentschelHB16ASE16b, title = {The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts}, author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel}, isbn = {978-1-4503-3845-5}, year = {2016}, date = {2016-01-01}, booktitle = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering}, pages = {846--851}, publisher = {ACM}, address = {Singapore, Singapore}, series = {ASE 2016}, abstract = {The Symbolic Execution Debugger (SED) is an extension of the Eclipse debug platform for interactive symbolic execution. Like a traditional debugger, the SED can be used to locate the origin of a defect and to increase program understanding. However, as it is based on symbolic execution, all execution paths are explored simultaneously. We demonstrate an extension of the SED called Interactive Verification Debugger (IVD) for inspection and understanding of formal verification attempts. By a number of novel views, the IVD allows to quickly comprehend interactive proof situations and to debug the reasons for a proof attempt that got stuck. It is possible to perform interactive proofs completely from within the IVD. It can be experimentally demonstrated that the IVD is more effective in understanding proof attempts than a conventional prover user interface. A screencast explaining proof attempt inspection with the IVD is available at youtu.be/8e-q9Jf1h_w.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The Symbolic Execution Debugger (SED) is an extension of the Eclipse debug platform for interactive symbolic execution. Like a traditional debugger, the SED can be used to locate the origin of a defect and to increase program understanding. However, as it is based on symbolic execution, all execution paths are explored simultaneously. We demonstrate an extension of the SED called Interactive Verification Debugger (IVD) for inspection and understanding of formal verification attempts. By a number of novel views, the IVD allows to quickly comprehend interactive proof situations and to debug the reasons for a proof attempt that got stuck. It is possible to perform interactive proofs completely from within the IVD. It can be experimentally demonstrated that the IVD is more effective in understanding proof attempts than a conventional prover user interface. A screencast explaining proof attempt inspection with the IVD is available at youtu.be/8e-q9Jf1h_w. |
Hentschel, Martin Integrating Symbolic Execution, Debugging and Verification PhD Thesis Technische Universität Darmstadt, 2016. @phdthesis{ TUD-CS-2016-0099, title = {Integrating Symbolic Execution, Debugging and Verification}, author = {Martin Hentschel}, year = {2016}, date = {2016-01-01}, school = {Technische Universit\"{a}t Darmstadt}, abstract = {In modern software development, almost all activities are centered around an integrated development environment (IDE). Besides the main use cases to write, execute and debug source code, an IDE serves also as front-end for other tools involved in the development process such as a version control system or an application lifecycle management. Independent from the applied development process, the techniques to ensure correct software are always the same. The general goal is to find defects as soon as possible, because the sooner a defect is found, the easier and cheaper it is to fix. In the first place, the programming language helps to prevent some kinds of defects. Once something is written, it is effective to review it not only to find defects, but also to increase its quality. Also tools which statically analyze the source code help to find defects automatically. In addition, testing is used to ensure that selected usage scenarios behave as expected. However, a test can only show the presence of a failure and not its absence. To ensure that a program is correct, it needs to be proven that the program complies to a formal specification describing the desired behavior. This is done by formal verification tools. Finally, whenever a failure is observed, debugging takes place to locate the defect. This thesis extends the software development tool suite by an interactive debugger based on symbolic execution, a technique to explore all feasible execution paths up to a given depth simultaneously. Such a tool can not only be used for classical debugging activities, but also during code reviews or in order to present results of an analysis based on symbolic execution. The contribution is an extension of symbolic execution to explore the full program behavior even in presence of loops and recursive method calls. This is achieved by integrating specifications in form of loop invariants and methods contracts into a symbolic execution engine. How such a symbolic execution engine based on verification proofs can be realized is presented as well. In addition, the presented Symbolic Execution Debugger (SED) makes the Eclipse platform ready for debuggers based on symbolic execution. Its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, program execution paths as well as intermediate states are visualized. By default, the SED comes with a symbolic execution engine implemented on top of the KeY verification system. Statistical evidence that the SED increases effectiveness of code reviews is gained from a controlled experiment. Another novelty of the SED is that arbitrary verification proofs can be inspected. Whereas traditional user interfaces of verification tools present proof states in a mathematical fashion, the SED analyzes the full proof and presents different aspects of it using specialized views. A controlled experiment gives statistical evidence that proof understanding tasks are more effective using the SED by comparing its user interface with the original one of KeY. The SED allows one to interact with the underlying prover by adapting code and specifications in an auto-active flavor, which creates the need to manage proofs directly within an IDE. A presented concept achieves this, by integrating a semi-automatic verification tool into an IDE. It includes several optimizations to reduce the overall proof time and can be realized without changing the verification tool. An optimal user experience is achieved only if all aspects of verification are directly supported within the IDE. Thus a thorough integration of KeY into Eclipse is presented, which for instance includes in addition to the proof management capabilities to edit JML specifications and to setup the needed infrastructure for verification with KeY. Altogether, a platform for tools based on symbolic execution and related to verification is presented, which offers a seamless integration into an IDE and furthers a usage in combination. Furthermore, many aspects, like the way the SED presents proof attempts to users, help to reduce the barrier of using formal methods.}, keywords = {}, pubstate = {published}, tppubtype = {phdthesis} } In modern software development, almost all activities are centered around an integrated development environment (IDE). Besides the main use cases to write, execute and debug source code, an IDE serves also as front-end for other tools involved in the development process such as a version control system or an application lifecycle management. Independent from the applied development process, the techniques to ensure correct software are always the same. The general goal is to find defects as soon as possible, because the sooner a defect is found, the easier and cheaper it is to fix. In the first place, the programming language helps to prevent some kinds of defects. Once something is written, it is effective to review it not only to find defects, but also to increase its quality. Also tools which statically analyze the source code help to find defects automatically. In addition, testing is used to ensure that selected usage scenarios behave as expected. However, a test can only show the presence of a failure and not its absence. To ensure that a program is correct, it needs to be proven that the program complies to a formal specification describing the desired behavior. This is done by formal verification tools. Finally, whenever a failure is observed, debugging takes place to locate the defect. This thesis extends the software development tool suite by an interactive debugger based on symbolic execution, a technique to explore all feasible execution paths up to a given depth simultaneously. Such a tool can not only be used for classical debugging activities, but also during code reviews or in order to present results of an analysis based on symbolic execution. The contribution is an extension of symbolic execution to explore the full program behavior even in presence of loops and recursive method calls. This is achieved by integrating specifications in form of loop invariants and methods contracts into a symbolic execution engine. How such a symbolic execution engine based on verification proofs can be realized is presented as well. In addition, the presented Symbolic Execution Debugger (SED) makes the Eclipse platform ready for debuggers based on symbolic execution. Its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, program execution paths as well as intermediate states are visualized. By default, the SED comes with a symbolic execution engine implemented on top of the KeY verification system. Statistical evidence that the SED increases effectiveness of code reviews is gained from a controlled experiment. Another novelty of the SED is that arbitrary verification proofs can be inspected. Whereas traditional user interfaces of verification tools present proof states in a mathematical fashion, the SED analyzes the full proof and presents different aspects of it using specialized views. A controlled experiment gives statistical evidence that proof understanding tasks are more effective using the SED by comparing its user interface with the original one of KeY. The SED allows one to interact with the underlying prover by adapting code and specifications in an auto-active flavor, which creates the need to manage proofs directly within an IDE. A presented concept achieves this, by integrating a semi-automatic verification tool into an IDE. It includes several optimizations to reduce the overall proof time and can be realized without changing the verification tool. An optimal user experience is achieved only if all aspects of verification are directly supported within the IDE. Thus a thorough integration of KeY into Eclipse is presented, which for instance includes in addition to the proof management capabilities to edit JML specifications and to setup the needed infrastructure for verification with KeY. Altogether, a platform for tools based on symbolic execution and related to verification is presented, which offers a seamless integration into an IDE and furthers a usage in combination. Furthermore, many aspects, like the way the SED presents proof attempts to users, help to reduce the barrier of using formal methods. |
Thüm, Thomas; Winkelmann, Tim; Schröter, Reimar; Hentschel, Martin; Krüger, Stefan Variability Hiding in Contracts for Dependent Software Product Lines Inproceedings Proceedings of the Tenth International Workshop on Variability Modelling of Software-intensive Systems, pp. 97–104, ACM, Salvador, Brazil, 2016, ISBN: 978-1-4503-4019-9. @inproceedings{ThumWSHK16, title = {Variability Hiding in Contracts for Dependent Software Product Lines}, author = {Thomas Th\"{u}m and Tim Winkelmann and Reimar Schr\"{o}ter and Martin Hentschel and Stefan Kr\"{u}ger}, isbn = {978-1-4503-4019-9}, year = {2016}, date = {2016-01-01}, booktitle = {Proceedings of the Tenth International Workshop on Variability Modelling of Software-intensive Systems}, pages = {97--104}, publisher = {ACM}, address = {Salvador, Brazil}, series = {VaMoS '16}, abstract = {Software product lines are used to efficiently develop and verify similar software products. While they focus on reuse of artifacts between products, a product line may also be reused itself in other product lines. A challenge with such dependent product lines is evolution; every change in a product line may influence all dependent product lines. With variability hiding, we aim to hide certain features and their artifacts in dependent product lines. In prior work, we focused on feature models and implementation artifacts. We build on this by discussing how variability hiding can be extended to specifications in terms of method contracts. We illustrate variability hiding in contracts by means of a running example and share our insights with preliminary experiments on the benefits for formal verification. In particular, we find that not every change in a certain product line requires a re-verification of other dependent product lines.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Software product lines are used to efficiently develop and verify similar software products. While they focus on reuse of artifacts between products, a product line may also be reused itself in other product lines. A challenge with such dependent product lines is evolution; every change in a product line may influence all dependent product lines. With variability hiding, we aim to hide certain features and their artifacts in dependent product lines. In prior work, we focused on feature models and implementation artifacts. We build on this by discussing how variability hiding can be extended to specifications in terms of method contracts. We illustrate variability hiding in contracts by means of a running example and share our insights with preliminary experiments on the benefits for formal verification. In particular, we find that not every change in a certain product line requires a re-verification of other dependent product lines. |
Dörre, Felix; Klebanov, Vladimir Pseudo-Random Number Generator Verification: A Case Study Inproceedings Revised Selected Papers of the 7th International Conference on Verified Software: Theories, Tools, and Experiments, pp. 61–72, Springer-Verlag New York, Inc., San Francisco, CA, USA, 2016, ISBN: 978-3-319-29612-8. BibTeX | Links: @inproceedings{DorreK15, title = {Pseudo-Random Number Generator Verification: A Case Study}, author = {Felix D\"{o}rre and Vladimir Klebanov}, url = {http://dx.doi.org/10.1007/978-3-319-29613-5_4}, doi = {10.1007/978-3-319-29613-5_4}, isbn = {978-3-319-29612-8}, year = {2016}, date = {2016-01-01}, booktitle = {Revised Selected Papers of the 7th International Conference on Verified Software: Theories, Tools, and Experiments}, volume = {9593}, pages = {61--72}, publisher = {Springer-Verlag New York, Inc.}, address = {San Francisco, CA, USA}, series = {VSTTE 2015}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
Scheurer, Dominic; Hähnle, Reiner; Bubel, Richard A General Lattice Model for Merging Symbolic Execution Branches Inproceedings Ogata, Kazuhiro; Lawford, Mark; Liu, Shaoying (Ed.): Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings, pp. 57–73, Springer International Publishing, 2016. @inproceedings{scheurer.hahnle.ea_general-lattice-model_16, title = {A General Lattice Model for Merging Symbolic Execution Branches}, author = {Dominic Scheurer and Reiner H\"{a}hnle and Richard Bubel}, editor = {Kazuhiro Ogata and Mark Lawford and Shaoying Liu}, url = {http://link.springer.com/chapter/10.1007/978-3-319-47846-3_5 /wp-content/uploads/2016/12/SHB-General_Lattice_Model-2016.pdf}, doi = {10.1007/978-3-319-47846-3_5}, year = {2016}, date = {2016-01-01}, booktitle = {Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings}, volume = {10009}, pages = {57--73}, publisher = {Springer International Publishing}, series = {LNCS}, abstract = {Symbolic execution is a software analysis technique that has been used with success in the past years in program testing and verification. A main bottleneck of symbolic execution is the path explosion problem: the number of paths in a symbolic execution tree is exponential in the number of static branches of the executed program. Here we put forward an abstraction-based framework for state merging in symbolic execution. We show that it subsumes existing approaches and prove soundness. The method was implemented in the verification system KeY. Our empirical evaluation shows that reductions in proof size of up to 80 % are possible by state merging when applied to complex verification problems; new proofs become feasible that were out of reach so far.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Symbolic execution is a software analysis technique that has been used with success in the past years in program testing and verification. A main bottleneck of symbolic execution is the path explosion problem: the number of paths in a symbolic execution tree is exponential in the number of static branches of the executed program. Here we put forward an abstraction-based framework for state merging in symbolic execution. We show that it subsumes existing approaches and prove soundness. The method was implemented in the verification system KeY. Our empirical evaluation shows that reductions in proof size of up to 80 % are possible by state merging when applied to complex verification problems; new proofs become feasible that were out of reach so far. |
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. BibTeX | Links: @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} } |
Mostowski, Wojciech; Ulbrich, Mattias Dynamic Dispatch for Method Contracts Through Abstract Predicates Journal Article Trans. Modularity and Composition, 1 , pp. 238–267, 2016. BibTeX | Links: @article{MostowskiU16, title = {Dynamic Dispatch for Method Contracts Through Abstract Predicates}, author = {Wojciech Mostowski and Mattias Ulbrich}, url = {http://dx.doi.org/10.1007/978-3-319-46969-0_7}, doi = {10.1007/978-3-319-46969-0_7}, year = {2016}, date = {2016-01-01}, journal = {Trans. Modularity and Composition}, volume = {1}, pages = {238--267}, crossref = {DBLP:journals/taosd/2016-1}, keywords = {}, pubstate = {published}, tppubtype = {article} } |
Hentschel, Martin; Hähnle, Reiner; Bubel, Richard Can Formal Methods Improve the Efficiency of Code Reviews? Inproceedings Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings, pp. 3–19, 2016. BibTeX | Links: @inproceedings{HentschelHB16iFM, title = {Can Formal Methods Improve the Efficiency of Code Reviews?}, author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel}, url = {http://dx.doi.org/10.1007/978-3-319-33693-0_1}, doi = {10.1007/978-3-319-33693-0_1}, year = {2016}, date = {2016-01-01}, booktitle = {Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings}, pages = {3--19}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
Wasser, Nathan Automatic generation of specifications using verification tools = Automatische Spezifikationserzeugung mit Hilfe von Verifikationswerkzeugen PhD Thesis Darmstadt University of Technology, Germany, 2016. BibTeX | Links: @phdthesis{DBLP:phd/dnb/Wasser16, title = {Automatic generation of specifications using verification tools = Automatische Spezifikationserzeugung mit Hilfe von Verifikationswerkzeugen}, author = {Nathan Wasser}, url = {http://tuprints.ulb.tu-darmstadt.de/5910/}, year = {2016}, date = {2016-01-01}, school = {Darmstadt University of Technology, Germany}, keywords = {}, pubstate = {published}, tppubtype = {phdthesis} } |
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. @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} } |
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. @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. |
Mostowski, Wojciech; Ulbrich, Mattias Dynamic Dispatch for Method Contracts through Abstract Predicates Inproceedings Proceedings of the 14th International Conference on Modularity, MODULARITY 2015, Fort Collins, CO, USA, March 16 - 19, 2015, pp. 109–116, ACM, 2015. BibTeX | Links: @inproceedings{MostowskiU15, title = {Dynamic Dispatch for Method Contracts through Abstract Predicates}, author = {Wojciech Mostowski and Mattias Ulbrich}, url = {http://doi.acm.org/10.1145/2724525.2724574}, doi = {10.1145/2724525.2724574}, year = {2015}, date = {2015-01-01}, booktitle = {Proceedings of the 14th International Conference on Modularity, MODULARITY 2015, Fort Collins, CO, USA, March 16 - 19, 2015}, pages = {109--116}, publisher = {ACM}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
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. BibTeX | Links: @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 Inproceedings 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. |
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. @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. |
Schmitt, Peter H; Ulbrich, Mattias Axiomatization of Typed First-Order Logic Inproceedings 20th International Symposium on Formal Methods (FM 2015), pp. 470–486, 2015. BibTeX | Links: @inproceedings{SchmittUlbrich2015, title = {Axiomatization of Typed First-Order Logic}, author = {Peter H. Schmitt and Mattias Ulbrich}, doi = {10.1007/978-3-319-19249-9_29}, year = {2015}, date = {2015-01-01}, booktitle = {20th International Symposium on Formal Methods (FM 2015)}, volume = {9109}, pages = {470--486}, series = {LNCS}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
Wasser, Nathan Generating Specifications for Recursive Methods by Abstracting Program States Inproceedings SETTA, pp. 243–257, Springer, 2015. @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 |
Hentschel, Martin; Käsdorf, Stefan; Hähnle, Reiner; Bubel, Richard An interactive verification tool meets an IDE Inproceedings Albert, Elvira; Sekerinski, Emil; Zavattaro, Gianluigi (Ed.): Proceedings of the 11th International Conference on Integrated Formal Methods, pp. 55–70, Springer, 2014. @inproceedings{hentschel.kasdorf.ea:interactive, title = {An interactive verification tool meets an IDE}, author = {Martin Hentschel and Stefan K\"{a}sdorf and Reiner H\"{a}hnle and Richard Bubel}, editor = {Elvira Albert and Emil Sekerinski and Gianluigi Zavattaro}, year = {2014}, date = {2014-09-01}, booktitle = {Proceedings of the 11th International Conference on Integrated Formal Methods}, pages = {55--70}, publisher = {Springer}, series = {LNCS}, abstract = {We present a general approach on how to integrate a semi-automatic verification tool into a state-of-the-art integrated development environment (IDE). The objective and challenge is to keep implementation, specification and proofs in sync. Following a change in one of the specifications or implementations, all proofs that could possibly be affected by that change are rescheduled. To improve performance we look at several optimizations. User feedback about proof results is provided within the IDE using standard markers and views. The approach has been implemented and realizes an integration of the interactive verification system KeY into the Eclipse IDE.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We present a general approach on how to integrate a semi-automatic verification tool into a state-of-the-art integrated development environment (IDE). The objective and challenge is to keep implementation, specification and proofs in sync. Following a change in one of the specifications or implementations, all proofs that could possibly be affected by that change are rescheduled. To improve performance we look at several optimizations. User feedback about proof results is provided within the IDE using standard markers and views. The approach has been implemented and realizes an integration of the interactive verification system KeY into the Eclipse IDE. |
Hentschel, Martin; Bubel, Richard; Hähnle, Reiner Symbolic Execution Debugger (SED) Inproceedings Bonakdarpour, Borzoo; Smolka, Scott A (Ed.): Proceedings of Runtime Verification 2014, pp. 255–262, Springer, 2014. @inproceedings{hentschel.bubel.ea:symbolic, title = {Symbolic Execution Debugger (SED)}, author = {Martin Hentschel and Richard Bubel and Reiner H\"{a}hnle}, editor = {Borzoo Bonakdarpour and Scott A. Smolka}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of Runtime Verification 2014}, pages = {255--262}, publisher = {Springer}, series = {LNCS}, abstract = {We present the Symbolic Execution Debugger for sequential Java programs. Based on symbolic execution, its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all possible program execution paths are explored simultaneously. To support program comprehension execution paths as well as intermediate states are visualized.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We present the Symbolic Execution Debugger for sequential Java programs. Based on symbolic execution, its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all possible program execution paths are explored simultaneously. To support program comprehension execution paths as well as intermediate states are visualized. |
Thüm, Thomas; Meinicke, Jens; Benduhn, Fabian; Hentschel, Martin; von Rhein, Alexander; Saake, Gunter Potential Synergies of Theorem Proving and Model Checking for Software Product Lines Inproceedings Proceedings of the International Software Product Line Conference (SPLC), ACM, New York, NY, USA, 2014. @inproceedings{ TUD-CS-2014-0930, title = {Potential Synergies of Theorem Proving and Model Checking for Software Product Lines}, author = {Thomas Th\"{u}m and Jens Meinicke and Fabian Benduhn and Martin Hentschel and Alexander von Rhein and Gunter Saake}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the International Software Product Line Conference (SPLC)}, publisher = {ACM}, address = {New York, NY, USA}, series = {SPLC}, abstract = {The verification of software product lines is an active research area. A challenge is to efficiently verify similar products without the need to generate and verify them individually. As solution, researchers suggest family-based verification approaches, which either transform compile-time into runtime variability or make verification tools variabilityaware. Existing approaches either focus on theorem proving, model checking, or other verification techniques. For the first time, we combine theorem proving and model checking to evaluate their synergies for product-line verification. We provide tool support by connecting five existing tools, namely FeatureIDE and FeatureHouse for product-line development, as well as KeY, JPF, and OpenJML for verification of Java programs. In an experiment, we found the synergy of improved effectiveness and efficiency, especially for product lines with few defects. Further, we experienced that model checking and theorem proving are more efficient and effective if the product line contains more defects.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The verification of software product lines is an active research area. A challenge is to efficiently verify similar products without the need to generate and verify them individually. As solution, researchers suggest family-based verification approaches, which either transform compile-time into runtime variability or make verification tools variabilityaware. Existing approaches either focus on theorem proving, model checking, or other verification techniques. For the first time, we combine theorem proving and model checking to evaluate their synergies for product-line verification. We provide tool support by connecting five existing tools, namely FeatureIDE and FeatureHouse for product-line development, as well as KeY, JPF, and OpenJML for verification of Java programs. In an experiment, we found the synergy of improved effectiveness and efficiency, especially for product lines with few defects. Further, we experienced that model checking and theorem proving are more efficient and effective if the product line contains more defects. |
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. @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. |
Hentschel, Martin; Hähnle, Reiner; Bubel, Richard Visualizing Unbounded Symbolic Execution Inproceedings Seidl, Martina; Tillmann, Nikolai (Ed.): Proceedings of Testing and Proofs (TAP) 2014, pp. 82–98, Springer, 2014. @inproceedings{ TUD-CS-2014-0831, title = {Visualizing Unbounded Symbolic Execution}, author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel}, editor = {Martina Seidl and Nikolai Tillmann}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of Testing and Proofs (TAP) 2014}, pages = {82--98}, publisher = {Springer}, series = {LNCS}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
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. BibTeX | Links: @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} } |
Bruns, Daniel Formal Verification of an Electronic Voting System Technical Report Department of Informatics, Karlsruhe Institute of Technology (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. |
Bruns, Daniel Towards Specification and Verification of Information Flow in Concurrent Java-like Programs Technical Report Department of Informatics, Karlsruhe Institute of Technology (2014,5), 2014, ISSN: 2190-4782. @techreport{Bruns14a, title = {Towards Specification and Verification of Information Flow in Concurrent Java-like Programs}, author = {Daniel Bruns}, url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000039446}, issn = {2190-4782}, year = {2014}, date = {2014-01-01}, number = {2014,5}, institution = {Department of Informatics, Karlsruhe Institute of Technology}, series = {Karlsruhe Reports in Informatics}, abstract = {Today, nearly all personal computer systems are multiprocessor systems, allowing multiple programs to be executed in parallel while accessing a shared memory. At the same time, computers are increasingly handling more and more data. Ensuring that no confidential data is leaked to untrusted sinks remains a major quest in software engineering. Formal verification, based on theorem proving, is a powerful technique to prove both functional correctness and security properties such as absence of information flow. Present verification systems are sound and complete, but often lack efficiency and are only applicable to sequential programs. Concurrent programs are notorious for all possible environment actions have to be taken into account. In this paper, we point out steps towards a formal verification methodology for information flow in concurrent programs. We consider passive attackers who are able to observe public parts of the memory at any time during execution and to compare program traces between different executions. Our approach consists of two main elements: (i) formalizing properties on whether two executions are indistinguishable to such an attacker in a decidable logic, and (ii) defining a technique to reason about executions of concurrent programs by regarding a single thread in isolation. The latter is based on the rely/guarantee approach.}, keywords = {}, pubstate = {published}, tppubtype = {techreport} } Today, nearly all personal computer systems are multiprocessor systems, allowing multiple programs to be executed in parallel while accessing a shared memory. At the same time, computers are increasingly handling more and more data. Ensuring that no confidential data is leaked to untrusted sinks remains a major quest in software engineering. Formal verification, based on theorem proving, is a powerful technique to prove both functional correctness and security properties such as absence of information flow. Present verification systems are sound and complete, but often lack efficiency and are only applicable to sequential programs. Concurrent programs are notorious for all possible environment actions have to be taken into account. In this paper, we point out steps towards a formal verification methodology for information flow in concurrent programs. We consider passive attackers who are able to observe public parts of the memory at any time during execution and to compare program traces between different executions. Our approach consists of two main elements: (i) formalizing properties on whether two executions are indistinguishable to such an attacker in a decidable logic, and (ii) defining a technique to reason about executions of concurrent programs by regarding a single thread in isolation. The latter is based on the rely/guarantee approach. |