一句话：提出并形式化 StkTokens 调用约定，借助硬件不可复制的线性 capability，证明其在 capability 机器上保证良括号控制流与局部状态封装。
论文研究如何在 capability 机器上通过调用约定保证控制流良好嵌套，并封装局部状态。作者提出 StkTokens：一种基于线性 capability 的调用约定，利用硬件保证这类 capability 不可复制，从而约束返回地址与栈访问，防止越权跳转和栈数据泄漏。为论证其有效性，作者形式化该约定，并提出“完全抽象 overlay 语义”作为证明方法，用其证明 StkTokens 确实实施良括号控制流和局部状态封装。结果是一个可证明安全的新调用约定，以及一种用于此类底层机制验证的语义框架。
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{paperbot688,
title = {StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities},
author = {Lau Skorstengaard and Dominique Devriese and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290332}
}