Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control

@InProceedings{BeckertBischofEA2018,
  author    = {Bernhard Beckert and
               Simon Bischof and
               Mihai Herda and
               Michael Kirsten and
               Marko Kleine B{\"{u}}ning               
               },
  editor    = {Jing Sun and Meng Sun},
  title     = {Using Theorem Provers to Increase the Precision of
               Dependence Analysis for Information Flow Control},
  booktitle = {20th International Conference on Formal Engineering
               Methods - Formal Methods and Software Engineering
               ({ICFEM} 2018)},
  location  = {Gold Coast, QLD, Australia},
  date      = {November 12-16},
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume    = {11232},
  year      = {2018},
  abstract  = {Information flow control ({IFC}) is a category of techniques for enforcing information
               flow properties. In this paper we present the \emph{Combined Approach}, a novel {IFC}
               technique that combines a scalable system-dependence-graph-based ({SDG}-based)
               approach with a precise logic-based approach based on a theorem prover. The
               \emph{Combined Approach} has an increased precision compared with the {SDG}-based
               approach on its own, without sacrificing its scalability. For every potential illegal
               information flow reported by the {SDG}-based approach, the \emph{Combined Approach}
               automatically generates proof obligations that, if valid, prove that there is no
               program path for which the reported information flow can happen. These proof
               obligations are then relayed to the logic-based approach.
               \newline

               We also show how the {SDG}-based approach can provide additional information to
               the theorem prover that helps decrease the verification effort. Moreover, we
               present a prototypical implementation of the \emph{Combined Approach} that uses the
               tools {JOANA} and {\KeY} as the {SDG}-based and logic-based approach respectively.},
  pages     = {284--300},
  month     = oct,
  doi       = {10.1007/978-3-030-02450-5\_17}
}