- 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
- Syntax
- K automatically generates:
- Parser
- Interpreter
- Symbolic debugger
- Reachability prover
- Note: these are not super optimized, but you get them for free!
- 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
- 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
trueorfalseback - This kinda sucks
- You write your proofs, and you just get a
- I.e., for any pre-state of this configuration, I can reach a post-state of this other configuration
- 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...
- 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...
- 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
- 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