Beckert, Bernhard
[VerfasserIn];
Bischof, Simon
[VerfasserIn];
Herda, Mihai
[VerfasserIn];
Kirsten, Michael
[VerfasserIn];
Kleine Büning, Marko
[VerfasserIn]
Combining Graph-Based and Deduction-Based Information-Flow Analysis
Titel:
Combining Graph-Based and Deduction-Based Information-Flow Analysis
Beteiligte:
Beckert, Bernhard
[VerfasserIn];
Bischof, Simon
[VerfasserIn];
Herda, Mihai
[VerfasserIn];
Kirsten, Michael
[VerfasserIn];
Kleine Büning, Marko
[VerfasserIn]
Erschienen:
Theoretical Foundations of Security Analysis and Design (IFIP WG 1.7), 2017-01-01
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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 pre- cision but potentially laborious user interaction. A noteworthy approach mitigating the weaknesses of both automatic and interactive IFC tech- niques is the hybrid approach, developed by Küsters et al., which – how- ever – 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 apply- ing a dependency-graph-based information-flow analysis first. Based on over-approximations, this step potentially generates false positives. Pre- cise 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.