WTF Solidity 工具篇：使用 Halmos Cheatcodes 在 Foundry 中编写符号执行测试-北京尧图网络

WTF Solidity 工具篇使用 Halmos Cheatcodes 在 Foundry 中编写符号执行测试【免费下载链接】WTF-SolidityWTF Solidity 极简入门教程供小白们使用。Now supports English! 官网: https://wtf.academy项目地址: https://gitcode.com/GitHub_Trending/wt/WTF-SolidityHalmos Cheat Codes 是面向符号执行Symbolic Execution测试而设计的一组 Solidity 抽象函数为测试合约提供在运行时创建任意符号值地址、整数、字节、calldata 等的能力。本篇文章以 WTF-Solidity 仓库内随 Foundry 工具链一同引入的 halmos-cheatcodes 源码为骨架讲解其安装方式、作弊码全量清单、源码实现原理并结合官方示例演示如何用符号测试自动化发现别人钱包代币被转走这类手工审查容易遗漏的安全漏洞让读者掌握一套可复用的符号化安全测试写法。为什么需要符号测试作弊码在传统单元测试与模糊测试fuzz testing中输入是具体的数值或随机生成的样本测试结果只覆盖被枚举到的有限执行路径而符号执行会把输入符号化为一段取值范围由求解器自动探索满足断言失效的所有路径从而给出反例counterexample。Halmos Cheat Codes 正是为此而生它们是抽象函数abstract functions用来在符号测试中创建新的符号值。按 README 的说明这些作弊码目前是 Halmos 专属但其设计并不绑定 Halmos未来也可能被其他符号测试工具支持。可以把它理解为Foundry 的vm作弊码负责操作具体的 EVM 环境而svm作弊码负责构造一个范围内的任意值二者配合即可写出覆盖全部可能状态的测试。在 Foundry 项目中安装 halmos-cheatcodes安装方式有两种均以 Foundry 工程forge命令行工具为前提。方式一forge install推荐forge install a16z/halmos-cheatcodes方式二直接添加为 git submodulegit submodule add https://github.com/a16z/halmos-cheatcodes安装后在测试合约中即可通过如下 import 使用与forge-std/Test.sol一并引入import {SymTest} from halmos-cheatcodes/SymTest.sol; import {Test} from forge-std/Test.sol;在本仓库中该库实际以依赖形式存在于 halmos-cheatcodes 目录其顶层结构只有src/SVM.sol、src/SymTest.sol、LICENSE与README.md四个文件是一个极简、无外部依赖的库因此非常容易嵌套引入。作弊码源码解析SVM 接口全量清单符号值由名为SVMSymbolic Virtual Machine符号虚拟机的接口提供完整定义见 src/SVM.sol。该文件声明了pragma solidity 0.8.0 0.9.0即要求在 Solidity 0.8.x 版本下使用与 WTF-Solidity 工具篇工程中solc 0.8.34的配置兼容。全部作弊码函数可归纳为以下清单函数签名作用createUint(uint256 bitSize, string name)创建取值范围为[0, 2**bitSize - 1]含端点的符号 uint 值createUint256(string name)创建符号 uint256 值createInt(uint256 bitSize, string name)创建符号有符号 int 值createInt256(string name)创建符号 int256 值createBytes(uint256 byteSize, string name)创建指定字节长度的符号字节数组createString(uint256 byteSize, string name)创建由符号数组支撑、指定字节长度的符号字符串createBytes32(string name)创建符号 bytes32 值createBytes4(string name)创建符号 bytes4 值createAddress(string name)创建符号地址createBool(string name)创建符号布尔值createCalldata(string contractOrInterfaceName)为指定合约/接口名创建任意符号 calldata合约名在多个文件中存在时会抛出异常可传入带.sol扩展名的文件名消歧义默认排除 view/pure 函数createCalldata(string contractOrInterfaceName, bool includeViewAndPureFunctions)同上可通过布尔标志决定是否包含 view/pure 函数createCalldata(string filename, string contractOrInterfaceName)带文件名消歧义的版本createCalldata(string filename, string contractOrInterfaceName, bool includeViewAndPureFunctions)完整参数版本enableSymbolicStorage(address)为未初始化的存储槽位赋符号值snapshotStorage(address)快照指定账户当前存储并返回快照 ID所有创建型函数的可见性均为external pure返回值是普通的 Solidity 类型因此可以像使用普通变量一样参与运算与断言。其中createCalldata是任意函数调用的核心它把整个 calldata 符号化让求解器自行挑选调用哪个函数、传什么参数来尝试打破你的不变量。SymTest 基类svm 作弊码从何而来Src/SymTest.sol 定义了需要被测试合约继承的抽象基类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); }关键点有二作弊码地址是确定的keccak256(svm cheat code)的低 160 位即为固定地址0xf3993a62377bcd56ae39d773740a5390411e8bc9。Halmos 工具在此地址注入符号执行逻辑因此测试合约无需部署任何辅助合约即可调用svm接口。svm是internal constant实例继承SymTest后测试合约内可直接使用svm.createAddress(...)、svm.createUint256(...)等方法无需额外初始化。需要说明的是SymTest只提供SVM接口这一个依赖测试中常用的vm.assume、vm.prank等仍是 Foundry 的Test合约提供的能力所以官方示例才同时继承SymTest, Test。实战用符号测试发现 Token 合约越权漏洞测试思路官方示例的目标是检查是否存在未授权访问他人代币的执行路径。思路是设置一个符号化的初始状态 → 执行一次任意函数调用 → 断言不变量不被打破让三个任意账户持有任意符号化的余额构造一个任意调用者caller与一个他人账户others由caller向 Token 合约发起一次符号化 calldata 的任意调用断言调用者的余额不会增加他人的余额不会减少。若存在违反该断言的执行路径Halmos 会给出反例。符号测试完整代码// 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 } }配套的带 bug 的 Token 合约官方文档配套给出了一个刻意有缺陷、禁止用于生产环境的 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且缺少余额检查与权限校验任何账户都可以直接以任意from、to、amount调用它。balanceOf[from] - amount在 Solidity 0.8.x 下遇到下溢会回滚但攻击者依然可以先把调用者的余额减到 0再把别人的余额转入自己名下从而实现减少他人余额、增加自己余额。运行与反例在 Foundry 工程中符号测试仍按普通测试编写与组织测试函数名以check开头而非 Foundry 默认的test前缀因为它是给 Halmos 运行的符号测试运行方式是在工程目录执行 Halmos 命令例如halmos --function checkBalanceUpdate。运行上述测试时Halmos 会找到一条违反断言的执行路径并输出反例——即一组具体的caller、others、calldata 取值直观展示调用者如何通过一次任意调用花掉了别人的代币这正是手工审查容易遗漏的边界场景。工程上下文与本仓库中的位置WTF-Solidity 工具篇Topics/Tools/TOOL07_Foundry/readme.md 系统介绍了 Foundry 的安装、forge/cast/anvil三大组件、作弊码与测试体系本文所述工程正是该讲对应的 hello_wtf 示例工程其 foundry.toml 使用solc 0.8.34并将lib与node_modules同时纳入库搜索路径。halmos-cheatcodes 的存放位置它作为 OpenZeppelin Contracts 的子依赖被带入位于 lib/openzeppelin-contracts/lib/halmos-cheatcodes读者可直接翻阅其src/目录核对上述接口定义。符号化思想在仓库中的延伸OpenZeppelin Contracts 还维护了独立的 fv/README.md 形式化验证说明基于 Certora与 Halmos 符号测试同属用形式化手段证明合约性质的实践两者互补符号测试更贴近日常安全回归形式化验证则追求更强的数学保证。注意事项与免责声明从源码与 README 中可以确认以下几点使用边界版本约束SVM.sol与SymTest.sol的pragma为0.8.0 0.9.00.9.x 及以上编译器无法直接编译。许可协议源码采用 AGPL-3.0 许可证商业闭源集成时需留意该许可的传染性要求。符号测试与普通测试的区分符号测试函数以check命名、依赖 Halmos 解释执行不能当作普通 Foundry 单元测试直接运行具体以你所用 Halmos 版本的命令行参数为准。官方免责声明halmos-cheatcodes 的智能合约与代码按原样as is提供未经过审计不保证安全性或正确性使用者需自担风险示例中的Token是刻意构造的缺陷合约严禁用于生产环境。文档同时强调仓库内容不构成投资或法律建议。总而言之Halmos Cheat Codes 用一组极简的接口把任意符号值引入 Solidity 测试配合 Foundry 的vm作弊码即可对合约的任意调用路径做穷举式安全探索。掌握svm.createAddress、svm.createUint256、svm.createBytes与createCalldata的组合用法你就能像官方示例那样在几行测试之内自动发现传统测试难以覆盖的越权漏洞。【免费下载链接】WTF-SolidityWTF Solidity 极简入门教程供小白们使用。Now supports English! 官网: https://wtf.academy项目地址: https://gitcode.com/GitHub_Trending/wt/WTF-Solidity创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考

