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

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