A Hybrid Approach for Proving Noninterference of Java Programs

Zeitschriftenartikel

Autor(en):Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin Mohr
Zeitschrift:IACR Cryptology ePrint Archive
Band:2015
Jahr:2015
Nummer:438
URL:http://eprint.iacr.org/2015/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ü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.

BibTeX

@article{KuestersTruderungBeckertEA2015b,
  author		= {Ralf K{\"u}sters 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},
  journal		= {{IACR} Cryptology ePrint Archive},
  url			= {http://eprint.iacr.org/2015/438},
  volume		= {2015},
  number		= {438},
  month			= may,
  year			= {2015},
  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.
                           \newline
				   
			   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.
                           \newline
				   
			   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.}
}