一句话：CopilotVerifier 为 Copilot 编译器输出的 C 监视器生成与源语义互模拟的正确性证明。
在安全攸关系统中使用运行时验证时，监视器代码本身的正确性至关重要。Copilot 框架通过从 Haskell 嵌入式 DSL 自动生成 C 监视器程序来实现这一目标，但人工审计者很难确信编译后的监视器不会崩溃，且其行为符合 Copilot 语义。本文提出 CopilotVerifier，它与 Copilot 编译器并行运行，为编译输出生成正确性证明。该证明表明：给定 Copilot 监视器与其编译形式在等价输入上产生等价输出，并且二者要么在相同情形下崩溃，要么都不会崩溃。证明以互模拟的形式给出，并被分解为一组验证条件；实现借助两项 SMT 支持的技术——面向 LLVM 的 Crucible 符号执行库与 What4 求解器接口库。结果表明，在现有工具之上构建即可用适中代价显著提升编译器保证，为实现能被人工审计者信服的形式化保证论证这一最终目标铺平了道路。
When runtime verification is used to monitor safety-critical systems, it is essential that monitoring code behaves correctly. The Copilot runtime verification framework pursues this goal by automatically generating C monitor programs from a high-level DSL embedded in Haskell. In safety-critical domains, every piece of deployed code must be accompanied by an assurance argument that is convincing to human auditors. However, it is difficult for auditors to determine with confidence that a compiled monitor cannot crash and implements the behavior required by the Copilot semantics. In this paper we describe CopilotVerifier, which runs alongside the Copilot compiler, generating a proof of correctness for the compiled output. The proof establishes that a given Copilot monitor and its compiled form produce equivalent outputs on equivalent inputs, and that they either crash in identical circumstances or cannot crash. The proof takes the form of a bisimulation broken down into a set of verification conditions. We leverage two pieces of SMT-backed technology: the Crucible symbolic execution library for LLVM and the What4 solver interface library. Our results demonstrate that dramatically increased compiler assurance can be achieved at moderate cost by building on existing tools. This paves the way to our ultimate goal of generating formal assurance arguments that are convincing to human auditors.
@article{paperbot1921,
title = {Trustworthy Runtime Verification via Bisimulation (Experience Report)},
author = {Ryan G. Scott and Mike Dodds and Ivan Perez and Alwyn E. Goodloe and Robert Dockins},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607841}
}