Credit: Bernhard Muller
Stealing carbon credits is so mid-2000s, but now blockchain technologies make hacking-for-cash a reality we can all enjoy! This research presents an approach for modeling Ethereum contracts for symbolic analysis, and provides examples to show the possibilities of applying SMT solving against Solidity programs. As program complexity often makes this sort of analysis impractical, this paper posits that stealing digital currency makes it worth the effort the simplicity of the Ethereum VM makes smart contracts eligible for real-world application of symbolic analysis.