A Language-Independent Approach To Smart Contract Verification

A Language-Independent Approach To Smart Contract Verification

A Language-Independent Approach To Smart Contract Verification Xiaohong Chen, Daejun Park, Grigore Rosu University of Illinois at Urbana-Champaign, USA November 05, 2018, ISoLA, Cyprus Smart Contract Snippet (ERC20) (one of the ~40,000 Ethereum ERC20s) Written in Solidity: ERC20 does not state that There should be no overflow when self-transfer 2

Attacks Happened. Many. Thats larger than $10703 ! What Can We Do About It? What can we do about execution environment to increase security? Blockchain clients Written in highlevel languages (Solidity, Vyper, etc.) Informal smart contract

standards Smart contracts running on VMs Consensus algorithms and protocols Unacceptable to build this complex potentially disruptive technology on top of poorly designed VMs and PLs. Ideal scenario feasible, stop compromising! Everything must be rigorously designed, using formal methods. Implementations provably correct!

Clients: provably correct VMs Smart contracts: well-designed PLs, with provably correct compilers or interpreters Verification: smart contracts 4 provably correct wrt their specs. Ideal language framework vision Parser Interpreter Deductive program verifier

Formal Language Definition (Syntax and Semantics) Model checker Compiler (semantic) Debugger Symbolic execution 5 Our Attempt: the K Framework http://kframework.org We tried various semantic styles, for ~15y

Small-/big-step SOS; Evaluation contexts; Abstract machines (CC, CK, CEK, SECD, ); Chemical abstract machine; Axiomatic; Continuations; Denotational; But each of the above had limitations Especially related to modularity, notation, verification K framework initially engineered: keep advantages and avoid limitations of various semantic styles Then theory came 6 Complete K definition of KernelC 7 Complete K definition of KernelC

Syntax declared using annotated BNF 8 Complete K definition of KernelC Configuration given as a nested cell structure. Leaves can be sets, multisets, lists, maps, or syntax 9 Complete K definition of KernelC Semantic rules given contextually rule

X = V => V X |-> (_ => V) 10 K scales Several large languages were recently defined in K: Java 1.4: by Bogdanas etal [POPL15] 800+ program test suite that covers the semantics JavaScript ES5: by Park etal [PLDI15] Passes existing conformance test suite (2872 programs) Found (confirmed) bugs in Chrome, IE, Firefox, Safari C11: Ellison etal [POPL12, PLDI15] 192 different types of undefined behavior 10,000+ program tests (gcc torture tests, obfuscated C, ) Commercialized by startup (Runtime Verification, Inc.)

+ EVM, IELE, Plutus, Solidity, Vyper 11 Ideal Language Framework Vision [K] Parser Interpreter Deductive program verifier Formal Language Definition (Syntax and Semantics) Model

checker Compiler (semantic) Debugger Symbolic execution 12 State-of-the-Art Redefine the language using a different semantic approach (Hoare/separation/dynamic logic) Language specific, non-executable, error-prone 13 Deductive

program verifier What We Want Formal Language Definition (Syntax and Semantics) Use directly the trusted executable semantics! Language-independent proof system Symbolic execution Takes operational semantics as axioms Derives reachability properties Sound and relatively complete for all languages!

14 Matching Logic [, LICS13, RTA15, OOPSLA16, FSCD16, LMCS17, ] Patterns (of each sort s) Structure Constraints Binders 15 Matching Logic Models

Patterns interpreted as sets (all elements that match them) as complement, as intersection, as union over all as intersection, as union over all as union over all x 16 Matching Logic Proof System First-Order Logic 13 Proof rules. Sound and complete C (1,, i-1,, i+1,, n) Technical (completeness) Local reasoning 17 Expressiveness Important logics for program reasoning can be framed as matching logic theories / notations

First-order logic Equality, membership, definedness, partial functions Lambda / mu calculi (least/largest fixed points) Modal logics x.e Hoare logics x.0(x,e) Dynamic logics

(x.e)e = e[e/x] LTL, CTL, CTL* x.e x. 0(x,e) Separation logic x.e = e[x.e/x] Reachability logic [e[/x] ] [x.e ] Knaster-Tarski Reachability Logic (Semantics of K) [LICS13, RTA14, RTA15,OOPLSA16] Rewrite rules over matching logic patterns: Can be expressed in matching logic: () is weak eventually Patterns generalize terms, so reachability rules

capture rewriting, that is, operational semantics Reachability rules capture Hoare triples [FM12] Sound & relative complete proof system Now proved as matching logic theorems 19 K = (Best Effort) Implementation of RL Reachability logic implemented in K, generically EVM IELE Plutus

Solidity Evaluated it with the existing semantics of C, Java, and JavaScript, and several tricky programs Morale: Performance is not an issue! 20 K framework vision Parser

Deductive program verifier Blo Interpreter ckc hai n La Definition FormalDLanguage efin ngu (Syntax and itiSemantics) on age Model

checker Compiler (semantic) Debugger Symbolic execution 21 KEVM: formal executable semantics of the Ethereum VM [CSL18] In Collaboration with IOHK Defined complete semantics of EVM in K https://github.com/kframework/evm-semantics

Passes all 40,683 tests of C++ reference impl. Only one order of magnitude slower than the official C++ implementation 22 What Can We Do with KEVM? 1) Generate and deploy correct-by-construction EVM client! IOHK has just done that, in collaboration with RV, as a Cardano testnet: 23 What Can We Do with KEVM? 2) Formally verify Ethereum smart contracts! RV is doing that, commercially. RV also won Ethereum Security grant to verify Casper. 24

