一句话：提出在 Coq 中以策略形式实现的编译器，将高阶协程自动可验证地编译为显式状态机。
安全关键网络协议常包含嵌套状态机，手工低层实现易隐藏缺陷，而依赖线程等高层抽象又可能牺牲性能与平台 ABI 兼容性。本文提出一种基于编译器的技术：用 freer monad 将嵌套协程写成自然的高层协议代码，再自动编译为带显式状态的低层代码。编译器实现在 Coq 证明助手中，作为策略将编译过程组织为寻找源程序与目标程序等价证明的搜索；因此可安全地通过新提示扩展，例如支持协程查找的数据结构。案例研究实现足以支持主流浏览器的 TLS 核心，提取出的 Haskell 代码达到合理性能。
One of the biggest implementation challenges in security-critical network protocols is nested state machines. In practice today, state machines are either implemented manually at a low level, risking bugs easily missed in audits; or are written using higher-level abstractions like threads, depending on runtime systems that may sacrifice performance or compatibility with the ABIs of important platforms (e.g., resource-constrained IoT systems). We present a compiler-based technique allowing the best of both worlds, coding protocols in a natural high-level form, using freer monads to represent nested coroutines , which are then compiled automatically to lower-level code with explicit state. In fact, our compiler is implemented as a tactic in the Coq proof assistant, structuring compilation as search for an equivalence proof for source and target programs. As such, it is straightforwardly (and soundly) extensible with new hints, for instance regarding new data structures that may be used for efficient lookup of coroutines. As a case study, we implemented a core of TLS sufficient for use with popular Web browsers, and our experiments show that the extracted Haskell code achieves reasonable performance.
@article{paperbot1559,
title = {Certifying derivation of state machines from coroutines},
author = {Mirai Ikebuchi and Andres Erbsen and Adam Chlipala},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498685}
}