Haseeb-Qureshi

Formal verification: the road to complete security of smart contracts

Martin Lundfall (MakerDao)

• What is formal verification?
  • Process of specifying and verifying the behavior of programs
  • Specification: mathematical description of intended program behavior
  • Verification: operational semantics of a language -> spec -> proof
  • There are 4 different "flavors" of assurances that formal verification can provide
    • 1. Smart contract bytecode verification - "Full description of EVM behavior"

• What can happen over the course of one transaction?

Haseeb-Qureshi

Betting on Blockchain Consensus with Fantômette

Speaker: Sarah Azouvi

• Bitcoin vs Traditional Consensus
  • Bitcoin is open memberships, participants unknown
  • One message broadcast per round
  • Incentives are at the core of its security
  • High energy consumption!
  • Slow...
• Blockchain without PoW?

Haseeb-Qureshi

Zexe: Enabling Decentralized Private Computation

Speaker: Pratyush Mishra

• How can we do computing on distributed ledgers?
  • Many existing systems for smart contract execution
    • Ethereum, Tezos, EOS, etc.
  • They all work through re-computation—every party redundantly performs the computations to agree on state
  • This comes with scalability tradeoffs
    • Recomputing all of these programs is costly

• Weakest computers (e.g. cell phones) can't keep up recomputing all transactions

Haseeb-Qureshi

Ethereum 2.0 and beyond

Vitalik Buterin (Ethereum Foundation)

• Ethereum 2.0 spec pre-release
  • Released yesterday!
• Proof of stake and sharding have been part of the ETH roadmap since 2014
  • Started with Slasher in 2014, which is totally broken
  • But since then have made a lot of progress
  • Casper FFG devised and formally verified

• Sharding is now better specified

Haseeb-Qureshi

// From: https://github.com/bitcoin/bitcoin/blob/master/src/chainparams.cpp

        vSeeds.emplace_back("seed.bitcoin.sipa.be"); // Pieter Wuille, only supports x1, x5, x9, and xd
        vSeeds.emplace_back("dnsseed.bluematt.me"); // Matt Corallo, only supports x9
        vSeeds.emplace_back("dnsseed.bitcoin.dashjr.org"); // Luke Dashjr
        vSeeds.emplace_back("seed.bitcoinstats.com"); // Christian Decker, supports x1 - xf
        vSeeds.emplace_back("seed.bitcoin.jonasschnelli.ch"); // Jonas Schnelli, only supports x1, x5, x9, and xd
        vSeeds.emplace_back("seed.btc.petertodd.org"); // Peter Todd, only supports x1, x5, x9, and xd
        vSeeds.emplace_back("seed.bitcoin.sprovoost.nl"); // Sjors Provoost
        vSeeds.emplace_back("dnsseed.emzy.de"); // Stephan Oeste

Haseeb-Qureshi

interface Lender {
  function goWild() external;
}

contract FlashERC20 is ERC20 {
  using SafeMath for uint256;
  
  function flash(uint256 amount) external {
    balances[msg.sender] = balances[msg.sender].add(amount);
    Lender(msg.sender).goWild();