Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Thu 21 Jan 2021 16:20 - 16:30 at POPL-A - Security

Type systems designed for information-flow control commonly use a program-counter label to track the sensitivity of the context and rule out data leakage arising from effectful computation in a sensitive context. Currently, type-system designers reason about this label informally except in security proofs, where they use ad-hoc techniques. We develop a framework based on monadic semantics for effects to give semantics to program-counter labels. This framework leads to three results about program-counter labels. First, we develop a new proof technique for noninterference, the core security theorem for information-flow control in effectful languages. Second, we unify notions of security for different types of effects, including state, exceptions, and nontermination. Finally, we formalize the folklore that program-counter labels are a lower bound on effects. We show that, while not universally true, this folklore has a good semantic foundation.

Thu 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00: SecurityPOPL at POPL-A
16:00 - 16:10
Talk
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
POPL
Aina Linn GeorgesAarhus University, Armaël GuéneauAarhus University, Thomas Van StrydonckKULeuven, Amin TimanyAarhus University, Alix TrieuAarhus University, Sander HuyghebaertVrije Universiteit Brussel, Dominique DevrieseVrije Universiteit Brussel, Lars BirkedalAarhus University
Link to publication DOI Pre-print
16:10 - 16:20
Talk
Mechanized Logical Relations for Termination-Insensitive Noninterference
POPL
Simon Oddershede GregersenAarhus University, Johan BayAarhus University, Amin TimanyAarhus University, Lars BirkedalAarhus University
Link to publication DOI Pre-print
16:20 - 16:30
Talk
Giving Semantics to Program-Counter Labels via Secure Effects
POPL
Andrew HirschMax Planck Institute for Software Systems, Ethan CecchettiCornell University
Link to publication DOI
16:30 - 16:40
Talk
Automata and Fixpoints for Asynchronous Hyperproperties
POPL
Jens Oliver GutsfeldWestfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-OlmUniversity of Münster, Christoph OhremWestfälische Wilhelms-Universität Münster (WWU), Germany
Link to publication DOI
16:40 - 16:50
Talk
Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper
POPL
Marco VassenaCISPA Helmholtz Center for Information Security, Craig DisselkoenUniversity of California at San Diego, USA, Klaus v. GleissenthallVrije Universiteit Amsterdam, Netherlands, Sunjay CauligiUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, Dean TullsenUniversity of California at San Diego, USA, Deian StefanUniversity of California at San Diego, USA
Link to publication DOI Pre-print
16:50 - 17:00
Break
Break
POPL