Hypercollecting semantics and its application to static analysis of information flow

Mounir Assaf, David A. Naumann, Julien Signoles, Éric Totel, Frédéric Tronel

Research output: Contribution to journalArticlepeer-review

5 Scopus citations

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 hyperproperties 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.

Original languageEnglish
Pages (from-to)874-887
Number of pages14
JournalACM SIGPLAN Notices
Volume52
Issue number1
DOIs
StatePublished - Jan 2017

Keywords

  • abstract interpretation
  • hyperproperties
  • information flow
  • static analysis

Fingerprint

Dive into the research topics of 'Hypercollecting semantics and its application to static analysis of information flow'. Together they form a unique fingerprint.

Cite this