Verifying Economic Security of Smart Contracts via Unintended Return

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.