A History of Greed: Practical Symbolic Execution for Ethereum Smart Contracts
摘要
Smart contracts have transformed blockchain applications, enabling decentralized computation and automated asset management without intermediaries. However, with the growth of decentralized finance, the high financial stakes make smart contract vulnerabilities particularly critical. Because vulnerabilities often go undetected, they lead to substantial losses and diminished trust in blockchain systems. Symbolic execution has emerged as a powerful technique to uncover subtle vulnerabilities by systematically exploring feasible execution paths. However, most existing symbolic execution tools for smart contracts are tailored to specific vulnerability patterns, making them unsuitable for detecting new types of vulnerabilities. In this paper, we introduce Greed, a highly versatile symbolic execution framework for Ethereum (or EVM-based) smart contracts. Greed features a state-of-the-art symbolic execution engine coupled with a suite of supporting analyses and a modular design that allows security researchers to prototype new analyses rapidly. To evaluate the effectiveness and extensibility of Greed, we compare it with the state-of-the-art. We first show that Greed can explore significantly more code paths – reaching 84% of all CALL statements, as opposed to 9% on average across existing tools. To demonstrate the ease of use (and extensibility) of Greed, we then implement a novel analysis to detect controllable JUMPI instructions and evaluate it against all deployed contracts on Ethereum and Binance Smart Chain (BSC), identifying 390 previously unknown vulnerable contracts. By releasing Greed to the community, we aim to lower the barrier to developing advanced security analyses for smart contracts, empowering security researchers to rapidly prototype new analyses and contribute to a more secure and resilient blockchain ecosystem.