Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Capability machines are a special form of CPUs that offer fine-grained privilege separation using a form of authority-carrying values known as capabilities. The CHERI capability machine offers local capabilities, which could be used as a cheap but restricted form of capability revocation. Unfortunately, local capability revocation is unrealistic in practice because large amounts of stack memory need to be cleared as a security precaution.
In this paper, we address this shortcoming by introducing uninitialized capabilities: a new form of capabilities that represent read/write authority to a block of memory without exposing the memory’s initial contents. We provide a mechanically verified program logic for reasoning about programs on a capability machine with the new feature and we formalize and prove capability safety in the form of a universal contract for untrusted code. We use uninitialized capabilities for making a previously-proposed secure calling convention efficient and prove its security using the program logic. Finally, we report on a proof-of-concept implementation of uninitialized capabilities on the CHERI capability machine.
Thu 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00
|Efficient and Provable Local Capability Revocation using Uninitialized Capabilities|
Aina Linn Georges Aarhus University, Armaël Guéneau Aarhus University, Thomas Van Strydonck KULeuven, Amin Timany Aarhus University, Alix Trieu Aarhus University, Sander Huyghebaert Vrije Universiteit Brussel, Dominique Devriese Vrije Universiteit Brussel, Lars Birkedal Aarhus UniversityLink to publication DOI Pre-print
|Mechanized Logical Relations for Termination-Insensitive Noninterference|
Simon Oddershede Gregersen Aarhus University, Johan Bay Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus UniversityLink to publication DOI Pre-print
|Giving Semantics to Program-Counter Labels via Secure Effects|
POPLLink to publication DOI
|Automata and Fixpoints for Asynchronous Hyperproperties|
Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-Olm University of Münster, Christoph Ohrem Westfälische Wilhelms-Universität Münster (WWU), GermanyLink to publication DOI
|Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper|
Marco Vassena CISPA Helmholtz Center for Information Security, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Sunjay Cauligi University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego, USALink to publication DOI Pre-print