@InProceedings{BeckertBischofEA2017, author = {Bernhard Beckert and Simon Bischof and Mihai Herda and Michael Kirsten and Marko {Kleine B\"{u}ning}}, title = {Combining Graph-Based and Deduction-Based Information-Flow Analysis}, booktitle = {5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017) affiliated with ETAPS 2017: European Joint Conferences on Theory and Practice of Software}, editor = {Ralf K{\"u}sters}, url = {https://sec.informatik.uni-stuttgart.de/_media/events/hotspot2017/proceedings.pdf#page=6}, month = apr, year = {2017}, pages = {6--25}, abstract = {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\"{u}sters et al., which -- however -- is based on program modifications and still requires a significant amount of user interaction. \newline 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.}, venue = {Uppsala, Sweden}, eventdate = {2017-04-23/2017-04-23} }
Combining Graph-Based and Deduction-Based Information-Flow Analysis
Author(s): | Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning |
---|---|
In: | 5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017) affiliated with ETAPS 2017: European Joint Conferences on Theory and Practice of Software |
Year: | 2017 |
Pages: | 6-25 |
URL: | https://sec.informatik.uni-stuttgart.de/_media/events/hotspot2017/proceedings.pdf#page=6 |
Abstract
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.