  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 sampled for concrete
validation and manual analysis, we reproduce real exploits at a true positive
rate of 89%, yielding exploits for3,686 contracts. Our tool finds exploits for
the infamous Parity bug that indirectly locked 200 million dollars worth in
Ether, which previous analyses failed to capture.
