3. 程序验证: Hoare 逻辑 / 符号执行 / 形式语义

TL;DR

TLA+ 验证"算法设计"，Coq 证明"数学命题"；**程序验证（Program Verification）**把两者连起来——验证真实代码满足规格。核心工具是 Hoare 逻辑（{P} 程序 {Q}：前置条件 P 下运行程序，结束时满足 Q）、符号执行（用符号变量替代输入，穷举路径）、形式语义（程序行为的严格定义）。这一章讲心智模型 + 最小示例，让你理解"为什么编译器/内核/加密代码能被证明"，以及符号执行工具（KLEE / CBMC）怎么自动找 bug。

读完应能：

1. 写出并理解 Hoare 三元组 {P} C {Q}，会推导最弱前置条件。
2. 理解形式语义的三种（操作/指称/公理），知道分别干什么。
3. 理解符号执行怎么自动找 bug（KLEE / CBMC 原理）。
4. 说出程序验证在工程（智能合约、加密、内核）里的实际用法。
5. 理解"验证代码"和"验证设计"的关系（本章 vs 上一章）。

一、Hoare 逻辑

1.1 Hoare 三元组

$$ {P}\ C\ {Q} $$

• $P$：前置条件（运行 C 前必须为真）
• $C$：程序（语句）
• $Q$：后置条件（C 运行结束后必须为真）

读作："如果 P 在执行前成立，并且 C 正常终止，那么执行后 Q 成立"。

1.2 例子

{x = 2}  x := x + 1  {x = 3}
{true}   x := 0      {x = 0}
{i < n}  i := i + 1  {i <= n}      ← 循环边界

1.3 核心推导规则

赋值公理（最强后置条件规则）：

$${P[x \mapsto E]}\ x := E\ {P}$$

把 P 里所有 x 替换成 E。例：

{x + 1 > 0}  x := x + 1  {x > 0}

序列规则：

{P} C1 {R}  ∧  {R} C2 {Q}  ⇒  {P} C1; C2 {Q}

条件规则：

{P ∧ B} C1 {Q}  ∧  {P ∧ ¬B} C2 {Q}  ⇒  {P} if B then C1 else C2 {Q}

循环不变量（while 的关键）：

{P ∧ B} C {P}  ⇒  {P} while B do C {P ∧ ¬B}

$P$ 是循环不变量：每轮循环开始/结束都为真，退出时加 ¬B。

二、形式语义

2.1 三种语义

2.2 操作语义示例（小步）

(x := E, σ) → (skip, σ[x ↦ Eval(σ, E)])     \* 状态更新
(skip; C2, σ) → (C2, σ)                      \* 顺序执行

程序 (C, σ) 二元组，→ 是一步步转换，直到 skip 结束。

2.3 为什么需要形式语义

• 语义是编译器/验证器/模型的共同地基：没有严格语义，"编译器正确"无法定义。
• 上一章 CompCert "保持语义"指的就是操作语义在变换前后不改变（观察行为一致）。

三、最弱前置条件（Weakest Precondition）

3.1 定义

给定语句 C 和后置条件 Q，最弱前置条件 wp(C, Q) 是所有使 C 执行后满足 Q 的最宽松条件。

{P} C {Q}  ⟺  P ⇒ wp(C, Q)

3.2 推导示例

# 目标: {?} y := x + 1; x := y * 2 {x > 10}
# 从后往前:
wp(x := y*2, x > 10)   = y*2 > 10  = y > 5
wp(y := x+1, y > 5)    = x+1 > 5   = x > 4
# 结论: {x > 4} y := x + 1; x := y * 2 {x > 10}

这就是程序验证器的核心算法——从后置条件反向推导前置条件，验证"实际前置 P 蕴含 wp"。

四、符号执行（Symbolic Execution）

4.1 与测试的区别

测试:   输入 = 具体值 → 跑 → 检查输出
符号执行: 输入 = 符号变量 x → 跑 → 记录路径条件 → 检查所有路径

• 用符号代替输入值，执行时路径条件是布尔表达式（x > 0、x < 100...）。
• 用 SMT 求解器（Z3）判断路径条件是否可满足 → 自动生成测试用例 / 找不可达路径 / 找 bug。

4.2 例子

int foo(int x) {
    int y = x + 1;
    if (y > 10) return 1;      // 路径1: x+1 > 10 → x > 9
    else return 0;             // 路径2: x+1 <= 10 → x <= 9
    // 符号执行枚举这两条路径, Z3 判断可满足性
}

4.3 工具

4.4 工程价值

• 自动生成测试：符号执行产出"覆盖所有可达路径"的输入。
• 找漏洞：数组越界、除零、断言失败自动发现。
• 智能合约安全：用符号执行 + 模型检查找重入、整数溢出（如 Mythril / Slither）。

五、静态分析：程序验证的"轻量版"

5.1 三档强度

• 静态分析可能误报（over-approximate），形式验证不误报（但要规格）。
• 工程上：Lint + SAST 进 CI（便宜），形式验证用于关键组件。

5.2 CodeQL 例子（找 SQL 注入）

import python
from FlaskRequest r, MySQLExec call
where call.getArg(0).getValue().getExpr().(Name)
      .refersTo(r.getArg("query"))
select call, "SQL injection from request param"

六、程序验证 vs 前面章节

TLA+ (设计)        验证算法/协议的性质        [上一章]
定理证明 (Coq)     验证数学命题 / 抽象程序    [上一章]
程序验证 (本章)     验证真实代码满足规格        ← 本章

三者的分工：

七、工程落地建议

什么时候用什么:
  并发协议设计        → TLA+ (设计期, 便宜)
  加密/解析器/内核关键  → 定理证明 + 程序验证 (代价高, 但正确性关键)
  智能合约            → 符号执行 + 静态分析 (Mythril / Slither)
  普通代码            → Lint + SAST + 测试 (工程默认)

八、结束 + 速查表

回主目录: 形式化方法卷 README.