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, and Lars Birkedal: Efficient and Provable Local Capability Revocation using Uninitialized Capabilities. In POPL 2021, January 2021, doi: 10.1145/3434287.
Journal Paper
Keywords: capability machines, local capabilities, uninitialized capabilities, capability safety, universal contracts, program logic, capability revocation, CHERI
Abstract.

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.

The bibtex source for this publication:
@article{DBLP:journals/pacmpl/GeorgesGSTTHDB21,
  author    = {A{\"{\i}}na Linn Georges and
               Arma{\"{e}}l Gu{\'{e}}neau and
               Thomas Van Strydonck and
               Amin Timany and
               Alix Trieu and
               Sander Huyghebaert and
               Dominique Devriese and
               Lars Birkedal},
  title     = {Efficient and provable local capability revocation using uninitialized
               capabilities},
  journal   = {Proc. {ACM} Program. Lang.},
  volume    = {5},
  number    = {{POPL}},
  pages     = {1--30},
  year      = {2021},
  url       = {https://doi.org/10.1145/3434287},
  doi       = {10.1145/3434287},
  timestamp = {Wed, 17 Feb 2021 08:54:00 +0100},
  biburl    = {https://dblp.org/rec/journals/pacmpl/GeorgesGSTTHDB21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}