KIT | KIT-Bibliothek | Impressum | Datenschutz

Using theorem provers to increase the precision of dependence analysis for information flow control

Beckert, B. ORCID iD icon 1; Bischof, S. 1; Herda, M. 1; Kirsten, M. ORCID iD icon 1; Kleine Büning, M. 1
1 Karlsruher Institut für Technologie (KIT)


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.

Postprint §
DOI: 10.5445/IR/1000088397
Veröffentlicht am 12.10.2019
DOI: 10.1007/978-3-030-02450-5_17
Zitationen: 1
Zitationen: 1
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsdatum 11.10.2018
Sprache Englisch
Identifikator ISBN: 978-3-030-02449-9
ISSN: 0302-9743, 1611-3349
KITopen-ID: 1000088397
HGF-Programm 37.01.03 (POF III, LK 01) Batteries in Application
Weitere HGF-Programme 46.23.01 (POF IV, LK 01) Methods for Engineering Secure Systems
Erschienen in 20th International Conference on Formal Engineering Methods, ICFEM 2018; Gold Coast; Australia; 12 November 2018 through 16 November 2018. Ed.: J. Sun
Verlag Springer
Seiten 284-300
Serie Lecture notes in computer science ; 11232
Projektinformation SPP 1496 (DFG, DFG KOORD, BE 2334/6-1)
Schlagwörter Information flow control, Noninterference, System dependence graph, Deductive verification
Nachgewiesen in Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page