一句话：提出未初始化能力及其机器化验证程序逻辑，在不暴露内存初值的前提下实现高效局部能力撤销并证明能力安全。
能力机通过携带权限的值（能力）实现细粒度特权隔离；CHERI 的局部能力可用于低成本的能力撤销，但需清空大量栈内存，实践中不现实。本文提出未初始化能力：一种表示对内存块读写权限、却不暴露其初始内容的新型能力，从而避免清空内存。作者为带该特性的能力机程序设计了机器化验证的程序逻辑，并以通用契约形式形式化并证明能力安全，使不可信代码的推理成为可能。作者还用未初始化能力改进了先前提出的安全调用约定，使其高效，并用该程序逻辑证明其安全性。最后在 CHERI 能力机上完成了概念验证实现。
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.
@article{paperbot1162,
title = {Efficient and provable local capability revocation using uninitialized capabilities},
author = {Aïna Linn Georges and Armaël Guéneau and Thomas Van Strydonck and Amin Timany and Alix Trieu and Sander Huyghebaert and Dominique Devriese and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434287}
}