Hypercollecting Semantics and its Application to Static Analysis of Information Flow - Archive ouverte HAL Access content directly
Conference Papers Year :

Hypercollecting Semantics and its Application to Static Analysis of Information Flow

(1) , (1) , (2) , (3) , (3)
1
2
3

Abstract

We show how static analysis for secure information flow can be expressed and proved correct entirely within the framework of abstract interpretation. The key idea is to define a Galois connection that directly approximates the hyperproperty of interest. To enable use of such Galois connections, we introduce a fixpoint characterisation of hypercollecting semantics, i.e. a " set of sets " transformer. This makes it possible to systematically derive static analyses for hyper-properties entirely within the calculational framework of abstract interpretation. We evaluate this technique by deriving example static analyses. For qualitative information flow, we derive a dependence analysis similar to the logic of Amtoft and Banerjee (SAS'04) and the type system of Hunt and Sands (POPL'06). For quantitative information flow, we derive a novel cardinality analysis that bounds the leakage conveyed by a program instead of simply deciding whether it exists. This encompasses problems that are hypersafety but not k-safety. We put the framework to use and introduce variations that achieve precision rivalling the most recent and precise static analyses for information flow.
Fichier principal
Vignette du fichier
2017_popl.pdf (379.93 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01618360 , version 1 (17-10-2017)

Identifiers

Cite

Mounir Assaf, David A Naumann, Julien Signoles, Eric Totel, Frédéric Tronel. Hypercollecting Semantics and its Application to Static Analysis of Information Flow. POPL 2017 - ACM Symposium on Principles of Programming Languages, Jan 2017, Paris, France. pp.874-887, ⟨10.1145/3009837.3009889⟩. ⟨hal-01618360⟩
270 View
122 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More