h5i-dev/h5i

h5i – 智能代理原生 Web 安全工作区

简介

• 一个命令行工作区，让您可以使用 AI 智能代理寻找 Web 应用漏洞，并对 Rust Web 服务进行形式验证。
• 两种主要模式：
  1. 红队（漏洞发现） – 代理驱动无头浏览器，捕获/修改 HTTP 流量，爬取网站，并可在 CI/CD 中重放。
  2. 形式验证 – 使用 h5i-app Rust 框架（基于 Axum）编写应用，通过 Aeneas 将代码转换为 Lean 4，并证明授权或数据隔离等属性。

关键组件

组件	作用
h5i CLI	为代理（浏览器、websec、recon、app 命令）提供统一接口。
浏览器工具包	自动化导航、点击、表单填写等。
HTTP 工具包	捕获、修改、重放请求；对回归测试很有用。
侦察爬虫	通过爬取和 JS 分析发现隐藏的端点和参数。
h5i-app crate	基于 Axum 的 Rust 框架，设计为可转换为 Lean 4。
仪表板（h5i ui）	显示代理会话、流量和沙箱状态的本地 Web UI。

典型工作流程

1. 安装 – 一键脚本添加二进制文件和可选插件（websec、recon、test）。
2. 红队 – 例如：

   h5i browser open https://example.com
   h5i browser click @e3
   h5i websec requests            # 查看捕获的流量
   h5i websec replay req_42 --set query.id=456
   h5i recon crawl --max-requests 200
   

   代理可以在具有可配置文件系统/网络限制的沙箱中运行，记录的操作流可以存储在 CI 管道中并重放。
3. 构建可验证的应用 – 例如：

   h5i app new counter && cd counter   # 搭建新项目
   h5i app extract                     # 将 Rust 代码转换为 Lean 4
   h5i app prove                       # 运行 Lean 证明检查器
   h5i app mutate                      # 变异代码以查看证明破坏情况
   

   Rust crate 作为依赖项添加（h5i-app = "0.1.1"），并支持 HTTP 和 Postgres 等功能。
4. 监控 – 使用 h5i ui 启动本地 UI，查看浏览器会话和重放日志。

重要性

• 将AI 驱动的安全测试（快速、代理控制的探索）与形式方法（数学保证）相结合，这在 Web 安全工具领域非常罕见。
• 保持代理端轻量化（CLI 命令），同时为可证明安全的服务提供 Rust 优先的开发路径。

开始使用

• 通过提供的脚本或 cargo install --path . 安装。
• 将二进制文件作为 技能 添加（npx skills add h5i-dev/h5i）用于代理运行时。
• 在 MANUAL.md 或通过 man h5i 阅读完整命令参考。

许可证 – Apache-2.0。

---

所有细节均直接取自仓库的 README。