Formal Analysis of Arithmetic Vulnerabilities in EVM Smart Contracts: Exploits and Mitigation Strategies

Smart contracts, particularly within the Ethereum ecosystem, form the backbone of decentralized finance (DeFi) applications, managing digital assets of substantial value. The correctness and security of these programs are therefore of critical importance. Arithmetic vulnerabilities, such as integer overflow and underflow, represent a class of programming flaws that, while subtle, can lead to catastrophic consequences, including unauthorized token creation and fund drainage. This whitepaper presents a formal and in-depth analysis of these vulnerabilities in the context of the Ethereum Virtual Machine (EVM). Using a state transition system model, we dissect the fundamental anatomy of an overflow exploit. We analyze in depth the historical case of the batchOverflow exploit (CVE-2018-10299) in the Beauty Chain (BEC) token, mathematically demonstrating how EVM's modular arithmetic was exploited.