Good ideas and conversation. No ads, no tracking. Login or Take a Tour!
- 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 of 3,759 contracts
which we sampled for concrete validation and manual
analysis, we reproduce real exploits at a true positive rate
of 89%, yielding exploits for 3,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.