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
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
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.
Type de document :
Communication dans un congrès
POPL 2017 - ACM Symposium on Principles of Programming Languages, Jan 2017, Paris, France. ACM, 52 (1), pp.874-887, ACM SIGPLAN Notices - POPL '17. 〈https://popl17.sigplan.org/〉. 〈10.1145/3009837.3009889〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01618360
Contributeur : Eric Totel <>
Soumis le : mardi 17 octobre 2017 - 17:35:55
Dernière modification le : jeudi 11 janvier 2018 - 06:28:14

Fichier

2017_popl.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

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. ACM, 52 (1), pp.874-887, ACM SIGPLAN Notices - POPL '17. 〈https://popl17.sigplan.org/〉. 〈10.1145/3009837.3009889〉. 〈hal-01618360〉

Partager

Métriques

Consultations de la notice

95

Téléchargements de fichiers

7