A Hybrid Approach for Proving Noninterference of Java Programs

@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                   = {https://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.}
}