WTF-Solidity 中的 Halmos Cheat Codes用符号执行Symbolic Execution编写 Solidity 形式化验证测试【免费下载链接】WTF-SolidityWTF Solidity 极简入门教程供小白们使用。Now supports English! 官网: https://wtf.academy项目地址: https://gitcode.com/GitHub_Trending/wt/WTF-SolidityHalmos Cheat Codes 是依附于 a16z Halmos 子模块以lib/openzeppelin-contracts/lib/halmos-cheatcodes形式存在并由 OpenZeppelin 的正式验证Formal Verification测试真实引用。读完本文你将掌握 cheatcode 的完整接口、安装方式以及如何用它为 ERC-20 这类合约写出能自动给出反例counterexample的符号测试。背景为什么需要符号测试传统单元测试unit test针对的是具体输入下的具体行为模糊测试fuzzing虽然扩大了输入空间但仍然是抽样验证。符号执行symbolic execution则不同它允许把输入表示为符号symbolic value而非具体数值让程序沿着所有可行路径执行并借助求解器判定是否存在满足条件的输入。Halmos 就是一套基于 Foundry 的 Solidity 符号执行工具。而本仓库 README 所介绍的 Halmos Cheat Codes定位非常清晰Halmos cheatcodes 是为便于编写符号测试symbolic tests而设计的抽象函数例如在运行时创建新的符号值。这些 cheatcode 目前由 Halmos 独占支持但并不局限于此未来也可能被其他符号测试工具采纳。也就是说你可以在测试合约里以调用普通接口的方式请求一个符号值而真正的符号化处理由 Halmos 在运行时完成。本文所依据的文档位于 lib/openzeppelin-contracts/lib/halmos-cheatcodes/README.md其实现只有两个核心文件src/SymTest.sol供测试合约继承的抽象基类src/SVM.sol声明全部 cheatcode 接口的 SVMSymbolic Virtual Machine符号虚拟机接口。源码剖析一SymTest 与 SVM 的固定地址机制先看 SymTest.sol 的完整实现// SPDX-License-Identifier: AGPL-3.0 pragma solidity 0.8.0 0.9.0; import {SVM} from ./SVM.sol; abstract contract SymTest { // SVM cheat code address: 0xf3993a62377bcd56ae39d773740a5390411e8bc9 address internal constant SVM_ADDRESS address(uint160(uint256(keccak256(svm cheat code)))); SVM internal constant svm SVM(SVM_ADDRESS); }关键点有三SymTest是abstract contract因此测试合约需要通过contract TokenTest is SymTest, Test的方式继承它Test来自 forge-stdSVM 并非部署在真实链上的合约而是通过keccak256(svm cheat code)派生出的固定地址0xf3993a62377bcd56ae39d773740a5390411e8bc9。这与 forge-std 中vm的机制一致——调用该地址由符号执行工具拦截处理属于典型的 cheatcode 设计模式合约使用pragma solidity 0.8.0 0.9.0;。当前仓库根目录 foundry.toml 配置的编译器为solc 0.8.34位于该区间内满足编译兼容性。源码剖析二SVM 提供的完整 cheatcode 接口SVM.sol 是一个interface其中声明的每个函数都对应一种创建符号值或操纵符号状态的能力。完整接口如下// SPDX-License-Identifier: AGPL-3.0 pragma solidity 0.8.0 0.9.0; /// notice Symbolic Virtual Machine interface SVM { // 创建一个新的符号 uint取值范围为 [0, 2**bitSize - 1]含端点 function createUint(uint256 bitSize, string memory name) external pure returns (uint256 value); // 创建一个新的符号 uint256 function createUint256(string memory name) external pure returns (uint256 value); // 创建一个新的符号有符号整数 function createInt(uint256 bitSize, string memory name) external pure returns (int256 value); // 创建一个新的符号 int256 function createInt256(string memory name) external pure returns (int256 value); // 创建一个指定字节长度的符号字节数组 function createBytes(uint256 byteSize, string memory name) external pure returns (bytes memory value); // 创建一个由符号数组支撑的、指定字节长度的符号字符串 function createString(uint256 byteSize, string memory name) external pure returns (string memory value); // 创建一个新的符号 bytes32 function createBytes32(string memory name) external pure returns (bytes32 value); // 创建一个新的符号 bytes4 function createBytes4(string memory name) external pure returns (bytes4 value); // 创建一个新的符号地址 function createAddress(string memory name) external pure returns (address value); // 创建一个新的符号布尔值 function createBool(string memory name) external pure returns (bool value); // 为给定的合约或接口名称创建任意符号 calldata。 // 若合约名称存在于多个文件中会抛出异常可提供可选的文件名带 .sol 后缀以消除歧义。 // 默认排除 view 和 pure 函数可通过可选布尔标志包含它们。 function createCalldata(string memory contractOrInterfaceName) external pure returns (bytes memory data); function createCalldata(string memory contractOrInterfaceName, bool includeViewAndPureFunctions) external pure returns (bytes memory data); function createCalldata(string memory filename, string memory contractOrInterfaceName) external pure returns (bytes memory data); function createCalldata(string memory filename, string memory contractOrInterfaceName, bool includeViewAndPureFunctions) external pure returns (bytes memory data); // 为未初始化的存储槽分配符号值 function enableSymbolicStorage(address) external; // 快照指定账户的当前存储并返回快照 ID function snapshotStorage(address) external returns (uint256 id); }接口按能力可分为四组分组函数用途标量符号值createUint/createUint256/createInt/createInt256/createAddress/createBool/createBytes32/createBytes4生成覆盖整个类型取值空间的符号量用于模拟任意账户、任意金额等场景复合符号值createBytes/createString生成符号字节数组/字符串其中byteSize参数决定符号数组的长度上限符号 calldatacreateCalldata4 个重载依据合约 ABI 自动生成能命中任意非 view/pure 函数的符号调用数据是实现任意函数调用的核心符号存储enableSymbolicStorage/snapshotStorage把合约中未初始化的存储槽符号化或对存储做快照以便符号级回滚/比较值得注意的细节所有创建符号值的函数都被声明为external pure说明它们不是真正的链上计算纯粹是工具层面的占位createCalldata默认排除view/pure函数因为验证状态变更时只读函数一般无关紧要若确实需要覆盖只读函数可通过第二个布尔参数显式开启当多个文件定义同名合约时createCalldata会因歧义抛出异常此时必须通过带.sol文件名的重载版本消歧——这提醒我们在符号测试中保持合约文件名唯一。安装与工程接入README 给出了两种安装方式。第一种是使用 Foundry 包管理器forge install a16z/halmos-cheatcodes第二种是直接将其添加为 git 子模块git submodule add a16z/halmos-cheatcodes 仓库地址在 WTF-Solidity 仓库中halmos-cheatcodes 正是以子模块的形式被 OpenZeppelin 合约库带入实际路径为lib/openzeppelin-contracts/lib/halmos-cheatcodes。若要在自己的 Foundry 工程中直接使用从代码结构看还需在 foundry.toml 的remappings中补充类似下面的映射使halmos-cheatcodes/前缀能解析到包根目录remappings [ forge-std/lib/forge-std/src/, halmos-cheatcodes/lib/halmos-cheatcodes/src/ ]仓库根目录的 foundry.toml 目前只声明了forge-std/与openzeppelin/contracts/两组 remapping上述 halmos 映射是结合导入语句import {SymTest} from halmos-cheatcodes/SymTest.sol推断出的最小配置。实战示例检测他人代币是否可被非法转移README 给出的是一个非常经典的符号测试用例检查 ERC-20 代币合约是否存在调用者能花掉别人代币的执行路径。整体思路是先为代币合约设置任意初始符号状态再向它发起一次任意函数调用最后断言不存在使调用者余额增加、他人余额减少的路径。完整测试代码如下// import Halmos cheatcodes import {SymTest} from halmos-cheatcodes/SymTest.sol; import {Test} from forge-std/Test.sol; import {Token} from /path/to/Token.sol; contract TokenTest is SymTest, Test { Token token; function setUp() public { token new Token(); // set the balances of three arbitrary accounts to arbitrary symbolic values for (uint256 i 0; i 3; i) { address receiver svm.createAddress(receiver); // create a new symbolic address uint256 amount svm.createUint256(amount); // create a new symbolic uint256 value token.transfer(receiver, amount); } } function checkBalanceUpdate() public { // consider two arbitrary distinct accounts address caller svm.createAddress(caller); // create a symbolic address address others svm.createAddress(others); // create another symbolic address vm.assume(others ! caller); // assume the two addresses are different // record their current balances uint256 oldBalanceCaller token.balanceOf(caller); uint256 oldBalanceOthers token.balanceOf(others); // execute an arbitrary function call to the token from the caller vm.prank(caller); uint256 dataSize 100; // the max calldata size for the public functions in the token bytes memory data svm.createBytes(dataSize, data); // create a symbolic calldata address(token).call(data); // ensure that the caller cannot spend others tokens assert(token.balanceOf(caller) oldBalanceCaller); // cannot increase their own balance assert(token.balanceOf(others) oldBalanceOthers); // cannot decrease others balance } }分步解读搭建符号初始状态setUp循环 3 次每次用svm.createAddress(receiver)生成一个任意地址用svm.createUint256(amount)生成一个覆盖整个uint256取值空间的任意金额并执行token.transfer(receiver, amount)。注意这里传给createAddress/createUint256的字符串receiver、amount是符号值的名字用于在反例中定位变量同名会互相覆盖因此循环中的每次创建需保证语义可区分。确立两个任意且不同的账户checkBalanceUpdate测试函数命名为checkBalanceUpdate以check前缀开头——这是 Halmos 识别待验证属性的默认约定README 中所有被测函数均采用该命名。函数内再创建符号地址caller与others并通过vm.assume(others ! caller)forge-std 的假设约束排除调用者即受害者这一平凡情形。记录变更前的余额用token.balanceOf(...)捕获caller与others在任意调用前的余额作为基准。由于余额本身是符号值这里的比较是符号级比较。执行任意函数调用vm.prank(caller)把调用者伪造成callerdataSize 100是代币合约 public 函数所需 calldata 的最大长度svm.createBytes(dataSize, data)生成符号 calldata最后通过底层address(token).call(data)发起调用。这样一来符号执行器会枚举transfer等所有非 view/pure 函数以及所有可能的参数取值。断言不变量两条assert表达了安全属性——调用者不能让自己的余额增加balanceOf(caller) oldBalanceCaller也不能让别人的余额减少balanceOf(others) oldBalanceOthers。Halmos 若找到任何违反该属性的执行路径就会输出对应反例。被测试的有缺陷代币合约README 同时给出了用于验证上述测试的有问题的 Token 合约/// notice This is a buggy token contract. DO NOT use it in production. contract Token { mapping(address uint) public balanceOf; constructor() public { balanceOf[msg.sender] 1e27; } function transfer(address to, uint amount) public { _transfer(msg.sender, to, amount); } function _transfer(address from, address to, uint amount) public { balanceOf[from] - amount; balanceOf[to] amount; } }该合约的漏洞在于_transfer是public且完全没有权限校验任何人包括caller都可以直接以任意地址为from调用它实现花别人的钱。这类漏洞在人工 code review 中极易被忽略——transfer表面上看是安全的从msg.sender转出真正的入口隐藏在公开的_transfer中。而符号测试通过createCalldata 底层call自动枚举所有 public 函数入口因而能发现caller调用_transfer(others, caller, amount)的路径并给出具体的反例输入。这正是 README 强调的Halmos 能提供人工审查可能遗漏的反例。仓库中的真实应用证据OpenZeppelin 的正式验证实践halmos-cheatcodes 并不是孤立存在的文档示例它在当前仓库的 OpenZeppelin 合约库中有真实落地依赖版本锁定在 lib/openzeppelin-contracts/fv-requirements.txt该文件明确声明halmos0.3.3并附注释说明这是为了避免与最新 Python 版本0.3.8不兼容而做的固定属于形式化验证Formal Verification流程的一部分多个测试文件直接导入并使用SymTest例如 test/utils/ShortStrings.t.sol 中的contract ShortStringsTest is Test, SymTest此外Arrays、SlotDerivation、Math、SignedMath等工具库测试同样引用了 Halmos 相关符号测试符号可通过搜索SymTest在lib/openzeppelin-contracts/test下确认。这说明以符号执行为核心的 cheatcode 用法已被 OpenZeppelin 这类以安全著称的库用于其标准组件如ShortStrings、Math、SlotDerivation的属性验证。在阅读 WTF-Solidity 教程中的 ERC20.sol、ERC721.sol 等章节时若想进一步做形式化层面的安全确认halmos-cheatcodes 提供的就是一条可落地的验证路径。使用注意事项与限制环境前提cheatcode 依赖 Halmos 在符号执行阶段的拦截因此测试需通过 Halmos 运行而非普通的forge test并以check前缀函数作为验证入口直接部署到真实链上并不会产生任何效果。calldata 歧义createCalldata在合约重名时抛异常需要提供文件名消歧默认不覆盖view/pure函数如需覆盖必须显式传布尔标志。符号数量控制符号值的数量与位宽bitSize直接影响求解复杂度示例中把dataSize定为 100 正是出于规模控制实际使用时应根据目标合约的 ABI 谨慎设定。免责声明要点README 在 Disclaimer 中明确——这些合约与代码按原样as is提供不做任何明示或暗示的保证未经审计可能无法按预期工作用户可能遭遇延迟、失败、错误、遗漏或信息丢失不构成投资建议或法律意见使用前应在相关司法辖区咨询专业律师。适用范围文档明确指出 cheatcode 目前是 Halmos 专属未来才可能被其他符号测试工具支持因此 API 属于演进中的设计使用时建议锁定版本如 OpenZeppelin 锁定halmos0.3.3的做法。总结Halmos Cheat Codes 把符号执行的能力以一组抽象接口的形式开放给 Solidity 测试通过 SymTest.sol 继承获得svm句柄再借助 SVM.sol 中createAddress、createUint256、createBytes、createCalldata、enableSymbolicStorage等接口即可在测试中构建任意符号状态、发起任意函数调用并断言安全不变量。README 提供的代币越权检测示例完整演示了设置符号初始状态 → 任意调用 → 断言不变量 → 由 Halmos 输出反例的符号测试闭环OpenZeppelin 将其用于自身工具库的形式化验证进一步印证了这一方案在生产级代码库中的可信度。对于在 WTF-Solidity 教程基础上追求更高安全保证的开发者而言这组 cheatcode 是把审查靠眼升级为验证靠机器的关键一环。【免费下载链接】WTF-SolidityWTF Solidity 极简入门教程供小白们使用。Now supports English! 官网: https://wtf.academy项目地址: https://gitcode.com/GitHub_Trending/wt/WTF-Solidity创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考