可复用的以太坊合约属性测试

随着智能合约安全技术的演进，基于属性的模糊测试已成为开发者和安全工程师的核心技术。该技术依赖代码属性（通常称为不变量）的创建，这些属性描述了代码的预期行为。为帮助社区定义属性，我们发布了168个预构建属性集，可用于指导我们的智能合约模糊测试工具Echidna，或直接通过单元测试使用。覆盖范围包括：

• 常见ERC代币接口合规性
• 通用可测试安全属性
• 定点数学运算测试属性

实战直播安排

为帮助掌握这些工具，我们将举办两场直播：

• 3月7日：ERC20属性、示例用法和Echidna作弊码（Guillermo Larregay主讲）
• 3月14日：ERC4626属性、示例用法及高效模糊测试技巧（Benjamin Samuels主讲）

为什么需要使用？

该资源库及配套研讨会将展示模糊测试如何提供比单元测试更高级别的安全保障。这些属性集可轻松集成到使用知名标准或常用库的项目中，当前包含：

• ABDKMath64x64库测试
• ERC-20代币标准
• ERC-4626代币化金库标准

核心测试内容

ERC20

• 标准接口函数属性
• 基础合理性属性（如：用户余额不应超过代币供应量）
• 可销毁、可铸造、可暂停等扩展功能属性

ERC4626

• 符合规范的舍入方向验证
• 禁止回退函数的属性
• 差分测试属性（如deposit()必须与previewDeposit()预测功能匹配）
• 非规范安全属性（份额通胀攻击、代币授权检查等）

ABDKMath64x64

• 交换律、结合律、分配律和恒等属性
• 差分测试属性（如2^(-x) == 1/2^(x)）
• 输入范围回退验证
• 区间属性（如min(x,y) <= avg(x,y) <= max(x,y)）

快速开始指南

1. 安装Echidna
2. 导入属性库：
   • Hardhat项目：npm install https://github.com/crytic/properties.git
   • Foundry项目：forge install crytic/properties
3. 按文档创建测试合约

ERC20测试合约示例

1
2
3
4
5
6
7
8
9

pragma solidity ^0.8.0;
import "./YetAnotherCashEquivalentToken.sol";
import {ICryticTokenMock} from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol";

contract CryticERC20ExternalHarness is CryticERC20ExternalBasicProperties {   
    constructor() {
        token = ICryticTokenMock(address(new CryticTokenMock()));
    }
}

Echidna配置文件

1
2
3
4

corpusDir: "tests/erc20/echidna-corpus"
testMode: assertion
testLimit: 100000
sender: ["0x10000", "0x20000", "0x30000"]

运行命令：echidna-test . --contract CryticERC20ExternalHarness --config echidna.yaml

未来计划

• 扩展数学库测试（如PRBMath）
• 增加更多ERC标准测试
• 构建AMM/流动性池等通用合约测试集

本文档所有技术内容均基于Trail of Bits官方发布材料，无AI虚构内容。