「AI Agent 挖洞」h5i 全拆解：Agent 浏览器红队 + Lean 4 形式化验证
原创
句芒安全实验室
句芒安全实验室
句芒安全实验室
2026年10月9日 12:31
上海
在小说阅读器读本章
去阅读
在公众号小说中沉浸阅读
一个正在发生的变化
过去你要测一个 Web 站点的漏洞，流程大概是固定的：开 Burp，配代理，手动点页面，抓包，改包，重放，对比。人来做，慢，但每一步都可控。
现在多了一条路：让 AI Agent 自己去开浏览器、抓流量、改请求。 这条路的诱惑很明显——快，而且能规模化；风险也很明显——Agent 会跑飞，会把你没授权的请求发出去，会把你的登录凭证带出沙箱。
h5i 这个项目，就是冲这条路的两个老大难来的。
它是什么
一句话：h5i 是「Agent 原生的 Web 安全工作站」，让 AI Agent 一边挖洞、一边用 Lean 4 证明代码正确。
它的定位是双轨的：
- 找 bug（红队）：给 AI Agent 一套无头浏览器 + 原生 HTTP 流量控制，在可配置的沙箱里探索站点、拦截请求、挖漏洞。官方点名适合「漏洞赏金、渗透测试、CI 回归」；
- 证明正确（形式化验证）：把后端建在
h5i-app（一个基于 Axum 的 Rust 框架）上，用 Lean 4 形式化验证应用逻辑，从租户隔离、授权一直证到核心业务状态不变量。
我核实时的数据（2026-10-09）：仓库 h5i-dev/h5i，693 个 star、66 个 fork、13 个未关 issue，Rust 写的，Apache-2.0，2026-03-11 建仓，最新推送就是今天。它同时挂着 Trendshift 的每日趋势徽章。
为什么 Web 安全需要「Agent 原生」
给 AI Agent 一把浏览器，和给人一把浏览器，是两码事。
人测站点，凭经验判断「这个链接该不该点、这个请求该不该改」；AI Agent 没有这种判断力，它只会照着目标往前冲。它跑飞了会做三件危险的事：发你没授权的请求、把页面里的恶意指令当成命令执行、把你的凭证和 cookie 泄露出去。
现有的浏览器自动化工具（Playwright、Puppeteer）是给「人写脚本」设计的，不是给「Agent 现场决策」设计的。它们不管网络策略、不留完整会话记录、也没有内置的 HTTP 改包工具。
h5i 的答案是把这三件事都做进一个 CLI 里。
亮点一：自带轻量浏览器，抓包改包重放一条龙
h5i 最核心的一块，是它自带一个轻量的 Rust 浏览器。Agent 读页面、点元素、抽取结构化数据，全走一条命令：
h5i browser open https://docs.rs/ --allow docs.rs
h5i browser snapshot # 页面大纲，带 @ref 句柄
h5i browser click @e3
h5i browser extract '{\"titles\": [\"h2\"]}' # 结构化抽取
h5i browser read https://docs.rs/ # 单页读取，不留会话
因为浏览器自己管着网络层，Agent 可以直接对 HTTP 流量做四件事：抓、看、改、比。
h5i browser open https://target.example --capture --allow target.example
h5i websec requests # 列出请求和 ID
h5i websec show req_42 --raw # 看单条原始请求
h5i websec replay req_42 --set query.id=456 # 改参数重发
h5i websec diff res_42 res_43 # 对比两次响应
h5i recon endpoints --state confirmed # 每个发现都标出证据
这里有一个设计细节值得注意：一个 session 把「页面状态 + cookie jar + 网络策略 + 请求记录」捆在一起。Agent 的每一次操作都在一个有边界的会话里，而不是散落在一堆进程里。需要完整 Chromium 的站点，走 h5i browser proxy，把代理套在 Chromium 前面，网络层的抓改重放还是同一套。
亮点二：沙箱 + 可审计，Agent 跑飞也能收场
让 Agent 自己跑，最大的问题是它可能做危险操作。h5i 给了一个可审计的沙箱，h5i browser requests 和 h5i browser audit 会把整场会话的动词、抓取、交接、结束全记下来。
要更强的隔离，就在 .h5i/env.toml 里选一个档位：workspace、process、supervised、container、microvm，限制网络出口和文件系统访问。
h5i box create alpha --profile agent-claude # 沙箱化的 git worktree
h5i box shell alpha # 受限的交互会话
h5i browser open https://docs.rs/ --in alpha # 在 box 里开浏览器
h5i box propose alpha # 出可复核快照
h5i box apply alpha # 合并已批准的改动
h5i box rm alpha # 丢弃
从宿主机用 h5i ui 看整场会话：
注意这个设计逻辑：Agent 干活在一个隔离盒子里，出结果要人复核（propose → apply），不合适就 rm。 这比「给 Agent 一个 shell 让它随便跑」高一个层级。
亮点三：用 Lean 4 形式化验证代码
红队能找到你没想到的 bug，但证明不了「没有 bug」。h5i 的另一条腿是形式化验证：把后端建在 h5i-app（Axum 的 Rust 框架）上，用 Aeneas 把 Rust 逻辑翻译成 Lean 4，然后在 Lean 里证明属性。
[dependencies]
h5i-app = { version = \"0.1\", features = [\"http\", \"postgres\"] }
它的做法是：把逻辑写成纯 Rust 函数，用 Aeneas 翻译到 Lean，在那里证「租户隔离」「授权」「不变量在每一次写库、每一次快照加载、每一种请求提交顺序下都成立」。翻译的是内核、SQL planner、JSON writer、token codec 这几块。
官方在 TRUST.md 里明确划了边界：证明了的是 transition 的属性、编译后的语句只碰租户自己的行、被接受的写所维持的不变量在每种数据库状态和快照下都成立；信任但没证的是 axum、PostgreSQL 的语句语义、HMAC 密钥、时钟，以及翻译工具本身。
这一点对读者很重要：形式化验证不是「代码绝对没 bug」的营销词。 它证明的是「你写下的那条性质」，边界之外的（框架、数据库语义、密钥、时钟）是信任，不是证明。分清这个，才不会被「形式化验证」四个字唬住。
上手
官方给了一条命令安装：
curl -fsSL https://h5i.dev/install.sh | sh -s -- --websec --recon --test # 三个可选插件
# cargo install --path . # 从源码构建
# h5i plugin list # 看装了哪些
它面向 Agent 的接口是一个 skill，二进制自带：
npx skills add h5i-dev/h5i # 还没有二进制时
h5i skill install # 写到你的运行时找的地方
h5i skill show policy # 或直接读一页
CI 里可以重放确认过的攻击流，官方模板：
- uses: h5i-dev/h5i@v1
with:
target: http://localhost:3000
tests: .h5i-tests/tests
避坑
第一，它不是 Burp 的替代品。官方自己写得很清楚：h5i 适合「Agent 需要浏览应用、并在一个界面里抓改重放对比 HTTP 流量」的场景；成熟的手工工作流、自动化扫描、扩展、底层协议测试，Burp 仍然更合适。
第二，它不适用所有网站。重内容站点和常见浏览器交互它做得最好；需要完整 Chromium 的站点，得走 h5i browser proxy，或者干脆把 Chromium 跑在沙箱里。
第三，它不能防住所有 prompt injection。官方在 FAQ 里说得很直接：没有浏览器能可靠检测或防住每一种 prompt injection。h5i 降低的是影响面——把页面内容当不可信、限制网络和文件访问、隔离凭证、记录 Agent 的动作供人复核。它不承诺「免疫」。
第四，沙箱默认只是轻量进程隔离。要强隔离，得主动把浏览器或整个工作流放进 supervised 沙箱、容器或 microVM。默认那层只是「顺手做了一点」，不是「已经关严了」。
第五，形式化验证只覆盖 h5i-app 那条路。它的 h5i-app 是给 Rust 项目用的 crate，不需要 h5i 二进制；两条腿是「各自独立、在一个 box 里相遇」的关系。你要用它证一个非 Rust 的应用逻辑，用不上。
第六，它没有托管服务，数据在本地。官方明确说没有 hosted service，session 存在本地；但浏览器流量仍会发到它允许的站点，模型流量仍会发到你配置的模型厂商。本地存储不等于「不出网」。
适合谁
- 用 AI Agent 做 Web 漏洞赏金/渗透测试的人：想要一个自带浏览器、抓改重放、还能记全会话的工具；
- 担心 Agent 跑飞的人：想要「隔离 + 可审计 + 出结果要人复核」这条链的；
- 写 Rust Web 后端的开发者：想知道「用 Lean 4 证应用逻辑」大概长什么样、边界在哪的；
- 研究 Agent 原生安全的人：想拆一个把「红队工具」和「形式化验证」放进同一个工作区的实现的。
不适合谁：想要「一键扫全网」的自动化扫描器的人——它的定位是 Agent 的 Web 安全工作台，不是扫描平台；以及想拿它替代 Burp 做成熟手工工作流的人。
最后
回到开头那个问题：要不要让 AI Agent 自己去开浏览器、抓流量、改请求。
h5i 给的是一个工程答案：Agent 的每一步都在有边界、可审计的会话里；要动手改数据，先出快照给人复核；要证正确性，把逻辑翻译成 Lean 4 证明，并明确写出哪些是证明、哪些只是信任。
这两年的 AI 安全，重心在悄悄挪位置。以前你担心的是模型会不会说错话，现在你更该担心的是模型周围那一圈工具、它手里的凭证，以及它发出的每一个请求。当每个 Agent 都能开浏览器、能改请求的时候，「把不可信的东西和凭证隔开、把每一个动作记下来」这件事，就得在工具里做，而不是靠自觉。
版权声明
本站仅做备份收录，仅供研究与教学参考之用。
读者将信息用于其他用途的，全部法律及连带责任由读者自行承担，本站不承担任何责任。
评论