IsaBIL：基于 Isabelle/HOL 的二进制验证（不）正确性框架（扩展版）
编程语言
2025-04-24 v1
摘要
本文提出了 IsaBIL，这是一个基于广泛使用的二进制分析平台（BAP）的 Isabelle/HOL 二进制分析框架。具体而言，在 IsaBIL 中，我们形式化了 BAP 的中间语言，即 BIL，并将其集成到霍尔逻辑（用于实现正确性证明）以及不正确性逻辑（用于实现不正确性证明）。IsaBIL 继承了 BAP 的全部灵活性，使我们能够验证针对广泛语言（C、C++、Rust）、工具链（LLVM、Ghidra）和目标架构（x86、RISC-V）的二进制文件，并且可以在二进制文件不可获取源代码的情况下使用。为使验证具有可行性，我们开发了若干大步规则，将 BIL 现有的小步规则在不同抽象层次上组合，以支持复用。我们为 RISC-V 指令（我们的主要目标架构）开发了高级推理规则，以进一步优化验证。此外，我们开发了 Isabelle 证明策略，利用 C 二进制文件在 RISC-V 上的常见模式，自动处理大量证明目标（通常有数百个）。IsaBIL 包括一个基于 Isabelle/ML 的 BIL 程序解析器，允许从 BAP 输出自动生成关联的 Isabelle/HOL 程序 locale。综上所述，IsaBIL 提供了一个高度灵活的程序二进制证明环境。作为示例，我们证明了关键性格准则（Joint Strike Fighter coding standards）和 MITRE 数据库中的正确性。
关键词
引用
@article{arxiv.2504.16775,
title = {IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL (Extended Version)},
author = {Matt Griffin and Brijesh Dongol and Azalea Raad},
journal= {arXiv preprint arXiv:2504.16775},
year = {2025}
}