Hypercollecting semantics and its application to static analysis of information flow

DOI10.1145/3009837.3009889MaRDI QIDQ5370922zbMATH OpenOpenAlexFDO

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

Publication date 20 October 2017

Published in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1608.01654

zbMATH Keywords

abstract interpretationstatic analysisinformation flowhyperproperties

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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 set" 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.

Recommendations

• scientific article; zbMATH DE number 1948407
• Verifying bounded subset-closed hyperproperties
• Static Analysis
• Security through safety. An approach to information flow control based on derivation of safety properties from a characterisation of insecure behaviour
• Analyzing Information Flow Properties in Assembly Code by Abstract Interpretation

Cited in

(6)

• Constraint-based relational verification
• Constructive Galois connections
• Verifying bounded subset-closed hyperproperties
• Sound symbolic execution via abstract interpretation and its application to security
• Abstract semantic dependency
• On collecting semantics for program analysis

This page was built for publication: Hypercollecting semantics and its application to static analysis of information flow

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370922)