一句话：提出并形式化 StkTokens 调用约定，用线性 capability 在能力机器上保证良括号控制流与局部状态封装。
论文研究如何在 capability 机器上以可证明的方式保证良括号控制流和局部状态封装，提出新的调用约定 StkTokens。其核心是线性 capability：硬件保证这类 capability 不能被复制，从而可在调用与返回时安全地传递和撤销栈 token。作者形式化了该调用约定，并提出一种“完全抽象叠加语义”（fully abstract overlay semantics），用于证明它确实强制良括号控制流和局部状态封装。结果表明，在该语义下，程序无法绕过受保护的调用边界或访问被封装的局部状态，为 capability 架构上的安全调用约定提供了可验证基础。
Abstract We propose and study StkTokens: a new calling convention that provably enforces well-bracketed control flow and local state encapsulation on a capability machine. The calling convention is based on linear capabilities: a type of capabilities that are prevented from being duplicated by the hardware. In addition to designing and formalizing this new calling convention, we also contribute a new way to formalize and prove that it effectively enforces well-bracketed control flow and local state encapsulation using what we call a fully abstract overlay semantics.
@article{paperbot1238,
title = {StkTokens
<i>: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities</i>},
author = {LAU SKORSTENGAARD and DOMINIQUE DEVRIESE and LARS BIRKEDAL},
journal = {Journal of Functional Programming},
volume = {31},
year = {2021},
doi = {10.1017/s095679682100006x}
}