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.