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

Hyperproperties have received increasing attention in the last decade due to their importance e.g. for security analyses. Past approaches have focussed on synchronous analyses, i.e. techniques in which different paths are compared lockstepwise. In this paper, we systematically study asynchronous analyses for hyperproperties by introducing both a novel automata model (Alternating Asynchronous Parity Automata) and the temporal fixpoint calculus Hμ, the first fixpoint calculus that can systematically express hyperproperties in an asynchronous manner and at the same time subsumes the existing logic HyperLTL. We show that the expressive power of both models coincides over fixed path assignments. The high expressive power of both models is evidenced by the fact that decision problems of interest are highly undecidable, i.e. not even arithmetical. As a remedy, we propose approximative analyses for both models that also induce natural decidable fragments.

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
10m
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
10m
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
10m
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
10m
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
10m
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
10m
Break
Break
POPL