POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 16:55 - 17:20 at Auditorium - Security and Privacy Chair(s): Cătălin Hriţcu

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.

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 17:45
Security and PrivacyPOPL at Auditorium
Chair(s): Cătălin Hriţcu Inria Paris
16:30
25m
Talk
LMS-Verify: Abstraction Without Regret for Verified Systems Programming
POPL
Nada Amin EPFL, Tiark Rompf Purdue University
16:55
25m
Talk
Hypercollecting Semantics and its Application to Static Analysis of Information Flow
POPL
Mounir Assaf Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Julien Signoles CEA LIST, Éric Totel CentraleSupélec, Frédéric Tronel CentraleSupélec
17:20
25m
Talk
LightDP: Towards Automating Differential Privacy Proofs
POPL
Danfeng Zhang Pennsylvania State University, Daniel Kifer Dept. of Computer Science and Engineering, Penn State University