一句话：提出定向能力使能力机器调用约定更高效，并用一元/二元逻辑关系与编译器完全抽象证明时间栈安全性，Coq机械化。
能力机器是一种支持细粒度权限分离的CPU，其形式模型此前主要关注局部状态封装与良括号控制流两种栈安全性质。本文引入一种新型的定向能力（directed capabilities），使先前的调用约定更加高效。与以往仅关注完整性不同，本文同时考虑机密性，分别用一元逻辑关系推理完整性、二元逻辑关系推理机密性，二者均足以表达时间栈安全。为证明栈安全对一大类程序成立，作者进一步证明了一个编译器的完全抽象：从将调用约定内化为单步调用并显式跟踪调用栈与帧生命周期的overlay语义，编译到基础能力机器。所有结果均在Coq中机械化。
Capability machines are a type of CPUs that support fine-grained privilege separation using capabilities , machine words that include forms of authority. Formal models of capability machines and associated calling conventions have so far focused on establishing two forms of stack safety properties, namely local state encapsulation and well-bracketed control flow. We introduce a novel kind of directed capabilities and show how to use them to make an earlier suggested calling convention more efficient. In contrast to earlier work on capability machine models we do not only consider integrity properties but also confidentiality properties; we provide a unary logical relation to reason about the former and a binary logical relation to reason about the latter, each expressive enough to reason about temporal stack safety. While the logical relations are useful for reasoning about concrete examples, they do not on their own demonstrate that stack safety holds for a large class of programs. Therefore, we also show full abstraction of a compiler from an overlay semantics that internalizes the calling convention as a single call step and explicitly keeps track of the call stack and frame lifetimes to a base capability machine. All results have been mechanized in Coq.
@article{paperbot1511,
title = {Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities},
author = {Aïna Linn Georges and Alix Trieu and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527318}
}