Formally Verified EVM Golf and Reverse Bug Bounties by Martin Lundfall, Lev Livnev (Devcon5)

Fri, Oct 2, 2020, 12:00 AM

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more. https://archive.devcon.org/archive/watch/5/formally-verified-evm-golf-and-reverse-bug-bounties With the formalized semantics of the EVM in the K framework (the Jello paper), a new arsenal of analysis tools has become available for Ethereum smart contract development. This workshop will demonstrate how this tooling can be used to verify the complete behavior of smart contracts, sharing the techniques and tools used to verify the core contracts of multicollateral dai.We will demonstrate the power of formal verification by presenting the Ethereum community with two challenges:In the first one, we invite the workshop participants to a round of formally verified EVM golf. The most gas efficient implementation of an ERC20 contract which provably matches the specification wins!In the second challenge, the task is to challenge the specification itself, by writing a passing adversarial smart contract. In this "reverse bug bounty", participants are invited to poke holes in a specification by writing smart contracts which satisfy the postulated requirements but are otherwise faulty in some way. Speaker(s): Lev Livnev, Martin Lundfall Skill level: Advanced Track: Developer Infrastructure Keywords: technical Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum Learn more about devcon: https://www.devcon.org/ Learn more about ethereum: https://ethereum.org/ Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. Devcon 5 was held in Osaka, Japan on Oct 8 - 11, 2019. Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/