2015
|
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. |
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. |
Schmitt, Peter H.; Ulbrich, Mattias Axiomatization of Typed First-Order Logic Proceedings Article In: 20th International Symposium on Formal Methods (FM 2015), pp. 470–486, 2015. @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 Proceedings Article In: 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 Proceedings Article In: 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) Proceedings Article In: 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 Proceedings Article In: 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 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. |
Hentschel, Martin; Hähnle, Reiner; Bubel, Richard Visualizing Unbounded Symbolic Execution Proceedings Article In: 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 Proceedings Article In: NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, pp. 173–187, 2014. @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 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. |
Bruns, Daniel Towards Specification and Verification of Information Flow in Concurrent Java-like Programs Technical Report Department of Informatics, Karlsruhe Institute of Technology no. 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. |
2013
|
Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Graf, Jürgen; Scheben, Christoph A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of Java Programs Proceedings Article In: Hammer, Christian; Mauw, Sjouke (Ed.): Grande Region Security and Reliability Day 2013, Luxembourg, 2013, (Extended Abstract). @inproceedings{kusters.truderung.ea:hybrid,
title = {A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of Java Programs},
author = {Ralf K\"{u}sters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and J\"{u}rgen Graf and Christoph Scheben},
editor = {Christian Hammer and Sjouke Mauw},
url = {http://grsrd.uni.lu/papers/grsrd2013_submission_2.pdf},
year = {2013},
date = {2013-01-01},
booktitle = {Grande Region Security and Reliability Day 2013},
address = {Luxembourg},
note = {Extended Abstract},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Beckert, Bernhard; Bruns, Daniel; Klebanov, Vladimir; Scheben, Christoph; Schmitt, Peter H.; Ulbrich, Mattias Information Flow in Object-Oriented Software - Extended Version Technical Report Department of Informatics, Karlsruhe Institute of Technology no. 2013,14, 2013, ISSN: 2190-4782. @techreport{BeckertBrunsKlebanovEtAl13,
title = {Information Flow in Object-Oriented Software - Extended Version},
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov and Christoph Scheben and Peter H. Schmitt and Mattias Ulbrich},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000037606},
issn = {2190-4782},
year = {2013},
date = {2013-01-01},
number = {2013,14},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
|
Beckert, Bernhard; Bruns, Daniel; Klebanov, Vladimir; Scheben, Christoph; Schmitt, Peter H.; Ulbrich, Mattias Secure Information Flow for Java - A Dynamic Logic Approach Technical Report Department of Informatics, Karlsruhe Institute of Technology no. 2013,10, 2013, ISSN: 2190-4782. @techreport{BeckertBrunsKlebanovEtAl13a,
title = {Secure Information Flow for Java - A Dynamic Logic Approach},
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov and Christoph Scheben and Peter H. Schmitt and Mattias Ulbrich},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000036786},
issn = {2190-4782},
year = {2013},
date = {2013-01-01},
number = {2013,10},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
|
Beckert, Bernhard; Bruns, Daniel Dynamic Logic with Trace Semantics Proceedings Article In: Bonacina, Maria Paola (Ed.): 24th International Conference on Automated Deduction (CADE-24), pp. 315–329, Springer-Verlag, 2013, ISBN: 978-3-642-38573-5. @inproceedings{BeckertBruns13,
title = {Dynamic Logic with Trace Semantics},
author = {Bernhard Beckert and Daniel Bruns},
editor = {Maria Paola Bonacina},
url = {http://link.springer.com/chapter/10.1007/978-3-642-38574-2_22},
doi = {10.1007/978-3-642-38574-2_22},
isbn = {978-3-642-38573-5},
year = {2013},
date = {2013-01-01},
booktitle = {24th International Conference on Automated Deduction (CADE-24)},
volume = {7898},
pages = {315--329},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
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 proving functional and information-flow properties in concurrent programs, among other applications.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
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 proving functional and information-flow properties in concurrent programs, among other applications. |
Gladisch, Christoph; Tyszberowicz, Shmuel Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking Proceedings Article In: de Moura, Leonardo; Iyoda, Juliano (Ed.): Brazilian Symposium on Formal Methods (SBMF), Springer, 2013. @inproceedings{gladischTyszberowicz2013,
title = {Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking},
author = {Christoph Gladisch and Shmuel Tyszberowicz},
editor = {Leonardo de Moura and Juliano Iyoda},
year = {2013},
date = {2013-01-01},
booktitle = {Brazilian Symposium on Formal Methods (SBMF)},
volume = {8195},
publisher = {Springer},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Kirsten, Michael Proving Well-Definedness of JML Specifications with KeY Masters Thesis ITI Schmitt, Karlsruhe Institute of Technology, 2013. @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
|
Ulbrich, Mattias; Geilmann, Ulrich; Ghazi, Aboubakr Achraf El; Taghdiri, Mana A Proof Assistant for Alloy Specifications Proceedings Article In: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 422-436, 2012. @inproceedings{ulbrich-geilmann-elghazi-taghdiri-tacas2012,
title = {A Proof Assistant for Alloy Specifications},
author = {Mattias Ulbrich and Ulrich Geilmann and Aboubakr Achraf El Ghazi and Mana Taghdiri},
year = {2012},
date = {2012-03-01},
booktitle = {18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
pages = {422-436},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Beckert, Bernhard; Bruns, Daniel Formal Semantics of Model Fields in Annotation-based Specifications Proceedings Article In: Glimm, Birte; Krüger, Antonio (Ed.): KI 2012: Advances in Artificial Intelligence, pp. 13–24, Springer-Verlag, 2012, ISBN: 978-3-642-33346-0. @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 no. 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). @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. |
Bruns, Daniel Eine formale Semantik für die Java Modeling Language Journal Article In: Informatik-Spektrum, vol. 35, no. 1, pp. 45–49, 2012. @article{Bruns12,
title = {Eine formale Semantik f\"{u}r die Java Modeling Language},
author = {Daniel Bruns},
url = {http://www.springerlink.com/content/b503j663353x482w/},
doi = {10.1007/s00287-011-0532-0},
year = {2012},
date = {2012-01-01},
journal = {Informatik-Spektrum},
volume = {35},
number = {1},
pages = {45--49},
publisher = {Springer-Verlag},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
|
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. |
Gladisch, Christoph Model generation for quantified formulas with application to test data generation Journal Article In: International Journal on Software Tools for Technology Transfer (STTT), pp. 1-21, 2012, ISSN: 1433-2779, (10.1007/s10009-012-0227-0). @article{springerlink:10.1007/s10009-012-0227-0,
title = {Model generation for quantified formulas with application to test data generation},
author = {Christoph Gladisch},
url = {http://dx.doi.org/10.1007/s10009-012-0227-0},
issn = {1433-2779},
year = {2012},
date = {2012-01-01},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
pages = {1-21},
publisher = {Springer Berlin / Heidelberg},
note = {10.1007/s10009-012-0227-0},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
|
Thüm, Thomas; Schaefer, Ina; Apel, Sven; Hentschel, Martin Family-Based Deductive Verification of Software Product Lines Proceedings Article In: Proceedings of the 11th International Conference on Generative Programming and Component Engineering, pp. 11-20, ACM, Dresden, Germany, 2012, ISBN: 978-1-4503-1129-8. @inproceedings{ TUD-CS-2012-0355,
title = {Family-Based Deductive Verification of Software Product Lines},
author = {Thomas Th\"{u}m and Ina Schaefer and Sven Apel and Martin Hentschel},
isbn = {978-1-4503-1129-8},
year = {2012},
date = {2012-01-01},
booktitle = {Proceedings of the 11th International Conference on Generative Programming and Component Engineering},
pages = {11-20},
publisher = {ACM},
address = {Dresden, Germany},
series = {GPCE '12},
abstract = {A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used of-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85 %.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used of-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85 %. |