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

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning
In:20th International Conference on Formal Engineering Methods - Formal Methods and Software Engineering (ICFEM 2018)
Publisher:Springer
Series:Lecture Notes in Computer Science
Volume:11232
Year:2018
Pages:284-300
DOI:10.1007/978-3-030-02450-5_17

Abstract

Information flow control (IFC) is a category of techniques for enforcing information flow properties. In this paper we present the 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 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 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.
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 Combined Approach that uses the tools JOANA and KeY as the SDG-based and logic-based approach respectively.

BibTeX

@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)},
venue     = {Gold Coast, QLD, Australia},
eventdate = {2018-11-12/2018-11-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}
}