RustHorn: CHC-based Verification for Rust Programs
RustHorn: CHC-based Verification for Rust Programs
复制标题
RustHorn：基于 CHC 的 Rust 程序验证
DOI：
10.1145/3462205
复制
发表时间：
2021
影响因子：
1.3
通讯作者：
Kobayashi Naoki
中科院分区：
文献类型：
--
作者：
Matsushita Yusuke;Tsukada Takeshi;Kobayashi Naoki
约束 Horn 子句 (CHC) 的可满足性约简是一种广泛研究的自动化程序验证方法。然而，当前基于 CHC 的方法对于指针操作程序来说效果不佳，尤其是那些具有动态内存分配的程序。本文提出了一种将指针操作 Rust 程序简化为 CHC 的新颖方法，它通过利用 Rust 的权限保证来清除指针和内存状态。我们将简化的 Rust 核心形式化，并证明其健全性和完整性。我们已经为 Rust 的一个子集实现了原型验证器，并确认了我们方法的有效性。
Reduction to satisfiability of constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. Current CHC-based methods, however, do not work very well for pointer-manipulating programs, especially those with dynamic memory allocation. This article presents a novel reduction of pointer-manipulating Rust programs into CHCs, which clears away pointers and memory states by leveraging Rust’s guarantees on permission. We formalize our reduction for a simplified core of Rust and prove its soundness and completeness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.