Vandal: A Scalable Security Analysis Framework for Smart Contracts
Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, Francois Gauthier, Vincent Gramoli, Ralph Holz, Bernhard Scholz
TL;DR
<3-5 sentence high-level summary>Vandal tackles the security-analysis challenge of Ethereum smart contracts by enabling direct analysis of EVM bytecode through a logic-driven, declarative framework. It builds a four-stage pipeline (Scraper, Disassembler, Decompiler, Extractor) to convert bytecode into logic relations and expresses vulnerability checks in Soufflé, enabling rapid prototyping of new analyses. The approach delivers large-scale empirical results, decompiling over $141{,}000$ unique bytecodes with an average runtime of $4.15$ seconds and outperforming established tools like Oyente, EthIR, Mythril, and Rattle. This work advances practical security auditing for deployed contracts and supports scalable benchmarking of contract vulnerabilities.
Abstract
The rise of modern blockchains has facilitated the emergence of smart contracts: autonomous programs that live and run on the blockchain. Smart contracts have seen a rapid climb to prominence, with applications predicted in law, business, commerce, and governance. Smart contracts are commonly written in a high-level language such as Ethereum's Solidity, and translated to compact low-level bytecode for deployment on the blockchain. Once deployed, the bytecode is autonomously executed, usually by a %Turing-complete virtual machine. As with all programs, smart contracts can be highly vulnerable to malicious attacks due to deficient programming methodologies, languages, and toolchains, including buggy compilers. At the same time, smart contracts are also high-value targets, often commanding large amounts of cryptocurrency. Hence, developers and auditors need security frameworks capable of analysing low-level bytecode to detect potential security vulnerabilities. In this paper, we present Vandal: a security analysis framework for Ethereum smart contracts. Vandal consists of an analysis pipeline that converts low-level Ethereum Virtual Machine (EVM) bytecode to semantic logic relations. Users of the framework can express security analyses in a declarative fashion: a security analysis is expressed in a logic specification written in the \souffle language. We conduct a large-scale empirical study for a set of common smart contract security vulnerabilities, and show the effectiveness and efficiency of Vandal. Vandal is both fast and robust, successfully analysing over 95\% of all 141k unique contracts with an average runtime of 4.15 seconds; outperforming the current state of the art tools---Oyente, EthIR, Mythril, and Rattle---under equivalent conditions.