TL;DR
This paper introduces MAIAN, a tool for detecting trace vulnerabilities in Ethereum smart contracts, revealing widespread issues including critical exploits like the Parity bug that locked billions of dollars.
Contribution
The paper presents MAIAN, the first systematic tool for analyzing trace vulnerabilities in smart contracts using inter-procedural symbolic analysis and concrete validation.
Findings
Identified 34,200 vulnerable contracts out of nearly one million analyzed.
Reproduced real exploits with an 89% true positive rate on sampled contracts.
Detected the Parity bug that locked 200 million dollars in Ether.
Abstract
Smart contracts---stateful executable objects hosted on blockchains like Ethereum---carry billions of dollars worth of coins and cannot be updated once deployed. We present a new systematic characterization of a class of trace vulnerabilities, which result from analyzing multiple invocations of a contract over its lifetime. We focus attention on three example properties of such trace vulnerabilities: finding contracts that either lock funds indefinitely, leak them carelessly to arbitrary users, or can be killed by anyone. We implemented MAIAN, the first tool for precisely specifying and reasoning about trace properties, which employs inter-procedural symbolic analysis and concrete validator for exhibiting real exploits. Our analysis of nearly one million contracts flags 34,200 (2,365 distinct) contracts vulnerable, in 10 seconds per contract. On a subset of3,759 contracts which we…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
