This pop-scientific conference paper introduces Mythril, a security analysis tool for Ethereum smart contracts, and its symbolic execution backend LASER-Ethereum. The first part of the paper explains symbolic execution of Ethereum bytecode in a largely formal manner. The second part showcases the vulnerability detection modules already implemented in Mythril. The modules use a pragmatic mix of static analysis, symbolic analysis and control flow checking.
8a7fc1857be351bac85ed32986c92e1568085599649c4da76ee6420d59f718c5