一句话：提出经济模型 CMod 与 Solidity 验证工具 CSol，通过证明不存在非预期单笔交易收益来验证 DeFi 合约的经济安全。
针对 DeFi 智能合约的经济安全，论文提出经济模型 CMod：它定义经济价值、预期收益条件与非预期单笔交易收益，并将经济安全归约为证明合约代码中不存在非预期单笔交易收益。基于该模型，作者协同设计 Solidity 自动验证工具 CSol，借助有界符号执行在多合约环境中推理路径性质，并引入三类优化：面向 CMod 的路径剪枝与归纳验证、证明目标化简以及求解器加速。评估表明，CMod 与 CSol 可应用于真实合约并刻画可被经济利用的漏洞：验证 245 个真实合约，识别 6 个活跃诈骗合约，检出 18 个真实攻击中的 16 个与 104 项审计阶段发现中的 92 项，并指出已有工具基准中的一处误判。
We propose CMod, an economic model for analyzing the economic security of decentralized finance (DeFi) smart contract code. CMod defines the notions of economic value, intended-return conditions, and unintended single-transaction return, and reasons about economic security by proving the absence of unintended single-transaction return. Based on CMod, we co-design CSol, an automated verification tool for Solidity that reasons about path properties in multi-contract environments via bounded symbolic execution. CSol incorporates three categories of optimizations: CMod-oriented path pruning and inductive verification, proof-goal simplification, and solver acceleration. Our evaluation shows that CMod and CSol can be applied to real-world contract code and characterize economically exploitable vulnerabilities. CSol verifies 245 real-world contracts, identifies 6 live scam contracts, detects 16 of 18 real-world exploits and 92 of 104 audit-stage findings, and exposes one misidentification in an existing tool's benchmark.
@article{paperbot12080,
title = {Verifying Economic Security of Smart Contracts via Unintended Return},
author = {Yi Rong and Xupeng Li and Ronghui Gu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839475}
}