WTF Solidity 工具篇：使用 Halmos Cheatcodes 在 Foundry 中编写符号执行测试

相关推荐

大模型定制化技术：RAG、Agent与微调实战解析

AI如何提升学术写作效率：从文献检索到查重降重

万达电影App headers check机制剖析：从抓包到签名算法还原

更多资讯

MATLAB电磁铁仿真：从磁路法到PDE的多物理场建模

基于Flink的实时风控系统实战：规则引擎、状态管理与数据集成全解析

OpenCV缝合线算法实战：消除图像拼接鬼影与接缝

用分数阶傅里叶变换(FRFT)实现chirp信号检测与参数估计

VulnHub mrrobot靶机实战：从信息收集到WordPress渗透与Linux提权全解析

在 awesome-codex-skills 中评估与接入 Zoho Desk 自动化：基于 Rube MCP 的工具发现、连接与替代方案实战

今日更新

基于高阶循环谱的MPSK载波频率估计与MATLAB实现

MiniPdf方：.NET开源Office转PDF的高效解决方案

Solon AI v3.10：Java全栈智能体开发框架解析

本周精选

AI驱动的自动化专利分析平台技术解析

LeetCode-Go 题解：1252. Cells with Odd Values in a Matrix（奇数值单元格计数）双解法剖析

在线答疑系统Java毕设实战：Spring Boot前后端分离与状态流转

本月热门

基于YOLO的焊缝缺陷检测：从数据标注到工业部署全流程实践

分布式服务的决策记录

创业产品的首版范围

读完文章，想聊聊您的网站？