Paper 2015/438

A Hybrid Approach for Proving Noninterference of Java Programs

Ralf Kuesters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr

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 \emph{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 the verification only 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 this 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--- as well as the CVJ framework proposed by Küsters, 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.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Minor revision. CSF 2015
Keywords
code-level cryptographic analysis
Contact author(s)
kuesters @ uni-trier de
History
2015-05-08: received
Short URL
https://ia.cr/2015/438
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2015/438,
      author = {Ralf Kuesters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and Michael Kirsten and Martin Mohr},
      title = {A Hybrid Approach for Proving Noninterference of Java Programs},
      howpublished = {Cryptology ePrint Archive, Paper 2015/438},
      year = {2015},
      note = {\url{https://eprint.iacr.org/2015/438}},
      url = {https://eprint.iacr.org/2015/438}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.