Using theorem provers to increase the precision of dependence analysis for information flow control
| Autor: | Simon Bischof, Michael Kirsten, Bernhard Beckert, Marko Kleine Büning, Mihai Herda |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Information flow control
Theoretical computer science Computer science Deductive verification DATA processing & computer science Control (management) 020207 software engineering 02 engineering and technology Dependence analysis Combined approach System dependence graph Theorem provers Automated theorem proving Scalability Path (graph theory) 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Information flow (information theory) ddc:004 Noninterference |
| Zdroj: | Formal Methods and Software Engineering ISBN: 9783030024499 ICFEM |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.5445/ir/1000088397 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|