Combining Graph-Based and Deduction-Based Information-Flow Analysis

Reviewed Paper In Proceedings

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.

BibTeX

@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}
}