A Hybrid Approach for Proving Noninterference of Java Programs

@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},
  pages         = {305--319},
  year          = {2015},
  month         = jul,
  language      = {english},
  venue         = {Verona, Italy},
  eventdate     = {2015-07-13/2015-07-17},
  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.}
}