Smart contract verification workflow rule transfer(To, Value) => true ... From From BalanceFrom => BalanceFrom -Int Value To BalanceTo => BalanceTo +Int Value Log => Log Transfer(From, To, Value)

requires To =/=Int From // sanity check andBool Value >=Int 0 andBool Value <=Int BalanceFrom andBool BalanceTo +Int Value <=Int MAXVALUE ERC20 Informal Business Logic Refinement ERC20-K formal executable high-level spec Refinement ERC20-EVM formal executable low-level spec that contains all EVM details [transfer] callData: #abiCallData("transfer", #address(TO_ID), #uint256(VALUE)) gas: {GASCAP} => _ refund: _ => _ requires: andBool 0 <=Int TO_ID andBool TO_ID andBool 0 <=Int BAL_FROM andBool BAL_FROM (RETURN RET_ADDR:Int 32 ~> _) localMem: .Map => ( .Map[ RET_ADDR := #asByteStackInWidth(1, 32) ] _:Map ) log: _:List ( .List => ListItem(#abiEventLog(ACCT_ID, "Transfer", #indexed(#address(CALLER_ID . . EVM Not Human Readable

If it must be (among other nuisences) low-level, then I prefer this: define public @sum(%n) { %result = 0 condition: %cond = cmp le %n, 0 br %cond, after_loop %result = add %result, %n %n = sub %n, 1 br condition after_loop: ret %result } 26 A New Virtual Machine (and

Language) for the Blockchain Incorporates learnings from defining KEVM and from using it to verify smart contracts IELE testnet (with IOHK): Register-based machine, like LLVM; unbounded* End of July18 IELE was designed and implemented using formal toolfrom ecosystem methods andWith semantics scratch! Until IELE, only existing or toy languages have been given formal semantics in K Not as exciting as designing new languages

We should use semantics as an intrinsic, active language design principle, not post-mortem 27 K Semantics of Other Blockchain Languages WASM (web assembly) in progress, by the Ethereum Foundation Solidity in progress, collaboration between RV and Sun Juns group in Singapore Plutus (functional) in progress, by RV following Phil Wadlers (@IOHK) design of the language Vyper in progress, by RV in collaboration with the Ethereum Foundation 28 Conclusion: This Can Be Done.

Parser Blo Interpreter Deductive program verifier ckc hai n La Definition FormalDLanguage

efin ngu a (Syntax and itiSemantics) on ges Model checker Compiler (semantic) Debugger Symbolic execution 29

Recently Viewed Presentations

  • 11.4: The Earliest Applications of Linear Algebra

    11.4: The Earliest Applications of Linear Algebra

    Cattle Problem. If thou art diligent and wise, O stranger, compute the number of cattle of the Sun, who once upon a time grazed on the fields of the Thrinacian isle of Sicily, divided into four herds of different colours,...
  • Práca s literatúrou a odkazovanie na použité zdroje

    Práca s literatúrou a odkazovanie na použité zdroje

    2. Citovanie a zoznam bibliografických odkazov Zásady publikačnej etiky Citovanie, citácia, citát, bibliografický odkaz Norma STN ISO 690 2.1. Zásady publikačnej etiky V odbornej práci riešite vedecký problém, preto je potrebné v prvej kapitole zmapovať súčasný stav riešenia danej problematiky...
  • START Control Technology What is control technology? What

    START Control Technology What is control technology? What

    Flow Chart Symbols. Go to Common K>ICT>Year 8>FLOWOL> Lesson 1. ... In Flowol there are several mimics that you can use. These are simulations that we can control using flow diagrams. Click USE MIMIC >Zebra Crossing. This is the mimic/simulation.
  • KS2 SATS - lancsngfl.ac.uk

    KS2 SATS - lancsngfl.ac.uk

    KS2 SATs Information Evening ... Task 45 minutes Tends to be non-fiction Handwriting is assessed from this piece Pip Davenport Imagine a person called Pip Davenport who became famous for inventing new kinds of funfair rides over a hundred years...
  • Graphing Station Lab - Loudoun County Public Schools

    Graphing Station Lab - Loudoun County Public Schools

    Design a line graph of the data and then answer the following questions. Analysis Questions. What is the dependent variable? (y-axis) What is the independent variable? (x-axis) What is the average number of tadpoles per sample? What is the optimum...
  • Jane Schaffer Writing Strategy

    Jane Schaffer Writing Strategy

    Triple-decker Paragraphs How to Write a Tasty, Juicy Paragraph A modified Jane Schaeffer paragraph Powerpoint created by Hollie Gustke and modified by Trina Mangione
  • Demo Days - rochester.edu

    Demo Days - rochester.edu

    UR Financials Demo Days - May 2014. Reporting Strategy - Summary. Challenges are lessening with each WD release, especially with Workday 23 in August 2014. But, incorporating new functionality will take some time. The goal is to update key reports...
  • Unit 1 - Matter and Qualitative Analysis

    Unit 1 - Matter and Qualitative Analysis

    UNIT 1 - MATTER AND QUALITATIVE ANALYSIS The Electromagnetic Spectrum, Bohr's Model, Chemical Bonding. ... Draw the Lewis Structure For. Ca H. N Ne Li Cl. ... Bromate BrO. 3-Chlorate ClO. 3-Nitrate NO. 3-Phosphate PO. 4. 3-Forming ionic compounds. Occur...