54 lines
2.1 KiB
Markdown
54 lines
2.1 KiB
Markdown
---
|
||
title: "Formal Verification（形式化验证）"
|
||
type: concept
|
||
tags: [blockchain, security, smart-contract, formal-verification]
|
||
sources: [blockchain-security-auditor]
|
||
last_updated: 2026-05-30
|
||
---
|
||
|
||
## Aliases
|
||
- Formal Verification
|
||
- 形式化验证
|
||
|
||
## Definition
|
||
|
||
形式化验证（Formal Verification）是通过数学方法严格证明智能合约关键属性正确性的技术手段。与测试只能穷举有限场景不同，形式化验证可以证明某个属性在**所有可能的输入和状态**下均成立。
|
||
|
||
## Core Methods
|
||
|
||
### Invariant Specification（不变式规范）
|
||
定义协议的关键属性，用数学语言表达"协议必须始终保持的真理"：
|
||
- 总份额 × 每股净值 = 总资产（份额不变性）
|
||
- 借贷后抵押率必须 ≥ 清算阈值（健康度不变性）
|
||
- 管理员无法直接提取用户资金（权限不变性）
|
||
|
||
### Symbolic Execution（符号执行）
|
||
将合约函数参数替换为符号变量而非具体值，遍历所有可能的执行路径：
|
||
- 发现边界条件和组合触发场景
|
||
- Certora Prover、KEVM、Mythril 使用此方法
|
||
|
||
### Equivalence Checking（等价性检验）
|
||
验证合约实现与形式化规范是否等价：
|
||
- 高风险升级前后必须进行
|
||
- 防止修复一个漏洞引入另一个
|
||
|
||
## Key Tools
|
||
|
||
| Tool | Method | Focus |
|
||
|------|--------|-------|
|
||
| [[Certora]] | 符号执行 | Solidity 合约属性证明 |
|
||
| [[Halmos]] | 字节码符号执行 | 字节码级别验证（不依赖源码） |
|
||
| KEVM | 形式化 EVM | EVM 操作语义形式化模型 |
|
||
| Medusa | 符号执行 | 并行化模糊测试 |
|
||
|
||
## Relationship to Audit
|
||
|
||
- 形式化验证是 **Slither/Mythril/Echidna 等工具的补充**，不是替代
|
||
- 高风险协议（> $10M TVL）在审计报告中通常包含形式化验证章节
|
||
- 形式化验证的局限性：无法验证的需求规范错误、依赖外部状态
|
||
|
||
## Connections
|
||
- [[Blockchain-Security-Auditor]] ← uses methodology ← [[Formal Verification]]
|
||
- [[Slither]] ← lower-level analysis ← [[Formal Verification]]
|
||
- [[Echidna]] ← property-based testing ← [[Formal Verification]]
|