Watch / Formally verified EVM golf and reverse bug bounties

Formally verified EVM golf and reverse bug bounties

  • YouTube
  • IPFS
  • Swarm
  • Details

Formally verified EVM golf and reverse bug bounties

Duration: 00:52:05

Speaker: Lev Livnev, Martin Lundfall

Type: Breakout

Expertise: Advanced

Event: Devcon 5

Date: Oct 2019

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.
  • Related