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-tr...