可复用的以太坊合约属性 - Trail of Bits博客

随着智能合约安全技术的持续演进，基于属性的模糊测试已成为开发者和安全工程师的首选技术。该技术依赖于代码属性（通常称为不变量）的创建，这些属性描述了代码预期实现的功能。为帮助社区定义属性，我们发布了一套包含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

此外，这项工作仍在持续进行。未来工作的一些想法包括：