Hypercollecting semantics and its application to static analysis of information flow

DOI10.1145/3009837.3009889zbMATH Open1380.68113arXiv1608.01654OpenAlexW3099266052MaRDI QIDQ5370922FDOQ5370922

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)

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.

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

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

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)

Cited In (6)

• Constraint-based relational verification
• Verifying bounded subset-closed hyperproperties
• Sound symbolic execution via abstract interpretation and its application to security
• Constructive Galois Connections
• 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)