Haseeb-Qureshi/formal_verification_makerdao.md

## formal_verification_makerdao.md

      
    Raw
  

              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


Smart contract bytecode verification - "Full description of EVM behavior"


What can happen over the course of one transaction?
Here, formal methods are extremely useful!


Dapp / system invariants


What can happen over the course of many transactions? (Or what can never happen?)
Here, formal methods are kinda OK.


(Harder) Blockchain-specific assurances


Are we assured against eclipse attacks? Replay attacks? Chain reorgs?
Here formal methods can't do much.


(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)


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


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