Efficient and provable local capability revocation using uninitialized capabilities

Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal

Onderzoeksoutput: Articlepeer review

9 Citaten (Scopus)
118 Downloads (Pure)


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.

Originele taal-2English
Pagina's (van-tot)1-30
Aantal pagina's30
TijdschriftProceedings of the ACM on Programming Languages
Nummer van het tijdschriftPOPL
StatusPublished - 4 jan 2021
EvenementACM SIGPLAN Symposium on Principles of Programming Languages - Copenhagen, Denmark
Duur: 17 jan 202122 jan 2021


Duik in de onderzoeksthema's van 'Efficient and provable local capability revocation using uninitialized capabilities'. Samen vormen ze een unieke vingerafdruk.

Citeer dit