Home  |  english  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

A Hybrid Approach for Proving Noninterference of Java Programs

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin Mohr
In:28th IEEE Computer Security Foundations Symposium (CSF 2015)
Jahr:2015
DOI:10.1109/CSF.2015.28

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

@InProceedings{KuestersTruderungBeckertEA2015,
  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},
  booktitle	= {28th IEEE Computer Security Foundations Symposium (CSF 2015)},
  editor	= {C{\'e}dric Fournet and Michael Hicks},
  doi           = {10.1109/CSF.2015.28},
  year		= 2015,
  month         = jul,
  language	= {english},
  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.}
}