Skip to content

Instantly share code, notes, and snippets.

@Haseeb-Qureshi
Created February 3, 2019 18:29
Show Gist options
  • Save Haseeb-Qureshi/d2c9392d1e3b733f2c55c30682767dec to your computer and use it in GitHub Desktop.
Save Haseeb-Qureshi/d2c9392d1e3b733f2c55c30682767dec to your computer and use it in GitHub Desktop.
Formal verification: the road to complete security of smart contracts (SBC19)

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!
        1. Dapp / system invariants
        • What can happen over the course of many transactions? (Or what can never happen?)
        • Here, formal methods are kinda OK.
        1. (Harder) Blockchain-specific assurances
        • Are we assured against eclipse attacks? Replay attacks? Chain reorgs?
        • Here formal methods can't do much.
        1. (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
    1. 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment