KIT | KIT-Bibliothek | Impressum | Datenschutz

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

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

Abstract:
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 ap ... mehr

Open Access Logo


Postprint §
DOI: 10.5445/IR/1000071329
Veröffentlicht am 16.10.2018
Seitenaufrufe: 27
seit 04.05.2018
Downloads: 5
seit 16.10.2018
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: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)
SPP 1496 (DFG, DFG KOORD, BE 2334/6-1)
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