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 approach, which is evaluated on a case study,
demonstrating the feasibility of automatic and precise non-interference
proofs for complex programs.

Open Access Logo


Postprint §
DOI: 10.5445/IR/1000071329
Veröffentlicht am 16.10.2018
Coverbild
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