# Formally Verifying Dapps from the Ground up
## Martin Lundfall, MKR

# K Framework
* Allows you to define a programming language by specifying a:
  - Syntax
    - via BNF notation
  - Configuration
    - state according to your VM, things like stack, memory, storage, etc.
  - Rewrite rules
    - How can you change the configuration according to terms you encounter
* K automatically generates:
  - Parser
  - Interpreter
  - Symbolic debugger
  - Reachability prover
  - Note: these are not super optimized, but you get them for free!

# KEVM
* A complete specification of the EVM, written in the K framework
* Like a formal, executable yellow paper
* KEVM comes with a:
  - Specification
  - Is executable
  - Verifier
  - Debugger
  - Evaluates gas usage

# KLab
* In KEVM, you *do* have automatic reachability proofs
  - I.e., for any pre-state of this configuration, I can reach a post-state of this other configuration
    - You can prove these claims formally by exploring the complete state space
    - (Is slow as hell, but hey)
    - But if it finds a proof, you have a guarantee that the end-state is always reachable
  - That said, it is completely opaque
    - You write your proofs, and you just get a `true` or `false` back
    - This kinda sucks
* So we built KLab, a graphical debugger that allows you to see why your proofs are failing
  - Basically an explorer of KEVM reachability proofs
  - Allows you to view symbolic values on the stack as you traverse the state space
* Also gives you concise ways to prove reachability in smart contracts
  * By adding more boilerplate for reachability claims
* Working on a web version of the interface...

# What this gives us
* Currently in MKR, we have proofs for about half of the functions in our smart contracts
* We want to guarantee that the EVM bytecode implements what we expect these functions do
* Essentially we have moved from a small step semantics to a big step semantics
* Only claims about what may happen over a single transaction
* What about higher level properties of our smart contacts?
  - Security against replay attacks?
  - Frontrunning vulnerabilities?
  - No ability to reason about incentives within formal verification...

# Dapp DSL
* Allows us to reason about our system over multiple transactions, and establish higher-level invariants
* A special DSL (domain-specific language) they created for reasoning about Dapps
  - Syntax consists of a list of all possible functions in your Dapp
  - Configuration consists of all state relevant to the dapp, abstracted from implementation details
* DSLs exist for ERC20 and ERC777
* Is blockchain-agnostic
  - Cardano also has ERC20 implementations
* For an ERC20 with fixed supply, you can prove invariants like:
  - The sum of each user's balance = total supply
* For MKR, you can prove:
  - rate * (CDP debt + system debt) = total Dai supply
* Kind of trivial, but adds a nice sanity check

# Future work
* Reachability claims are totally exhaustive yet
  - Gas constraints are not currently taken into account—this is tricky
* Can use the dapp DSL to explore agent-based modeling