智能合约审计是一个"多防线"的过程：自动化工具在 5 分钟内发现 80% 的"愚蠢错误"，工具辅助的审查覆盖边界条件，而深度的经济博弈分析则需要经验丰富的审计师。
12.4.1 审计的多层模型
graph TB
subgraph 自动层["自动层 0-5min"]
S[Static Analysis<br/>Slither / SolorVite]
F[Fuzzing<br/>Echidna / Foundry]
end
subgraph 半自动层["半自动层 1-3h"]
M[符号执行<br/>Mythril / Halmos]
D[Dependency 扫描<br/>Advisories]
end
subgraph 人工层["人工层 10-40h"]
M1[架构审查<br/>业务逻辑分析]
M2[经济攻击面分析<br/>MEV / 闪电贷场景]
M3[链下集成风险<br/>预言机 / 跨链桥]
end
S --> M
F --> D
M --> M1
D --> M2
M1 --> M3
style S fill:#c8e6c9
style F fill:#c8e6c9
style M1 fill:#bbdefb
style M2 fill:#bbdefb
style M3 fill:#bbdefb12.4.2 Slither：静态分析的事实标准
核心能力
Slither（Trail of Bits）使用 抽象语法树（AST）+ 控制流图（CFG） 分析所有可能的执行路径，检测已知 bug 模式：
| 检测类型 | 示例 | 误报率 |
|---|---|---|
| 重入检测 | 外部调用后未更新状态 | 中 |
| 未检查返回 | call() 返回值未检查（当用低层 call） | 低 |
| 重命名继承 | 变量名隐藏父类变量 | 低 |
| 中心化 | 关键函数 onlyOwner 但缺乏 2-步操作 | 低 |
| 自委托 | 智能合约可以自调用外部函数 | 极低 |
| 可重入性 | 循环中调用外部合约 | 低 |
typescript
/**
* 简化静态分析逻辑：模拟重入检测的核心模式
*/
interface ASTNode {
type: string;
children: ASTNode[];
externalCall?: boolean; // msg.sender.call() 等外部调用
stateWrite?: boolean; // balances[x] = ... 等状态写
functionName: string;
}
function detectReentrancy(functions: ASTNode[]): {
vulnerabilities: { functionName: string; confidence: "high" | "low" }[];
totalFunctions: number;
} {
const vulns: { functionName: string; confidence: "high" | "low" }[] = [];
for (const fn of functions) {
// 模式：存在 externalCall 且在其之后有 stateWrite
// 实际 Slither 使用数据依赖分析，这里是简化启发式
const externalCalls = collectNodes(fn, n => n.externalCall);
const stateWrites = collectNodes(fn, n => n.stateWrite);
if (externalCalls.length > 0) {
// 检查是否有 stateWrite 发生在 AFTER 外部调用之后
const callIndex = fn.children.findIndex(findMaxDepth(externalCalls));
const writeIndex = fn.children.findIndex(findMaxDepth(stateWrites));
if (callIndex >= 0 && writeIndex > callIndex) {
vulns.push({ functionName: fn.functionName, confidence: "high" });
} else if (callIndex >= 0 && writeIndex === -1) {
vulns.push({ functionName: fn.functionName, confidence: "low" });
}
}
}
return { vulnerabilities: vulns, totalFunctions: functions.length };
}
function collectNodes(root: ASTNode, predicate: (n: ASTNode) => boolean): ASTNode[] {
const result: ASTNode[] = [];
function walk(n: ASTNode) {
if (predicate(n)) result.push(n);
for (const c of n.children) walk(c);
}
walk(root);
return result;
}
function findMaxDepth(nodes: ASTNode[]) {
return (n: ASTNode) => nodes.some(target => target === n);
}
// 示例
const badWithdraw: ASTNode = {
type: "function",
functionName: "withdraw",
children: [
{ type: "call", externalCall: true, functionName: "msg.sender.call", children: [], stateWrite: false },
{ type: "write", externalCall: false, functionName: "balances[msg.sender]=0", stateWrite: true, children: [] },
],
externalCall: false,
stateWrite: false,
};
console.log("Bad pattern:", detectReentrancy([badWithdraw]).vulnerabilities);
// 输出: high confidence: 外部调用在状态写之前12.4.3 符号执行：Mythril / Halmos
符号执行不是运行程序时以具体数值，而是以符号变量（如 ）作为输入，跟踪程序在所有路径上的约束。
求解约束系统：SMT 求解器（Z3-based）可以精确发现溢出路径：
text
约束1: a = α, b = β, a >= 0, b >= 0
约束2: a + b < a (溢出条件)
=> β > MAX_UINT256 - α
SMT solver response: 可解！示例: α = 2^255, β = 2^255这可以精确找到边界条件，但状态空间爆炸限制了分析深度。
| 工具 | 架构 | 适用类型 | 局限 |
|---|---|---|---|
| Mythril | 基于 Python + Z3 | 重入、溢出、权限 | 路径爆炸，>1K 行难以分析 |
| Halmos | Haskell + Z3 | 函数性质验证 | 需要规范注解 |
| Certora | Java + SMT | 业务逻辑、协议不变式 | 高级，需要学习 Certora Script |
| Echidna | 基于属性的 Fuzzing | 快速覆盖 | 不保证穷尽 |
12.4.4 审计报告结构
如果一名审计师给你回到报告，至少应包括：
| 等级 | 严重度 | 响应时间 |
|---|---|---|
| C-0/Critical | 资金直接可虑取 | 发布前必须修复 |
| C-1/High | 资金在特殊条件下可虑取 | 24 小时评估 |
| C-2/Medium | 业务逻辑缺陷 | 30 天内修复 |
| C-3/Low | 代码质量/效率 | 有空再修 |
| Info/Gas | 不影响安全的优化 | 可选 |
> ← 上一节：12.3 漏洞 | 前往 → 12.5 可升级合约 |*
评论
0评论加载中…