使用 HolBA 中的符号执行对 RISC-V 二进制程序进行可靠性验证
计算机科学中的逻辑
2025-03-19 v1
摘要
许多类型的形式化验证都是针对抽象的高级程序表示来建立性质，这与运行时程序之间存在很大的差距。虽然可以通过精化等技术有时缩小差距，但已验证程序的可信计算基可能仍包含编译器和内联汇编。相比之下，针对 RISC-V 等指令集架构（ISA）的二进制程序验证可以确保机器码在真实硬件上按预期行为。虽然二进制分析对于确保软件系统的可靠性有用且有时甚至是必要的，但现有工具缺乏形式化基础或缺乏验证的自动化。我们提出了一种基于 HOL4 定理证明器和 HolBA 二进制分析库的工作流程和工具链，用于对 RISC-V 二进制程序进行可靠的形式化验证。该工具链通过对 HolBA 中间语言 BIR 中的程序进行前向符号执行来自动化二进制契约的证明。我们通过验证 RISC-V 二进制程序的正确性来验证了该工具链，包括（1）ChaCha20 流密码的一个实现，以及（2）操作系统内核中上下文切换的手写汇编代码。
引用
@article{arxiv.2503.14135,
title = {Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA},
author = {Karl Palmskog and Andreas Lindner and Scott Constable and Roberto Guanciale and Hamed Nemati},
journal= {arXiv preprint arXiv:2503.14135},
year = {2025}
}
备注
12 pages, 7 figures, 1 table