KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo
§
Postprint
DOI: 10.5445/IR/1000071329
Veröffentlicht am 16.10.2018

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

Beckert, Bernhard; Bischof, Simon; Herda, Mihai; Kirsten, Michael; Kleine Büning, Marko

Abstract (englisch):
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üsters et al., which – however – is based on program modifications and still requires a significant amount of user interaction.
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 evaluate ... mehr


Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Jahr 2017
Sprache Englisch
Identifikator URN: urn:nbn:de:swb:90-713299
KITopen-ID: 1000071329
Erschienen in ETAPS 2017: 5th Workshop on Hot Issues in Security Principles and Trust : Hotspot 2017, Uppsala, Sweden, 22-29 April 2017
Verlag Theoretical Foundations of Security Analysis and Design (IFIP WG 1.7)
Seiten 6-25
Projektinformation KASTEL_IoE (BMBF, 16KIS0346)
Vorab online veröffentlicht am 10.03.2017
Schlagworte non-interference, information flow control, dependency graph, verification
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page