# Formal Verification on Smart Contract <!-- Put the link to this slide here so people can follow --> slides: https://hackmd.io/p/rJzvzC9TN#/ Note: Hello, everyone, I am chen yixi from cheng kung university. So, what is formal verification? and why do we need formal verification? --- ##  Debug challenges. Note: We had already spend a lot of time debuging compared to developing, and sometimes can not even make sure the efforts on debugging is actually meaningful. ----  Note: Most of the time, we have to deal with something we are not familiar with. So we have to use profiler or debuger to trace or sometime guess the workflow. ----  Confusing operations Note: For example, this is a very simple C implentation of getting an absolute value from a integer. If you are not used to bitwise operation, this might be a little confusing. And, if you think more about this function, how do we prove the correctness of this implementation ? ----  Note: The first idea come into my mind might solve it with brute force, under current processor structure, we assume the whole operation took 50 cycles, so for a 32-bit integer, we will have to use 30 seconds for verification. And for 64-bit integer, we will then have to use almost 4000 years only to verify this simple function. ---- ## Why not just edge case ? <!-- .element: class="fragment" data-fragment-index="1" --> Note: It sounds ridiculous to you, at least to me. So we use test case to detect some frequent mistakes like integer overflow. But how can we ganurantee the coverage of such test case ? And this is the exact counterexample for this implementation. ----  Compute arbitrary-precision square roots. Note: That is just a simplied example, and this is an real implementation on getting sqare root. This is way harder to get the meaningful test case. ----  Note: And you might think, "it was all because the bad alignment of the coding style" ---- ```c= #define crBegin static int state=0; switch(state) { case 0: #define crReturn(x) do { state=__LINE__; return x; \ case __LINE__:; } while (0) #define crFinish } int decompressor(void) { static int c, len; crBegin; while (1) { c = getchar() if (c == EOF) break; if (c == 0xFF) { len = getchar(); c = getchar(); while (len--) crReturn(c); } else crReturn(c) } crReturn(EOF); crFinish; } ``` Co-routined version of a decompressor for RLE Note: And this is a decompressor for run-length encoding ----  Note: Designing testcase to verify the correctness is always available, however, it is hard to evaluate the effectness and coverage of different test case. Especially when we didn't have a concrete expectation on the specification. ---  Note: I assumed that everybody has already know what is blockchain and smart contract, while Blockchain is a distributed ledger, and smart contract helps automate the trading process. ---- ## Cryptocurrency Theft  Note: We all heard about huge finanical loss on cryptocurrency, the security issue is somehow different than what we used to see before. ----  Note: Take the DAO event for example, this is a simplified version of the buggy function. ---- ## Normal Usecase  Atomic operation ?<!-- .element: class="fragment" data-fragment-index="1" --> Note: This is how the function "withdraw" should used. When someone, that say, the Wallet Contract tries to withdraw money from Contract DAO, it call function withdraw in Contract DAO, then function withdraw evaluate the value, then call back to Wallet Contract to notify it to receive money, and then modify DAO's balance. ---- ## Re-entrancy Abuse  Note: However, if we change the "receiver function" in Wallet Contract to call withdraw again, since DAO hasn't modify its balance yet, the attacker will be able to call withdraw function for unlimited time in this section. ---- ## Smart Contract Challenges 1. Transactions are processed after a delay<!-- .element: class="fragment" data-fragment-index="1" --> 2. Adversaries can re-order and “frontrun” transactions<!-- .element: class="fragment" data-fragment-index="2" --> 3. All smart contract data is public<!-- .element: class="fragment" data-fragment-index="3" --> 4. Execution is expensive (gas costs, tx fees)<!-- .element: class="fragment" data-fragment-index="4" --> 5. Code is difficult to change (“Code is law”)<!-- .element: class="fragment" data-fragment-index="5" --> Note: Bitcoin can take hours to confirm a tranction The order of transaction within a time section is not ganuaranteed. ---- ## Verification Tools  Note: So there are many automatic verification tool to assure the correctness of smart contract. Today we'll be focus on KEVM. --- ## Formal Verfication  Note: In KEVM, we re-write the spec into a formal semantic, and then verify it with the proof checker, in KEVM, it is pretty similar to compiler frontend, plus state transition to detect if there is a illegal operation. ---- ## Formal Semantics  [EIP 20: ERC-20 Token Standard](https://eips.ethereum.org/EIPS/eip-20) Note: So, what is formal semantics? Let's look at the ERC20-spec, erc20 spec is a smart contract standard for exchanging ethereum to other 3rd party token. As you can see here, there are some interface like balanceof(), approve(), and today we will be focus on transferfrom() Transfrom() allow the 3rd party account to help transfer money from other account to account, the caller should be the 3rd party account, and from account, to account. ----  Note: Before the 3rd party account calls "transferFrom()", from_account should first call approve() function to permit 3rd party account for a certain amount of money. This make sense, right? ----  1. Allowance: Should we modify it ?<!-- .element: class="fragment" data-fragment-index="1" --> 2. Gas: Potential Gas Depletion ?<!-- .element: class="fragment" data-fragment-index="2" --> Note: But what if the to_account and from_account is the same account ? First, should we modify the allowance since it is a weird transaction ? And since it should always be successful, do we have to check the transfer value to make sure it is small enough ? Finally, the meaningless contraction also consume gas, which might in the end deplete the total gas storage ? ---- ## Formal Verfication Is Not A Magic [runtimeverification/erc20-semantics/erc20.k](https://github.com/runtimeverification/erc20-semantics/blob/master/erc20.k)  /\*uint128 a = 1\*/ Note: Formal Semantic is the requirement of conducting formal verification, formal verfication is not a magic, you must have to be fully aware of the whole structure behavior and possible side effects, otherwise, it is totally useless. Especially while nowadays project structures are getting more and more complex, the difficulty to construct a formal semantic is getting harder and harder. So formal verification requires lots of time and efforts, so it is too hard for massive deployment. ---- ## Formal Verification <!-- .element: class="fragment" data-fragment-index="1" --> Note: But if you make it to the correct formal semantic of your specs and implementations, then we can move on to formal verification. Formal verification use the concept of symbolic execution. Take these two implementation for example, according to ERC20-spec, the totalSupply function should return the 3rd party token total amount, and the upper one should be the correct one, while the lower one is the crappy one. ---- ## Symbolic execution  Note: When there is a branch situatation, the workflow will split into applying different corresponding rule, and the whole graph is construct with series of condition state. Once the graph is completed, it will verify each available execution path by choosing a representing number that fullfill all the condition along with its path, and compare the result with spec and implementation. ----  when supply != 0x1000....0000 ----  when supply == 0x1000....0000 --- ## Reference 1. [Beginner Guide for EVM Execution](https://github.com/kframework/evm-semantics/blob/master/evm.md) 2. [K: A Semantic Framework for Programming Languages and Formal Analysis Tools, Grigore Rosu](https://pdfs.semanticscholar.org/7160/ab5a93942d49c3de7939e3699f21f51851a6.pdf) 3. [Detailed Kprove Beginner Guide](https://github.com/runtimeverification/verified-smart-contracts/blob/master/resources/kprove-tutorial.md) 4. [KAST syntax guide](https://github.com/kframework/k-legacy/wiki/KAST) 5. [Formal verification of ERC-20 contracts ( Very Useful )](https://runtimeverification.com/blog/erc-20-verification/) 6. [Formal Verification of HackerGold (HKG) ERC20 Token Contract](https://github.com/runtimeverification/verified-smart-contracts/tree/master/erc20/hkg) 7. [Formal verification of ERC-20 contracts](https://runtimeverification.com/blog/erc-20-verification/)