以太坊合约可复用属性

随着智能合约安全技术的持续演进，基于属性的模糊测试已成为开发者和安全工程师的首选技术。该技术依赖于代码属性（通常称为不变量）的创建，这些属性描述了代码应实现的功能。为帮助社区定义属性，我们发布了一套包含168个预构建属性的集合，可用于指导我们的智能合约模糊测试工具Echidna，或直接通过单元测试使用。覆盖的属性包括符合最常见ERC代币接口的合规性、通用可测试的安全属性，以及测试定点数学运算的属性。

由于掌握这些工具需要时间和实践，我们将在Twitch和YouTube频道举办两场直播，提供这些不变量的实战经验：

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

为什么应该使用这个？

代码库和相关研讨会将展示模糊测试如何提供比单元测试更高级别的安全保证。这套属性集合易于与使用知名标准或常用库的项目集成。本次发布包含对ABDKMath64x64库、ERC-20代币标准和ERC-4626代币化金库标准的测试：

ERC20

• 标准接口函数的属性
• 推断的合理性属性（例如：用户余额不应大于代币供应量）
• 可销毁、可铸造和可暂停代币等扩展功能的属性

ERC4626

• 验证舍入方向符合规范的属性
• 必须永不回退函数的回退属性
• 差分测试属性（例如：deposit()必须匹配previewDeposit()预测的功能）
• 功能属性（例如：redeem()从正确账户扣除份额）
• 非规范安全属性（份额通胀攻击、代币批准检查等）

ABDKMath64x64

• 相关函数的交换律、结合律、分配律和恒等属性
• 差分测试属性（例如：2^(-x) == 1/2^(x)）
• 对特定输入范围应回退函数的回退属性
• 对特定输入范围不应回退函数的负回退属性
• 区间属性（例如：min(x,y) <= avg(x,y) <= max(x,y)）

这些属性的目标是检测漏洞或与预期结果的偏差，确保符合标准，并为编写不变量的开发者提供指导。通过参加本研讨会，开发者将能够识别传统单元和参数化测试无法检测的复杂安全问题。此外，使用此代码库将使开发者能够专注于更深层次的系统性问题，而不是在低挂果实上浪费时间。

作为额外收获，在创建和测试这些属性时，我们在ABDKMath64x64库中发现了一个错误：对于divuu函数的特定输入范围，库中可能触发断言。关于该错误的更多信息，可从库的一位作者处找到此处。

自己动手！

如果不想等待直播，可以立即开始。以下是如何将属性添加到自己的代码库：

1. 安装Echidna。
2. 将属性导入项目：
   • 如果使用Hardhat，执行：npm install https://github.com/crytic/properties.git 或 yarn add https://github.com/crytic/properties.git
   • 如果使用Foundry，执行：forge install crytic/properties
3. 根据文档创建测试合约。

假设要创建一个名为YetAnotherCashEquivalentToken的新ERC20合约，并检查其是否符合标准。按照前述步骤，创建以下测试合约以执行外部测试：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

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

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

contract CryticTokenMock is YetAnotherCashEquivalentToken, PropertiesConstants {
    bool public isMintableOrBurnable;
    uint256 public initialSupply;
    constructor () {
        _mint(USER1, INITIAL_BALANCE);
        _mint(USER2, INITIAL_BALANCE);
        _mint(USER3, INITIAL_BALANCE);
        _mint(msg.sender, INITIAL_BALANCE);

        initialSupply = totalSupply();
        isMintableOrBurnable = false;
    }
}

然后，需要配置文件来设置Echidna中运行的模糊测试参数：

1
2
3
4
5
6

corpusDir: "tests/crytic/erc20/echidna-corpus-internal"
testMode: assertion
testLimit: 100000
deployer: "0x10000"
sender: ["0x10000", "0x20000", "0x30000"]
multi-abi: true

最后，在测试合约上运行Echidna：

1

echidna-test . --contract CryticERC20ExternalHarness --config tests/echidna-external.yaml

此外，这项工作是流动的。未来工作的一些想法包括：

如果您喜欢这篇文章，请分享：

• Twitter
• LinkedIn
• GitHub
• Mastodon
• Hacker News

页面内容：为什么应该使用这个？自己动手！最近帖子：使用Deptective调查依赖项、AIxCC评分轮次进行中、超越私钥风险的智能合约成熟度、Go解析器中意外的安全陷阱、评审首批DKLs23库的收获、Silence Laboratories的23个库。© 2025 Trail of Bits。使用Hugo和Mainroad主题生成。