A Hybrid Approach for Proving Noninterference of Java Programs
Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns,
Michael Kirsten, and Martin Mohr
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 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 Kuesters, 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.