Program Verification

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}