Formal verification: the road to complete security of smart contracts (SBC19)

formal_verification_makerdao.md

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?
      • Here, formal methods are extremely useful!
    • 2. Dapp / system invariants
      • What can happen over the course of many transactions? (Or what can never happen?)
      • Here, formal methods are kinda OK.
    • 3. (Harder) Blockchain-specific assurances
      • Are we assured against eclipse attacks? Replay attacks? Chain reorgs?
      • Here formal methods can't do much.
    • 4. (Hardest) Incentive reasoning
      • How will a self-interested, rational actor behave in your protocol?
      • Likewise, formal methods are not so effective.
        • There are formal methods that can automatically find Nash Equilibria
          • But haven't really been used in blockchain contexts
    • (Note: we're excluding tools for determining the correctness of cryptographic protocols)
• 1. EVM Bytecode Verification
  • One paradigm for defining operational semantics is to rewrite logic
  • KEVM, a.k.a. "The Jello Paper" has the semantics of the EVM defined in K
  • By defining the EVM in K, you automatically get a compiler, debugger, verification engine
    • All for free!
  • Can express reachability claims:
    • S requires P(S) rewritten as S' requires P(S')
      • S = Ethereum state, defined as KEVM configuration
    • Then does an exhaustive search using symbolic execution
      • Branches through all possible symbolic executions until error or out of memory
  • Where MakerDAO adds to reachability analysis:
    • KLab Act, MakerDAO's specification format that pares down much of the relevant state
    • Makes it easier to express invariants
    • Act can be converted to K reachability rules
  • KLab has more functionality though!
    • Has a proof debugger
      • Normally K's prover only outputs True or False
    • But KLab debugger lets you step through a symbolic execution
      • Like any debugger, but lets you view symbolic values for variables! Whoo!
• How to write provable smart contracts?
  • Keep code as modular and simple as possible
  • Think in EVM, not in Solidity
  • Methods should do one thing under the right conditions and REVERT otherwise
  • Avoid calls to unknown code as much as possible
  • Contract inheritance and use of libraries sweeps complexity under the rug
• Overall security of Dapps
  • Once you've written complete specifications for all contracts...
    • That essentially defines a dapp
  • Any bytecode that verifies against these specifications should be just as good as the canonical implementation
  • What about bytecode that passes the specs but is otherwise faulty?
    • The false positive rate is a key consideration for any formal verification process
    • I.e., what "malicious programs" would slip through the cracks of this process?
  • Reverse bug bounties
    • Ask for people to submit bytecode that passes your specs but is "faulty", pay out bounties
• 2. System invariants
  • Once a complete spec has been proven, the specs define the atomic steps of a small state machine
  • This makes it much easier to reason about what your system requires!
  • Can model your system as a series of state transitions
    • And contract methods are now "first class" primitives for transitioning between states
  • By induction, can prove your invariants hold over every state transition
• Future of formal verification
  • Server-client based KLab - verifying your contracts in the browser
  • Documentation generation from specs alone
  • Symbolic exploration tools for bytecoe in the wild(!)
  • Viper, WASM support
  • Formal methods to tackle "blockchain-specific" properties, incentives