Trail of Bits 发布了一组预构建的属性，用于指导智能合约模糊测试工具 Echidna，或直接通过单元测试使用。这些属性涵盖了与常见 ERC token 接口的兼容性、通用可测试的安全属性以及用于测试定点数学运算的属性。此外，文章还介绍了如何使用这些属性，以及未来的工作方向。
随着智能合约安全性的不断发展，基于属性的模糊测试已成为开发者和安全工程师的首选技术。这种技术依赖于创建代码属性——通常称为不变量——来描述代码应该做什么。为了帮助社区定义属性，我们发布了一组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 函数的特定输入范围，可能会在库中触发断言。有关该错误的更多信息，请参见此处，该信息来自该库的作者之一。
自己动手！
如果你不想等待直播，你可以立即开始。以下是如何将属性添加到你自己的存储库：
假设你要创建一个名为 YetAnotherCashEquivalentToken 的新 ERC20 合约，并检查它是否符合标准。按照之前的步骤，你创建以下测试合约来执行外部测试：
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() {
// Deploy 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 中运行：
corpusDir: "tests/crytic/erc20/echidna-corpus-internal"
testMode: assertion
testLimit: 100000
deployer: "0x10000"
sender: ["0x10000", "0x20000", "0x30000"]
multi-abi: true
最后，在测试合约上运行 Echidna：
echidna-test . --contract CryticERC20ExternalHarness --config tests/echidna-external.yaml
此外，这项工作是流动的。未来工作的一些想法包括：
我们现在是主播了 2022 年 11 月 14 日\
多年来，我们构建了许多高影响力的工具，用于安全审查。你可能知道其中一些，例如 …你能通过 Rekt 测试吗？ 2023 年 8 月 14 日\
区块链开发人员面临的最大挑战之一是客观评估其安全态势并衡量 …持续集成的道 2021 年 2 月 26 日\
现代软件开发中的一个不言而喻的真理是，强大的持续集成 (CI) 系统是必要的。但是很多 …
