Research Summary: Finding Bugs Automatically in Smart Contracts with Parameterized Invariants

Auditing and Security
, ,
1

TLDR
The most difficult part of verification is expressing the desired properties of the program (i.e. specification). However, invariants appear across different software versions and platforms. Keeping a library of reusable invariants could reduce the cost of formal verification. The researchers share several useful invariants they’ve already identified and propose a specification framework that formalizes them using parameterized Hoare triples.

Citation

  • Bernardi, T., Dor, N., Fedotov, A., Grossman, S., Immerman, N., Jackson, D., … & Wilcox, J. R. (2020). WIP: Finding Bugs Automatically in Smart Contracts with Parameterized Invariants. Retrieved July, 14, 2020.

Link

Core Research Question

  • If the best way to ensure program correctness is formal program verification, how can math and logic prove a program behaves appropriately as a mechanism for early bug detection?

Background

  • Formal program verification: Formal verification can provide a reliable guarantee for blockchain smart contract security. This paper summarizes five kinds of security issues in smart contracts and presents formal verification invariants for these issues.
    • MakerDAO’s mint function didn’t set a token supply limit, thus establishing a formal verification framework that can effectively verify the security vulnerabilities of smart contracts.
    • To verify a smart contract, we need to produce a formal specification stating what the smart contract is supposed to do.
  • KEVM is the K semantics of the Ethereum Virtual Machine. It passes all of the Ethereum Test Suite, and is used for verifying EVM programs.
  • The KEVM paper mentions that runtime verification, which uses the K framework (rewrite-based executable semantic framework)[1].
  • Hoare triple: the term comes from the field of Axiomatic Semantics of programs. has three parts, a precondition P, a program statement or series of statements S, and a postcondition Q. It’s usually written in the form {P} S {Q} following:

if P then { C;

assert Q; }

{P} C {Q} where P and Q are Boolean conditions and C is a sequence of instructions to denote that if the execution of C on input states satisfying P, terminates then the resulting state must satisfy Q.

  • Reusable invariants: These invariants could be evaluated and checked by the community of developers and users in three steps:
    • The first step is to define that an informal label such as Bounded Supply infinite minting is not possible.
    • The second step is formalized invariants, for example, token supply, can be represented by different contracts, this step representation problem using parameterized invariants.
    • The third step is to check the code against the invariant.
  • Bounded supply: Sum of the token supply defined by smart contract creator.
  • Aggregated ledger integrity: is defined as a relationship between a collection of values and their aggregated values, often separately maintained. Aggregated Ledger Integrity relates a more intricate relationship between the total amount of collateral stored and the total debt issued, such as those used in Compound and Maker.
  • Robustness: is a property that relates two similar executions. If two executions differ slightly in their inputs, then the difference in the effects of the executions is also small.
  • Authorized operation: operations should only be executed by users with privileges. For example, with the mint function only smart contract owners should be able to execute this function.
  • Proportional token distribution: a fair exchange of value. One should not be able to exchange an asset worth nothing with a positively valued asset.

Summary

  • This paper approaches proofs that use reachability logic, a generalization of Hoare logic, separation logic, and modal logic, and are performed using the K-framework.
  • Reusable smart contract invariants can detect if two contracts capture similar concepts using different interface names, the parameterized invariants would be detected using parameterized Hoare triples.

Method

  • Define Reusable smart contract invariants below:

1600×675 91.9 KB

Here describe one of the invariants in more detail, beginning with Bounded Supply. Assume that the token implements a totalSupply() function as part of its interface which returns the current number of tokens. The property requires that the values returned by totalSupply() are bounded.

1130×154 6.22 KB

totalSupply() ≤ b is an invariant that should hold after every transaction. This property is instantiated with a totalSupply() function and a bound b. It requires that throughout the execution, the supply does not exceed b.

  • Reusable smart contract invariants property

This paper defines the reusable smart contract invariants and specific each invariant’s property including (1) bounded supply, (2) aggregated ledger integrity, (3) Authorized operation, (4) Proportional token distribution, (5) Robustness. Then give each invariant logic reason to identify the property.

Results

  • This work discovered that 8 out of 24 types of tokens checked to violate reusable smart contract invariants this rule while the remaining 16 satisfy this rule.
  • MakerDAO’s auction code implements an auction where the prize has decreasing value, and the payment stays constant. A bidder that reduces the prize is set as a tentative winner. This paper detected that it violated Bounded Supply because the implementation of balanceOf is standard, and not to be given.

1066×146 5.78 KB

|522x196.84046674125614
|522x196.840466741256141416×534 57.6 KB

1600×439 64.6 KB

A trace which shows a bug in the Maker MCD test version allowing infinite minting, the trace demonstrates that the supply can reach 2256 tokens.

1600×468 110 KB

The violating method in the MCD code is called deal and it is the equivalent to close in our simplified example. The figure also shows the concrete supply values in the counterexample produced by the tool, which are 0x1fff initially and 0xf…f finally.

  • This paper applicability of different invariants to influential projects in the Ethereum community shown Table below:

1600×267 32.9 KB

  1. Compound Finance violates Bounded Supply because the implementation of balanceOf is standard, and not to be given.
  2. Celo violates Proportional token distribution because it should not be able to exchange an asset worth nothing with a positively valued asset.

Discussion & Key Takeaways

  • The formal verification process is limited to its steps, even the standard reusable invariants are identified following Hoare triple principle. The first step is to informally define that an informal label such as Bounded Supply infinite minting is not possible. Define the invariants and property of bounded supply, aggregated ledger integrity, authorized operation, proportional token distribution, and robustness still need to be more detailed about the content.

Implications & Follow-ups

  • Smart contract automatic verification process methods can be improved since many different contracts obey the same set of invariants.
  • Smart contract parameter dependence could also be one of the checkpoints to verify, it can easily detect the related invariants between smart contracts.

Applicability

  • Automatic finding bugs in a smart contract is implemented in the different project following K framework:
    • KWasm
      • KWasm is the K semantics of WebAssembly. WebAssembly is a low-level assembly language. More recently, it has been used in several blockchain smart-contract platforms as the underlying language for executing financial agreements. KWasm has been used for measuring coverage of test-suites over Wasm code and verifying programs that are compiled to Wasm.
      • Advantage: fast execution engine for browser-based tools.
      • Disadvantage: programs developed using low-level languages are machine-dependent and are not portable.
    • KEVM
      • KEVM is the K semantics of the Ethereum Virtual Machine. It passes all of the Ethereum Test Suite, and is used for verifying EVM programs, which powers the Cardano blockchain testnet framework. KEVM is using a runtime verification applied in this paper.
      • Advantage: This method would check every reusable invariants and property while running
      • Disadvantage: It may take a longer time to detect all the checkpoints.
    • K-Michelson
      • K-Michelson is the K semantics of Michelson blockchain programming language, which powers the Tezos blockchain. K-Michelson provides additional testing tools for developers. K-Michelson is using a runtime verification framework.
      • Advantage: a unit-testing framework that is extendable to symbolic property testing.
      • Disadvantage: It may take a longer time to detect all the checkpoints.
5 Likes