Skip to Main content Skip to Navigation
Conference papers

Hypercollecting Semantics and its Application to Static Analysis of Information Flow

Mounir Assaf 1 David Naumann 1 Julien Signoles 2 Eric Totel 3 Frédéric Tronel 3
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
3 CIDRE - Confidentialité, Intégrité, Disponibilité et Répartition
CentraleSupélec, Inria Rennes – Bretagne Atlantique , IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Eric Totel <>
Submitted on : Tuesday, October 17, 2017 - 5:35:55 PM
Last modification on : Friday, July 10, 2020 - 4:02:10 PM
Long-term archiving on: : Thursday, January 18, 2018 - 3:39:17 PM


Files produced by the author(s)



Mounir Assaf, David 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⟩



Record views


Files downloads