发表机构
Barkhausen Institute; Kernkonzept GmbH（巴特豪森研究所; Kernkonzept有限公司）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
Corten是基于Iris分离逻辑的Rust程序基础验证框架，在Rocq中实现了Rust表层语义，可缩小证明规模并验证伙伴分配器的内存安全，为跨软硬件的端到端验证奠基。
AI 中文摘要
我们在Rocq定理证明器中提出了Corten，这是一个基于Iris分离逻辑框架的Rust程序基础验证框架。Corten提供了首个在证明助手内实现的表层Rust形式语义，附带程序逻辑，直接基于《Rust参考手册》：它将类型化高级中间表示（THIR）深度嵌入Rocq，并将Rust的动态语义形式化为最弱前置条件谓词变换器演算。由于在THIR而非内部编译器表示上运行，Corten的证明目标显示THIR抽象语法树（AST），其可漂亮打印为表层Rust代码，使验证贴近源代码，便于代码演进时的维护。在该语义之上，Corten开发了程序逻辑和语法导向的证明自动化层；程序逻辑包含去函数化的延续栈，可保持证明目标为一阶且紧凑。我们针对交互树语义按构造逐步建立了可靠性。一个综合测试套件显示，与原始语义证明相比，证明规模缩小了2至4倍。我们还通过伙伴分配器案例研究展示了Corten，验证了分配和释放函数的内存安全性，为在跨越软硬件边界的共享Rocq语义基础上进行端到端验证奠定了基础。
英文摘要
We present Corten, a foundational verification framework for Rust programs in the Rocq theorem prover, built on the Iris separation logic framework. Corten provides the first semantics of surface-level Rust mechanized in a proof assistant with an attached program logic, directly grounded in the Rust Reference: it deeply embeds the Typed High-level Intermediate Representation (THIR) into Rocq and formalises Rust's dynamic semantics as a weakest-precondition predicate transformer calculus. By operating at THIR rather than on internal compiler representations, Corten proof goals display the THIR AST, which pretty-prints to surface Rust, keeping verification close to the source code and facilitating maintainability as code evolves. Atop this semantics, Corten develops a program logic and a syntax-directed proof automation layer; the program logic includes defunctionalized continuation stacks that keep proof goals first-order and compact. Soundness is established incrementally, construct by construct, against an interaction-trees denotation. A synthetic test suite demonstrates a two-to-four times reduction in proof size compared to raw semantic proofs. We further showcase Corten on a buddy allocator case study, verifying memory safety of the allocation and deallocation functions, laying the groundwork for end-to-end verification in a shared Rocq semantic foundation spanning hardware-software boundaries.
Comments41 pages, 13 figures
