Information flow control (IFC) is a category of techniques for enforcing information
flow properties. In this paper we present the Combined Approach, a novel IFC
technique that combines a scalable system-dependence-graph-based (SDG-based)
approach with a precise logic-based approach based on a theorem prover. The
Combined Approach has an increased precision compared with the SDG-based
approach on its own, without sacrificing its scalability. For every potential illegal
information flow reported by the SDG-based approach, the Combined Approach
automatically generates proof obligations that, if valid, prove that there is no
program path for which the reported information flow can happen. These proof
obligations are then relayed to the logic-based approach.
We also show how the SDG-based approach can provide additional information to
the theorem prover that helps decrease the verification effort. Moreover, we
present a prototypical implementation of the Combined Approach that uses the
tools JOANA and KeY as the SDG-based and logic-based approach respectively.