SHARE

TWEET

# Untitled

a guest
Oct 11th, 2018
78
Never

**Not a member of Pastebin yet?**

**, it unlocks many cool features!**

__Sign Up__- # 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

RAW Paste Data

We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.