Need a unique gift idea?
A Pastebin account makes a great Christmas gift
SHARE
TWEET

Untitled

a guest Oct 11th, 2018 80 Never
Upgrade to PRO!
ENDING IN00days00hours00mins00secs
 
  1. # Formally Verifying Dapps from the Ground up
  2. ## Martin Lundfall, MKR
  3.  
  4. # K Framework
  5. * Allows you to define a programming language by specifying a:
  6.   - Syntax
  7.     - via BNF notation
  8.   - Configuration
  9.     - state according to your VM, things like stack, memory, storage, etc.
  10.   - Rewrite rules
  11.     - How can you change the configuration according to terms you encounter
  12. * K automatically generates:
  13.   - Parser
  14.   - Interpreter
  15.   - Symbolic debugger
  16.   - Reachability prover
  17.   - Note: these are not super optimized, but you get them for free!
  18.  
  19. # KEVM
  20. * A complete specification of the EVM, written in the K framework
  21. * Like a formal, executable yellow paper
  22. * KEVM comes with a:
  23.   - Specification
  24.   - Is executable
  25.   - Verifier
  26.   - Debugger
  27.   - Evaluates gas usage
  28.  
  29. # KLab
  30. * In KEVM, you *do* have automatic reachability proofs
  31.   - I.e., for any pre-state of this configuration, I can reach a post-state of this other configuration
  32.     - You can prove these claims formally by exploring the complete state space
  33.     - (Is slow as hell, but hey)
  34.     - But if it finds a proof, you have a guarantee that the end-state is always reachable
  35.   - That said, it is completely opaque
  36.     - You write your proofs, and you just get a `true` or `false` back
  37.     - This kinda sucks
  38. * So we built KLab, a graphical debugger that allows you to see why your proofs are failing
  39.   - Basically an explorer of KEVM reachability proofs
  40.   - Allows you to view symbolic values on the stack as you traverse the state space
  41. * Also gives you concise ways to prove reachability in smart contracts
  42.   * By adding more boilerplate for reachability claims
  43. * Working on a web version of the interface...
  44.  
  45. # What this gives us
  46. * Currently in MKR, we have proofs for about half of the functions in our smart contracts
  47. * We want to guarantee that the EVM bytecode implements what we expect these functions do
  48. * Essentially we have moved from a small step semantics to a big step semantics
  49. * Only claims about what may happen over a single transaction
  50. * What about higher level properties of our smart contacts?
  51.   - Security against replay attacks?
  52.   - Frontrunning vulnerabilities?
  53.   - No ability to reason about incentives within formal verification...
  54.  
  55. # Dapp DSL
  56. * Allows us to reason about our system over multiple transactions, and establish higher-level invariants
  57. * A special DSL (domain-specific language) they created for reasoning about Dapps
  58.   - Syntax consists of a list of all possible functions in your Dapp
  59.   - Configuration consists of all state relevant to the dapp, abstracted from implementation details
  60. * DSLs exist for ERC20 and ERC777
  61. * Is blockchain-agnostic
  62.   - Cardano also has ERC20 implementations
  63. * For an ERC20 with fixed supply, you can prove invariants like:
  64.   - The sum of each user's balance = total supply
  65. * For MKR, you can prove:
  66.   - rate * (CDP debt + system debt) = total Dai supply
  67. * Kind of trivial, but adds a nice sanity check
  68.  
  69. # Future work
  70. * Reachability claims are totally exhaustive yet
  71.   - Gas constraints are not currently taken into account—this is tricky
  72. * 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. OK, I Understand
 
Top