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).