A Hybrid Approach for Proving Noninterference and Applications to the
Cryptographic Verification of Java Programs
Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns,
Jürgen Graf, and Christoph Scheben
The problem of checking noninterference properties of programs has a long
tradition in the field of computer security and, in particular, in
language-based security. A program is called noninterferent
(w.r.t. confidentiality) if no information from high variables, which contain
confidential information, flows to low variables, which can be observed by the
attacker or an unauthorized user. Several tools and approaches exist in the
literature for checking noninterference. Some approaches, such as type
checking, abstract interpretations, and program dependency graphs, with tools
including Joana, JIF, and TAJ, have a high degree of automation, but they
overapproximate the actual information flow, and hence, may produce false
positives. Others, such as those based on theorem proving, with tools such as
KeY, Isabelle, and Coq, allow for very precise analysis, but need human
interaction and, hence, analysis is often time-consuming. Certainly, fully
automated tools are preferable over interactive approaches. However, if
automated tools fail due to false positives and the analysis cannot further be
refined by these tools, because, for example, the tools do not allow this or
run into scalability problems, the only option for proving noninterference so
far is to drop the automated tools altogether and instead turn to fine-grained
but interactive, and hence, more time-consuming approaches, such as theorem
proving. This "all or nothing" approach is unsatisfying and problematic in
practice. In this paper, we therefore propose a simple, tool-independent
approach, which we call hybrid approach and which allows one to use automated
analysis of noninterference properties as much as possible and only resort to
more fine-grained analysis at places in a program where necessary, where the
latter analysis requires checking merely specific functional properties in
parts of the program, rather than checking the more involved noninterference
properties (for the whole program).