可复用的以太坊合约属性 - 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

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

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News