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.




posted by kleinbl00: 203 days ago