GoProve

一款针对 Go 语言的静态分析工具，它使用抽象解释来数学证明代码的相关属性 —— 或者确切地告诉你它无法证明的地方。

当 GoProve 提示存在 Bug 时，这是有保证的。当它说你的代码安全时，这是经过证明的。当它不确定时，也会诚实地告诉你。 ## 目录 - [为什么选择 GoProve？](#why-goprove) - [安装](#install) - [用法](#usage) - [检测内容](#what-it-detects) - [工作原理](#how-it-works) - [三色模型](#three-color-model) - [与其他工具的对比](#comparison-with-other-tools) - [可靠性详情](#soundness-details) - [实际结果](#real-world-results) - [CI 集成](#ci-integration) - [路线图](#roadmap) - [贡献](#contributing) - [致谢](#credits) - [许可证](#license) ``` $ goprove ./... Error: billing/charge.go:47 nil dereference of nil pointer — value is always nil Warning: handler/click.go:89 possible nil dereference of config — add a nil check before use Summary: 1 bugs, 1 warnings. ``` ## 为什么选择 GoProve？ Go 语言的类型系统可以在编译期阻止多种类型的 Bug，但有三类问题总是会逃逸到生产环境中：**nil 指针解引用**、**除零错误**和**整数溢出**。这些属于运行时 panic —— 它们取决于值而不是类型，再多的类型安全性也无法阻止它们。 现有的 Go 工具通常通过模式匹配（如 `go vet`、`staticcheck`）或约束推断（如 `NilAway`）来处理这些问题。这些方法很有用但存在局限性 —— 它们可能会遗漏真正的 Bug 或误报正确的代码，且在这两方面都无法提供形式化的保证。 GoProve 采用了一种截然不同的方法。它使用了**抽象解释**（Cousot & Cousot, 1977）—— 这是一个用于计算程序行为可靠近似值的数学上严谨的框架。相同的理论基础也被应用于 Polyspace（汽车/航空航天）和 Astrée（空中客车飞行控制器）等工具中。GoProve 将这一技术应用于生产级别的 Go 代码。 ### 为什么在航空航天之外的领域也需要数学证明 形式化验证传统上一直专用于安全关键型系统 —— 飞行控制器、医疗设备、核反应堆。人们通常认为普通软件不需要数学证明。 但是，考虑一下“普通”的 Go 后端实际上在做什么：处理支付、计算归因、车辆路线规划、处理数以百万计的请求。这些系统中的 nil panic 不会致命 —— 但它会损失金钱、破坏数据、打破 SLA，并在凌晨 3 点呼叫工程师。这些 Bug 造成的代价是真实且可衡量的。 阻碍进行证明的原因并非是后端代码不需要它 —— 而是证明工具需要注解、规范或博士级别的专业知识才能操作。抽象解释消除了这一障碍。它可以直接处理未经修改的源代码，在几秒钟内运行完毕，并为您提供与空客飞行软件相同的数学保证：**如果工具说它是安全的，那它就是安全的。** 现在的问题不再是“我的代码是否足够安全关键到需要证明？”，而是“我为什么不想要一个数学保证，来确保我的 nil 检查是切实有效的？” ### 适用人群 构建 Go 后端的工程师，尤其适用于： - **银行/支付系统** —— 事务处理器中的 nil panic 意味着资金损失 - **广告技术/归因计算** —— 计费时隐秘的整数溢出意味着错误的收费 - **网约车/物流** —— 路线规划中的除零错误意味着凌晨 3 点的告警呼叫 - 任何厌倦了 linter 无法捕获的运行时 panic 的团队 ### 核心理念 - **零注解。** 不需要特殊的注释、契约或规范文件。该工具会从您的代码中推断出一切。 - **对 Bug 的判断是可靠的。** 当 GoProve 报告 Bug 时，抽象解释已经证明了它在所有执行路径上都存在。对于已证明的 Bug，不存在漏报。 - **对局限性保持诚实。** 三色模型（Bug/警告/安全）透明地展示了分析能证明和不能证明的内容。分析器故意牺牲了完备性 —— 为了绝不漏报已证明的 Bug，分析可能会对实际安全的代码发出警告。 - **增量价值。** 每个分析域本身都能提供可用的工具价值。您不需要完整的套件即可获益。 ### GoProve 不是什么 - 不是测试的替代品 —— 它证明关于所有输入的属性，但仅限于它跟踪的模式。 - 不是认证工具 —— 它是为生产工程师设计的，而不是用于安全认证（IEC 62304, DO-178C）。 - 不是基于注解的验证器 —— 那是 [Gobra](https://github.com/viperproject/gobra) 的领域。 - 不是定理证明器 —— 那是 [coq-of-go](https://github.com/formal-land/coq-of-go) 的领域。 - 不是运行时分析器 —— 那是竞态检测器的领域。 ## 安装 GoProve 根据您的需求提供两种模式： ### CLI（全程序分析 —— 推荐用于 CI） ``` go install github.com/ahmedaabouzied/goprove/cmd/goprove@latest ``` CLI 会一次性分析您的整个程序。它使用带不动点迭代的全程序参数跟踪 —— 如果函数的所有调用者在 nil 守卫之后都传递了 non-nil，则该参数被**证明**为 non-nil。这是最准确的模式，具有最少的误报。 ### go/analysis 插件（用于 golangci-lint 和 go vet） ``` go install github.com/ahmedaabouzied/goprove/cmd/goprove-lint@latest ``` `go/analysis` 集成可与 golangci-lint、`go vet` 以及任何支持该框架的工具配合使用。它一次分析一个包，因此无法提供全程序参数跟踪功能 —— 您可能会看到 CLI 本会证明为安全的参数产生了额外的警告。 ### 该用哪个？ | | CLI / [GitHub Action](https://github.com/ahmedaabouzied/goprove-action) | go/analysis 插件 | |---|---|---| | 全程序参数跟踪 | 是 | 否（仅限单包） | | 跨包 nil 安全 | 是 | 否 | | golangci-lint / go vet | 否 | 是 | | IDE 集成 | 否 | 是 | | 最适合 | CI 流水线，完整证明 | 本地开发，快速反馈 | **我们的建议：** 两者都用。在本地运行 `goprove-lint` 以在开发期间获取快速反馈。在 CI 中运行 [GitHub Action](https://github.com/ahmedaabouzied/goprove-action) 以获取完整的全程序证明。 ## 用法 ### CLI ``` # 分析单个 package goprove ./pkg/server # 分析所有 package（推荐） goprove ./... # 在 CI 中使用 — 如果有任何 findings 则以退出码 1 退出 goprove ./... || exit 1 ``` ### go vet ``` go vet -vettool=$(which goprove-lint) ./... ``` ### golangci-lint 添加到您的 `.golangci.yml` 中： ``` linters: enable: - goprove ``` （与 golangci-lint 的插件注册即将推出。） ## 检测内容 ### Nil 指针解引用 GoProve 会在您的整个程序中跟踪 nil 状态： ``` func process(config *Config) { if config == nil { return } helper(config) // GoProve knows config is non-nil here } func helper(config *Config) { config.Validate() // No warning — all callers pass non-nil } ``` - 已证明的 nil 解引用（`var p *int; *p`）被标记为 **Bug** - 未经检查的参数被标记为 **警告** —— 除非所有调用者都传递 non-nil - Nil 检查（`if p != nil`）、提前返回（`if p == nil { return }`）、`new()`、`make()`、`&x` 都会被跟踪 - 在 nil 检查后的字段重载（`if o.Field != nil { o.Field.Use() }`）会被证明为安全 - 检测到对 nil 接口的接口方法调用（`s.Method()`） - 全局变量的 nil 检查会传播到后续的读取操作中 ### 除零错误 ``` func safe(x, y int) int { if y != 0 { return x / y // GoProve: safe } return 0 } func unsafe(x int) int { zero := 0 return x / zero // GoProve: Bug — division by zero } ``` ### 整数溢出 ``` func narrow(x int16) int8 { if x < 100 && x > -100 { return int8(x) // GoProve: safe — x fits in int8 } return 0 } ``` - int8, int16, int32 上的算术溢出 - 收缩转换溢出（int16 → int8） - 取负溢出（`-math.MinInt8`） ## 工作原理 GoProve 基于 Go 的 SSA（Static Single Assignment）中间表示构建，并使用两个域运行抽象解释： 1. **区间域**：每个整数变量的 `[lo, hi]` —— 证明除法和溢出安全性 2. **Nil 状态域**：每个指针的 `{DefinitelyNil, DefinitelyNotNil, MaybeNil}` —— 证明 nil 安全性 关键技术： - **基于地址的内存模型** —— 跟踪每个内存地址的 nil 状态，而不是每个 SSA 寄存器。来自同一字段的两次加载共享 nil 状态。 - **全程序参数分析** —— 不动点迭代计算每个参数实际接收到的调用者传递的内容。如果在 nil 守卫之后所有调用者都传递 non-nil，则该参数被证明为 non-nil。 - **过程间返回摘要** —— 被调用者的返回 nil/区间状态通过 CHA 调用图解析进行跟踪。 - **分支细化** —— `if p != nil`、`if y != 0`、`<`、`<=`、`>`、`>=` 会缩小每个分支的抽象状态。 - **带拓宽的工作列表** —— 确保循环中的终止性，同时保持可靠性。 ## 三色模型 GoProve 使用诚实的三色分类： | 颜色 | 含义 | 保证 | |-------|---------|-----------| | **Bug**（红色） | 证明会在运行时崩溃 | 数学保证 —— 没有漏报 | | **警告**（黄色） | 无法证明安全或不安全 | 值得调查 —— 可能是真的 Bug，也可能是分析局限 | | **安全**（无输出） | 证明对于跟踪模式是安全的 | 数学保证 —— 针对我们跟踪的模式 | ## 与其他工具的对比 | | **GoProve** | **NilAway (Uber)** | **staticcheck** | **go vet** | |---|---|---|---|---| | 技术 | 抽象解释 | 基于约束的 2-SAT | 模式匹配 | 模式匹配 | | Nil 检测 | 基于格并带有证明 | 约束推断 | 有限的模式 | 非常有限 | | 除零检测 | 是（区间域） | 否 | 否 | 否 | | 整数溢出检测 | 是（区间域） | 否 | 否 | 否 | | 可靠性 | **对 Bug 可靠** | 既非可靠也非完备 | 不可靠 | 不可靠 | | 过程间分析 | 返回摘要 + 全程序参数 | go/analysis Facts | 否 | 否 | | 参数跟踪 | **全程序数据流** | 约束传播 | 否 | 否 | | 地址模型 | **基于内存地址** | 断言树 | 否 | 否 | | golangci-lint | 暂不支持 | 是 | 是 | 是 | | 测试规模 | 约 5 万行代码 | 9000 万行代码 | 生产级别 | 生产级别 | **GoProve 的优势**：当它报告 Bug 时，这是经过证明的。当它说安全时，这是有数学保证的。没有任何其他开源 Go 工具能做到这一点。 **NilAway 的优势**：速度更快，可扩展到庞大的代码库，与 golangci-lint 集成。但它可能会同时产生误报和漏报。 ## 可靠性详情 **“证明”的含义：** - Bug 发现是可靠的：抽象解释已经证明了该 Bug 在所有执行路径上都存在。 - 安全发现在跟踪模式内是可靠的：如果 GoProve 没有产生任何发现，则该操作在它分析的模式范围内是安全的。 **该工具不涵盖的范围：** - 并发：不跟踪跨 goroutine 或 channel 的值。 - 反射：`reflect.Call` 参数对静态分析是不可见的。 - 某些 `unsafe.Pointer` 转换链。 - CGo：C 函数调用位于 Go 的类型系统之外。 **务实的有意选择：** - 方法接收器被假定为 non-nil（减少了噪音，但会遗漏 `(*T)(nil).Method()`）。 - 切片索引仅标记已证明为 nil 的切片，而不是可能的 nil（推迟到未来的边界检查器处理）。 **正确处理的模式：** - `v, ok := m[key]; if ok && v != nil { *v }` —— map ok 模式 - `v, ok := x.(T); if ok { v.Do() }` —— 类型断言 ok 模式 - `time.NewTimer()`、`bytes.NewBuffer()` —— 标准库返回值（通过过程间分析） - `if x.F != nil { x.F.Use() }` —— nil 检查后的字段重载（通过地址模型） ## 实际结果 | 代码库 | 发现 | |----------|----------| | 生产日志包 | 0 个警告（在引入全程序参数跟踪之前为 32 个） | | go-redis v9.7.3 | 62 个 nil + 3 个溢出警告，全部合理。在受守卫保护的模式上 0 误报。 | | net/http（标准库） | 0 个已证明的 Bug。仅对导出的函数参数发出警告。 | | 生产平台包 | 0 个警告 | | gboost（ML 库） | 个 Bug，16 个警告 | ## CI 集成 ### GitHub Action（推荐 —— 全程序分析） 使用 [GoProve Action](https://github.com/ahmedaabouzied/goprove-action) 进行完整的全程序证明： ``` - uses: ahmedaabouzied/goprove-action@v1 with: path: ./... ``` ### 手动 CI 步骤 ``` - name: Run GoProve run: | go install github.com/ahmedaabouzied/goprove/cmd/goprove@latest goprove ./... ``` 当检测到发现时，GoProve 将以代码 1 退出。 ## 路线图 | 阶段 | 重点 | 状态 | |-------|-------|--------| | 1 | 整数区间分析（除零，溢出） | 已完成 | | 2 | Nil 指针分析（地址模型，过程间，全程序参数） | 已完成 | | 3 | 切片边界分析 | 已规划 | | 4 | 全程序整数范围跟踪 | 已规划 | | 5 | GC 压力分析 | 已规划 | | 6 | 并发分析 | 已规划 | | 7 | SARIF 输出，golangci-lint 插件，GitHub Action | 已规划 | ## 致谢 Gopher 吉祥物由 [Mat Ryer](https://github.com/matryer) 和 [Ashley McNamara](https://github.com/ashleymcnamara) 使用 [gopherize.me](https://gopherize.me) 创建，基于 [Renee French](https://reneefrench.blogspot.com/) 的原创 Go gopher 设计。 ## 许可证 [MIT](LICENSE)

标签：Bug检测, EVTX分析, Go语言, SAST, 代码安全, 代码审查, 可靠性, 威胁情报, 开发者工具, 形式化验证, 抽象解释, 数学证明, 日志审计, 漏洞枚举, 盲注攻击, 程序破解, 空指针解引用, 编译器原理, 错误基检测, 静态代码分析, 静态测试