Combining Graph-Based and Deduction-Based Information-Flow Analysis
Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten,
Marko Kleine Büning
Information flow control (IFC) is a category of techniques for ensuring system
security by enforcing information flow properties such as
non-interference. Established IFC techniques range from fully automatic
approaches with much over-approximation to approaches with high precision but
potentially laborious user interaction. A noteworthy approach mitigating the
weaknesses of both automatic and interactive IFC techniques is the hybrid
approach, developed by Küsters et al., which – however – is based on program
modifications and still requires a significant amount of user interaction.
In this paper, we present a combined approach that works without any program
modifications. It minimizes potential user interactions by applying a
dependency-graph-based information-flow analysis first. Based on
over-approximations, this step potentially generates false positives. Precise
non-interference proofs are achieved by applying a deductive theorem prover
with a specialized information-flow calculus for checking that no path from a
secret input to a public output exists. Both tools are fully integrated into a
combined approach, which is evaluated on a case study, demonstrating the
feasibility of automatic and precise non-interference proofs for complex
programs.