73 lines
2.2 KiB
Markdown
73 lines
2.2 KiB
Markdown
---
|
||
title: "Certora（形式化验证工具）"
|
||
type: concept
|
||
tags: [blockchain, security, smart-contract, formal-verification, tooling]
|
||
sources: [blockchain-security-auditor]
|
||
last_updated: 2026-05-30
|
||
---
|
||
|
||
## Aliases
|
||
- Certora
|
||
- Certora Prover
|
||
- Certora Verification System
|
||
|
||
## Definition
|
||
|
||
Certora 是一个基于符号执行（Symbolic Execution）的智能合约形式化验证工具，通过 CVL（Certora Verification Language）描述协议规范，系统性证明 Solidity 合约的关键属性是否在所有可能状态下成立。与测试不同，Certora 可以证明某个属性**在数学上不可能被违反**。
|
||
|
||
## Key Capabilities
|
||
|
||
- **属性证明**：验证合约不变性（invariant）在所有执行路径上成立
|
||
- **反例生成**：当属性无法被证明时，自动生成导致属性失败的最小执行序列
|
||
- **多合约分析**：支持分析调用关系复杂的合约系统
|
||
- **并行验证**：可并行验证多条规则
|
||
|
||
## CVL Example
|
||
|
||
```
|
||
rule noUnauthorizedWithdrawal(method f) {
|
||
env e;
|
||
calldataarg args;
|
||
|
||
require f != nop; // 排除空调用
|
||
|
||
// 如果调用成功，则调用者必须是所有者
|
||
f(e, args);
|
||
assert e.msg.sender == owner, "Unauthorized withdrawal";
|
||
}
|
||
|
||
invariant totalSupplyInvariant() {
|
||
// 总供应量恒定
|
||
invariant totalSupply == init(totalSupply);
|
||
}
|
||
```
|
||
|
||
## Integration with Foundry
|
||
|
||
Certora 可与 Foundry 集成：
|
||
```bash
|
||
# 使用 Halmos 进行字节码级验证
|
||
forge test --match-contract CertoraTest
|
||
|
||
# 使用 Certora CLI
|
||
certora Run Vault.spec Vault.sol --prover z3 cvc5
|
||
```
|
||
|
||
## Limitations
|
||
|
||
- 需要人工编写精确的 CVL 规范（规范本身可能出错）
|
||
- 复杂合约状态空间可能导致超时
|
||
- 对外部依赖和链上状态处理有限
|
||
- 学习曲线陡峭
|
||
|
||
## Relationship to Audit
|
||
|
||
- Certora 是 [[Blockchain-Security-Auditor]] 进行 [[Formal-Verification]] 的主要工具
|
||
- 适合验证关键协议属性：份额不变性、借贷健康度、权限不变性
|
||
- 与 [[Slither]] 互补：Slither 找代码模式漏洞，Certora 证明数学属性
|
||
|
||
## Connections
|
||
- [[Blockchain-Security-Auditor]] ← uses ← [[Certora]]
|
||
- [[Formal-Verification]] ← implements ← [[Certora]]
|
||
- [[Halmos]] ← complementary bytecode verification ← [[Certora]]
|