kth-step/HolBA

# HolBA - HOL 中的二进制分析 [][workflow-link] HolBA 是一个基于 HOL4 定理证明器的库，提供了 用于分析和形式化证明使用 ARMv8、RISC-V 和 Cortex-M0 指令集的 二进制格式程序属性的工具。 HolBA 的应用包括 ARMv8 和 RISC-V 二进制文件的契约自动验证， 以及 Cortex-M0 的执行时间界限验证，所有这些都基于 [L3 language](https://acjf3.github.io/l3/index.html) 中相应的形式化 ISA 规范。 HolBA 分析使用一种称为 BIR 的中间语言，该语言抽象了许多 ISA 细节。 有关更多技术细节，请参阅 [publications](#related-publications)， 以及针对特定 ISA 的二进制分析 [examples](examples)。 ## 构建 HolBA 使用 HOL4 捆绑的 `Holmake` 工具构建。 ### 依赖项 - [HOL4](https://github.com/HOL-Theorem-Prover/HOL)，标签 `trindemossen-2`。 - [Poly/ML](https://github.com/polyml/polyml)，5.9.2 - 或者，Poly/ML 5.7.1（Ubuntu 24.04 打包的版本） - [Z3](https://github.com/Z3Prover/z3)，4.14.1 ### 使用现有的 HOL4 安装进行构建 如果您已经安装了 HOL4 并且 `Holmake` 在您的路径中， 您可以执行以下操作来构建整个库（不包括示例）： ``` git clone https://github.com/kth-step/HolBA.git cd HolBA Holmake ``` 要构建示例，您需要设置 Z3 二进制文件的路径，然后在 `examples` 目录中运行 `Holmake`： ``` export HOL4_Z3_EXECUTABLE=/path/to/z3 cd examples Holmake ``` ### 从头开始构建 为了方便起见，HolBA 提供了一些脚本，用于从 bash shell 引导带有 HOL4 和 Z3 的环境。 ``` git clone https://github.com/kth-step/HolBA.git cd HolBA # This sets up all dependencies in this HolBA # directory (${HOLBA_DIR}/opt). It downloads and # builds polyml and HOL4 for example. ./scripts/setup/install_all.sh # In order to create a configuration file with # the directories for the installed tools, # execute the following line ./configure.sh # For convenience and indepence of make, this command # augments the environment with ${HOLBA_*} variables # as well as the ${PATH} variable. Now calls to Holmake # use the installed instance of HOL4 in the opt directory. # Furthermore, some tools require these variables to # run properly. It has to be run for each new shell. source env.sh # This builds the whole library, excluding examples ${HOLBA_HOLMAKE} # This builds the examples cd examples ${HOLBA_HOLMAKE} ``` ## 库组织 ### 目录结构 - `doc`：关于 HolBA 和 BIR 的文档 - `examples`：HolBA 的应用 - `arm8`：指定和验证 ARMv8 程序的示例，包括使用符号执行自动进行契约证明 - `arm_cm0`：指定和验证 Cortex-M0 程序的示例，包括使用符号执行自动进行执行时间界限证明 - `bir`：使用中间 BIR 语言进行规范和验证的示例 - `riscv`：指定和验证 RISC-V 程序的示例，包括使用符号执行自动进行契约证明 - `scripts`：CI 和安装脚本 - `src`：库源代码 - `extra`：通用理论和库 - `shared`：工具间共享的库 - `convs`：转换策略 (conversion tactics) - `l3-machine-code`：来自 HOL4 示例的 L3 模型扩展 - `smt`：通过 SMTLIB 连接 SMT 求解器的自定义接口（目前是 Z3） - `sml-simplejson`：JSON 解析器 - `theory`：特定领域理论 - `bir`：核心 BIR 语言 - `bir-support`：BIR 的扩展和支持理论 - `models`：额外的机器模型 - `program_logic`：用于非结构化代码的抽象 Hoare 风格逻辑 - `tools`：`src/tools` 中工具库的理论 - `tools`：特定领域的库 - `backlifter`：用于从 BIR 契约获取 ISA 级契约的实用程序 - `cfg`：控制流图实用程序 - `comp`：契约组合 - `compute`：在 HOL4 中使用 `cv_compute` 的实用程序 - `exec`：具体执行 - `lifter`：从二进制 ISA 代码到 BIR 的转换 - `pass`：Passification 实用程序 - `scamv`：抽象侧信道模型验证框架 - `symbexec`：BIR 的符号执行 - `wp`：最弱前置条件传播 ### 工具状态 - `tools/backlifter`： * 产生证明 (Proof-producing) * 接口清晰 * 实验性实现 * 在示例中使用 * 支持：ARMv8、RISC-V - `tools/cfg`： * 非产生证明 * 尚无清晰接口 * GraphViz 导出器可用 - `tools/comp`： * 产生证明 * 接口尚可 * 实验性实现 * 需要文档 - `tools/exec`： * 产生证明 * 不稳定的 BIR 求值实用程序（尚无清晰接口） * 相当易于使用 - `tools/lifter`： * 产生证明 * 稳定 * 在示例中广泛使用 * 支持：ARMv8、Cortex-M0、带时钟周期计数器的 Cortex-M0、RISC-V - `tools/pass`： * 非产生证明 * 实验性的 SSA Passification 转换 - `tools/scamv`： * 适用于小型程序 * 包含选定的缓存侧信道模型 - `tools/symbexec`： * 产生证明 * 关键库函数的接口 * 可用于自动 BIR 契约证明 - `tools/wp`： * 产生证明 * 接口开发中 * 相当稳定 * 包含替换简化的原型 ### 在基于 HOL4 的项目中使用 HolBA 要在基于 HOL4 的项目中依赖 HolBA，我们建议设置您的项目 以使用 `Holmake` 进行构建，然后在您的 `Holmakefile` 中添加引用， 指向您使用的 HolBA 模块所在的目录（相对于 变量 `HOLBADIR`）。 例如，如果您依赖 `src/theory/bir` 和 `src/theory/bir-support` 目录中的模块，您的 `Holmakefile` 可能如下所示： ``` INCLUDES = $(HOLBADIR)/src/theory/bir $(HOLBADIR)/src/theory/bir-support all: $(DEFAULT_TARGETS) .PHONY: all ``` 然后要构建您的项目，您可以导出 HolBA 代码库副本的路径 并在包含 `Holmakefile` 的目录中运行 `Holmake`，这将递归地 构建所有必需的理论： ``` export HOLBADIR=/path/to/holba Holmake ``` ## 错误报告 请在 [issue tracker](https://github.com/kth-step/HolBA/issues) 中报告任何错误或功能请求。 ## 贡献 欢迎以 [pull requests](https://github.com/kth-step/HolBA/pulls) 的形式贡献新功能和错误修复， 但在提交之前请务必阅读 [contribution guide](CONTRIBUTING.md)。 ## 相关出版物 - A. Lindner, K. Palmskog, S. Constable, M. Dam, R. Guanciale and H. Nemati, **"Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification"**, in International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 147-172, 2026. [Link](https://arxiv.org/abs/2304.08848v2). _（使用符号执行自动进行二进制验证）_ - D. Lundberg, R. Guanciale, A. Lindner and M. Dam, **"Hoare-Style Logic for Unstructured Programs"**, Journal of Logical and Algebraic Methods in Programming, vol. 149, 2025. [Link](https://doi.org/10.1016/j.jlamp.2025.101099). _（用于验证分解的程序逻辑）_ - P. Buiras, H. Nemati, A. Lindner, and R. Guanciale, **"Validation of Side-Channel Models via Observation Refinement"**, in International Symposium on Microarchitecture, pp. 578-591, 2021. [Link](https://doi.org/10.1145/3466752.3480130). _（验证抽象侧信道模型的框架）_ - H. Nemati, P. Buiras, A. Lindner, R. Guanciale and S. Jacobs, **"Validation of Abstract Side-Channel Models for Computer Architectures"**, in International Conference on Computer Aided Verification, pp. 225-248, 2020. [Link](https://doi.org/10.1007/978-3-030-53288-8_12). _（验证抽象侧信道模型的框架）_ - A. Lindner, R. Guanciale and R. Metere, **"TrABin : Trustworthy analyses of binaries"**, Science of Computer Programming, vol. 174, pp. 72-89, 2019. [Link](https://doi.org/10.1016/j.scico.2019.01.001). _（HOL4 中具有最弱前置条件的产生证明的二进制分析框架）_ - D. Lundberg, **"Provably Sound and Secure Automatic Proving and Generation of Verification Conditions"**, Master Thesis, 2018. [Link](http://urn.kb.se/resolve?urn=urn%3Anbn%3Ase%3Akth%3Adiva-239441). - R. Metere, A. Lindner and R. Guanciale, **"Sound Transpilation from Binary to Machine-Independent Code"**, in 20th Brazilian Symposium on Formal Methods, pp. 197-214, 2017. [Link](https://doi.org/10.1007/978-3-319-70848-5_13). _（HOL4 中间语言的形式化及产生证明的 Lifter）_

标签：ARMv8, BIR, Cortex-M0, HOL4, HolBA, L3语言, RISC-V, SMT求解器, TLS抓取, Z3, 中间语言, 二进制分析, 云安全监控, 云安全运维, 交互式定理证明器, 可配置连接, 合约验证, 固件分析, 定理证明, 嵌入式安全, 形式化方法, 形式化验证, 执行时间分析, 指令集架构, 时间边界验证, 程序分析, 符号执行, 软件安全, 静态分析, 高可信度