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. Continue reading...
