一句话：为带局部能力的能力机器建立逻辑关系，证明控制流正确性与局部状态封装。
能力机器在机器级提供安全保证，是能够可证明地实施控制流正确性和局部状态封装等性质的安全编译方案的重要目标。本文形式化了一个具有局部能力的代表性能力机器，并研究了一种新颖的调用约定。作者定义了一个逻辑关系，从语义上刻画硬件提供的保证（一种能力安全），并用其证明控制流正确性与局部状态封装。该逻辑关系不局限于特定调用约定，可用于推理任意程序。
Capability machines provide security guarantees at machine level which makes them an interesting target for secure compilation schemes that provably enforce properties such as control-flow correctness and encapsulation of local state. We provide a formalization of a representative capability machine with local capabilities and study a novel calling convention. We provide a logical relation that semantically captures the guarantees provided by the hardware (a form of capability safety) and use it to prove control-flow correctness and encapsulation of local state. The logical relation is not specific to our calling convention and can be used to reason about arbitrary programs.
@article{paperbot695,
title = {Reasoning about a Machine with Local Capabilities},
author = {Lau Skorstengaard and Dominique Devriese and Lars Birkedal},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {42},
number = {1},
year = {2019},
doi = {10.1145/3363519}
}