一句话：提出 Hetrify，将异构程序或不可验证片段编译为二进制并语义等价转换为可验证 C 代码，在 RISC-V 上实现高效验证。
当代软件常包含闭源库、嵌入式汇编片段和多语言模块等异构组件，给程序验证带来显著挑战，目前缺乏成熟可用的方法。本文提出一种通用验证方法：先将整个程序或其中不可验证的片段编译为二进制，并在保证语义等价的前提下把这些二进制转换为可验证的 C 代码，随后利用现有 C 验证工具完成验证。该方法理论上适用于任何可编译为二进制代码的异构程序，不受具体编程语言限制。作者基于 RISC-V 架构实现了工具 Hetrify，并给出严格数学证明，确保转换所得 C 程序与原程序之间操作语义等价。评估在 130 个程序上进行，包括 100 个汇编程序和 30 个缺少关键函数源码的大型异构程序，结果表明该方法有效。
The heterogeneous nature of contemporary software, comprising components like closed-source libraries, embedded assembly snippets, and modules written in multiple programming languages, leads to significant verification challenges. Currently, there are no mature and available methods to effectively address such problems. To bridge this gap, we propose a verification approach capable of effectively verifying heterogeneous programs. This approach is universally applicable. It theoretically supports the verification of any heterogeneous program that can be compiled into binary code, without being constrained by any specific programming language. The approach begins by compiling the entire program or its unverifiable segments into binary format. Under guarantees of semantic equivalence, these binaries are converted into verifiable C code, which can then be verified using existing C verification tools. Based on the RISC-V architecture, we developed the Hetrify tool to implement this verification approach. The tool is supported by rigorous mathematical proofs to ensure operational semantic equivalence between the converted C programs and their original counterparts. To validate our approach, we conducted verification experiments on 130 programs, including 100 assembly programs and 30 large heterogeneous programs with missing critical function source code, demonstrating the effectiveness of our approach.
DOI 原文 ·
@inproceedings{paperbot8857,
title = {Hetrify: Efficient Verification of Heterogeneous Programs on RISC-V},
author = {Yiwei Li and Liangze Yin and Wei Dong and Jiaxin Liu and Yanfeng Hu and Shanshan Li},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00081}
}