KIT | KIT-Bibliothek | Impressum | Datenschutz

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

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


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 pre-
cision but potentially laborious user interaction. A noteworthy approach
mitigating the weaknesses of both automatic and interactive IFC tech-
niques is the hybrid approach, developed by Küsters et al., which – how-
ever – 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 apply-
ing a dependency-graph-based information-flow analysis first. Based on
over-approximations, this step potentially generates false positives. Pre-
cise 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 evaluated on a case study,
... mehr

Postprint §
DOI: 10.5445/IR/1000071329
Veröffentlicht am 16.10.2018
Cover der Publikation
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
Publikationsjahr 2017
Sprache Englisch
Identifikator urn:nbn:de:swb:90-713299
KITopen-ID: 1000071329
HGF-Programm 46.12.03 (POF III, LK 01) Data Security
Weitere HGF-Programme 46.23.01 (POF IV, LK 01) Methods for Engineering Secure Systems
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 SPP 1496 (DFG, DFG KOORD, BE 2334/6-1)
KASTEL_IoE (BMBF, EU 6. RP, 16KIS0346)
Vorab online veröffentlicht am 10.03.2017
Schlagwörter non-interference, information flow control, dependency graph, verification
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page