ManuelLerchner/Voblint-Verification-Master-Thesis

# Voblint ## 摘要 Voblint 是一个可重用、经过机器检查的 Isabelle/HOL 框架，用于构建、执行和验证通用的过程间抽象解释器。受 Goblint 的模块化 D/G 架构启发，它结合了对 VIMP 程序的经过验证的编译、激活局部的操作语义、可执行的方程生成、经过验证的自顶向下求解器以及端到端的源码级可靠性。 与大多数现有的形式化方法不同，Voblint 证明的是由经过验证的求解器计算出的分析结果的属性，而不是外部提供的不动点。 ## 为什么选择 Voblint？ * **计算得出的结果：** 经过验证的求解器在 Isabelle/HOL 内部计算抽象不动点。所有可靠性定理都直接应用于此计算结果。 * **设计上的通用性：** 该框架对抽象域、传递函数、拓宽策略、D/G 分析和上下文抽象都是通用的。 * **上下文敏感：** 分析由任意上下文键参数化，支持单变体、基于激活、调用字符串或自定义上下文抽象，而无需更改证明基础设施。 * **可执行：** 分析不仅是被规约出来的；它们直接在 Isabelle/HOL 中运行。 * **可视化：** 为经过认证的分析结果生成可执行的 GraphViz 输出。 ## 基础 Voblint 的灵感来源于几个互补的研究方向： * **Goblint** ([Github](https://github.com/goblint/analyzer)) – 模块化的过程间抽象解释和 D/G 分析架构。 * **带注解命令的抽象解释** ([ITP 2012](https://doi.org/10.1007/978-3-642-32347-8_9)) – Isabelle/HOL 中可重用的抽象解释。 * **经过验证的自顶向下求解器：建立对静态分析器的信心** ([CAV 2024](https://doi.org/10.1007/978-3-031-65627-9_15)) – 可执行的、经过验证的不动点求解。 * **混合流敏感的静态分析：工程模块化** ([FM 2026](https://doi.org/10.1007/978-3-032-26220-2_22)) – 构建模块化的异构分析。 ## 经过认证的执行流水线 Voblint 证明了一个连续的端到端执行逻辑。该框架弥合了具体源代码与计算出的数学不动点之间的差距： ``` VIMP Program │ ▼ Verified CFG Compilation │ ▼ Activation-local Semantics │ ▼ Generic D/G Specification │ ▼ Executable Equation Generation │ ▼ Verified TD Solver │ ▼ Computed Abstract Solution │ ▼ Collecting Semantics │ ▼ Source-Level Soundness ``` ## 通用 D/G 框架 Voblint 的分析建立在受 Goblint 模块化分析架构启发的、可重用的 **D/G 框架** 之上。Voblint 不再为每个分析单独实现求解器和证明，而是将分析拆解为： - **D** — 与程序点相关联的抽象事实， - **G** — 在程序点之间发布和消费的全局共享分析信息。 其核心抽象是 `sound_dg_spec` locale，这是对 Goblint [`Spec`](https://github.com/goblint/analyzer/blob/1ab59c9c4d9859e9135885d3c9a9aa1a8f3b677e/src/framework/analyses.ml#L168-L263)-接口 的 Isabelle/HOL 形式化。分析通过在抽象载体上提供特定于域的传递、合并和通信操作来实例化此 locale。基于此规约，该框架自动派生出： - 可执行的方程生成， - 与经过验证的自顶向下求解器的集成， - 可重用的收集语义可靠性定理， - 可重用的源码级正确性定理， - 完整的可执行分析流水线。 这种分离允许 Sign、Interval、混合的 Sign × Interval 以及未来的分析重用相同的已验证基础设施，而只需改变特定于域的分析逻辑。 可执行前端由 `Exec_DG_Bridge.thy` 提供，它实现了： - D/G 状态的可执行有限映射表示， - 精化态射 `fun_of_dg_st`， - 通过 `dg_gen_of` 生成可执行方程， - 通过 `part_post_solution_dg_st_to_abs` 将求解器计算的结果传输到抽象后解。 因此，添加新的 D/G 分析仅需实例化 `sound_dg_spec`；方程生成、求解器执行和端到端正确性证明均可从通用框架中继承。 ## 扩展 Voblint 该框架设计为高度可扩展的。无需从零开始证明一个新的分析，您只需提供特定于域的组件： | 扩展 | 所需工作 | | ----------------------------- | ------------------------------------- | | **抽象域** | 定义格和具体化 (γ) | | **传递函数** | 证明局部可靠性 | | **Goblint D/G 规范** | 实例化通用接口 | | **上下文抽象** | 定义上下文键 | | **拓宽** | 提供拓宽/收窄算子 | ## 仓库结构 ``` VIMP │ Source language ▼ CFG │ Compilation & semantics ▼ Analysis │ Generic D/G framework ▼ Formalization │ End-to-end soundness ▼ Examples Executable analyses & GraphViz ``` * **`VIMP/`**：语法、过程、全局/局部变量、小步语义 * **`CFG/`**：过程感知的 CFG 编译、激活局部追踪和收集语义 * **`Analysis/`**：通用 D/G 框架、域、求解器接口、可执行分析 * **`Formalization/`**：端到端求解器、收集语义和源码级可靠性 * **`Examples/`**：可执行运行、旗舰演示和 GraphViz 工具 * **`vendor/`**：经验证的 TD 求解器子模块和 Isabelle2025 补丁 * **`docs/`**：证明概述、阶段追踪和智能体工作流笔记 ## 构建说明 ### 前置条件 * **[Isabelle](https://isabelle.in.tum.de/) 2025**（或更新版本） * **[AFP](https://www.isa-afp.org/)**（Formal Proofs 归档）检出包含 `Root_Balanced_Tree` 和 `Dijkstra_Shortest_Path`。 * `make`、`git` 和标准的 POSIX 工具。 ### 构建 将 `AFP` 设置为您本地的 AFP `thys/` 目录（默认为 `~/afp/thys`）： ``` # 1. 初始化 TD solver 子模块并应用兼容性补丁 make vendor # 2. 构建主 formalization 会话（sorry-free） make AFP=/path/to/afp/thys build # 3. 启动 jEdit 并预加载会话根目录 make AFP=/path/to/afp/thys jedit ``` *注意：有关使用 Isabelle/Q 和无头 Isabelle/R 进行智能体辅助开发的详细信息，请参见 `docs/ISABELLE_AGENT_NOTES.md` 和提供的 `./scripts/setup.sh`。* ### 将 TD 求解器作为本地 vendor 内容引入 上游：[stilscher/td-verification](https://github.com/stilscher/td-verification)。 通过私有 fork 作为子模块引入： [`ManuelLerchner/td-verification`](https://github.com/ManuelLerchner/td-verification) （CI + 本地访问）。GitHub Actions 无法使用默认的 `GITHUB_TOKEN` 克隆该 fork；请添加一个具有 `repo` 范围的经典 PAT 作为仓库密钥 `SUBMODULES_TOKEN`，或者将此 fork 设为公开。一个较小的 Isabelle2025 兼容性更改位于 `vendor/td-verification.patch` 中；`make vendor` 会应用它（幂等）。 ### 智能体辅助开发 证明开发实验使用 [Isabelle/Q](https://github.com/awslabs/AutoCorrode/tree/main/iq) (I/Q)，这是一个用于 Isabelle/jEdit 的 MCP 服务器，允许编码智能体编辑理论、查询证明 状态、运行 Sledgehammer 并探索策略。遵循 Kappelmann 等人的自动形式化工作流， [*Just Type It in Isabelle!*](https://arxiv.org/abs/2604.15713) (arXiv:2604.15713, 2026), §6.1。参见 `AGENTS.md` 和 `docs/ISABELLE_AGENT_NOTES.md`。 | 脚本 | 角色 | | --- | --- | | `./scripts/setup.sh` | 一次性引导：子模块、虚拟环境、I/Q 插件（使用 `--no-iq` 跳过） | | `./scripts/start-iq.sh` | 端口 8765 上的 Isabelle/jEdit + I/Q | | `./scripts/start-ir.sh` | 端口 9148 上的无头 Isabelle/R MCP | | `./scripts/start-both.sh` | I/R 后台 + I/Q 前台；Ctrl+C 会同时终止两者 | `start-ir.sh` 通过 `isabelle components -u` 将 `vendor/td-verification` 注册为 Isabelle 组件。这种持久且幂等的注册允许 I/R 的 `ML_process` 解析父会话 `TD`；I/R 启动器仅接受一个显式的会话目录。如果需要，请使用以下命令移除注册： ``` isabelle components -x "$(pwd)/vendor/td-verification" ```

标签：Isabelle/HOL, 云安全监控, 定理证明, 形式化验证, 抽象解释, 编译器, 网络安全研究, 静态分析