Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- # 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
Add Comment
Please, Sign In to add comment