一句话：提出基于 Kripke 规约单子构造符号执行验证器并证明其可靠性的系统方法，在 Katamaran 中全验证实现。
验证基于符号执行的程序验证器的可靠性十分困难，尤其当工具需在证明助手之外使用、无法依赖浅嵌入断言逻辑与元编程时。本文提出一套系统化方法：先在 specification monad 中以对象语言解释器实现浅层验证条件生成器，其抽象接口包含天使与恶魔非确定性；再在符号 specification monad 中实现类似解释器以构造符号执行器，该 monad 位于按作用域变量与路径条件做 Kripke 索引的宇宙中；最后用 Kripke 逻辑关系关联两个执行器，把符号执行的可靠性归约到浅层执行的可靠性。作者在 ISA 安全保证验证工具 Katamaran 中实践该技术，结合公理化分离逻辑与基于 Iris 的公理实现，获得全验证工具，并在实用性与效率上取得良好结果。
Verifying soundness of symbolic execution-based program verifiers is a significant challenge. This is especially true if the resulting tool needs to be usable outside of the proof assistant, in which case we cannot rely on shallowly embedded assertion logics and meta-programming. The tool needs to manipulate deeply embedded assertions, and it is crucial for efficiency to eagerly prune unreachable paths and simplify intermediate assertions in a way that can be justified towards the soundness proof. Only a few such tools exist in the literature, and their soundness proofs are intricate and hard to generalize or reuse. We contribute a novel, systematic approach for the construction and soundness proof of such a symbolic execution-based verifier. We first implement a shallow verification condition generator as an object language interpreter in a specification monad, using an abstract interface featuring angelic and demonic nondeterminism. Next, we build a symbolic executor by implementing a similar interpreter, in a symbolic specification monad. This symbolic monad lives in a universe that is Kripke-indexed by variables in scope and a path condition. Finally, we reduce the soundness of the symbolic execution to the soundness of the shallow execution by relating both executors using a Kripke logical relation. We report on the practical application of these techniques in Katamaran, a tool for verifying security guarantees offered by instruction set architectures (ISAs). The tool is fully verified by combining our symbolic execution machinery with a soundness proof of the shallow verification conditions against an axiomatized separation logic, and an Iris-based implementation of the axioms, proven sound against the operational semantics. Based on our experience with Katamaran, we can report good results on practicality and efficiency of the tool, demonstrating practical viability of our symbolic execution approach.
@article{paperbot1492,
title = {Verified symbolic execution with Kripke specification monads (and no meta-programming)},
author = {Steven Keuchel and Sander Huyghebaert and Georgy Lukyanov and Dominique Devriese},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547628}
}