Home

Awesome

Token Libraries with Proofs

Build Status

This repository collects correctness proofs of Ethereum token contracts wrt. given specifications and high-level properties. All of them are accomplished in Coq.

Proofs of following contracts are included, and more will be added in the future.

Requirements

Coq is required if you are going to check the correctness of proofs in this repo. ProofGeneral or CoqIde is required if you are going to read the definitions and the proofs in this repo thoroughly.

Coq 8.8.0

Coq is an interactive proof assistant, which, as its name suggested, assists users to construct proofs. Its also provides a small proof checker that checks the correctness of the proof. It is required if you desire to check the correctness of proofs in this repo.

The definitions and the proofs are implemented in Coq 8.8.0 (other versions may or may not work), which can be installed by following the official instructions.

CoqIde

CoqIde is the official graphic front-end of Coq. It's usually installed along with Coq as shown in the above Coq installation instructions. It does not require further configurations after installation. If any, you can refer to the official instructions.

ProofGeneral

If you are an Emacs user, a more convenient front-end of Coq is ProofGeneral. The installation instructions of ProofGeneral can be found at https://proofgeneral.github.io/ and https://github.com/ProofGeneral/PG/blob/master/INSTALL.

Repo Structure

Quick Check Proofs

Coq proof checker can be invoked to check whether proofs are correct by the following command,

make

or if you want to check the proof of an individual contract,

cd erc20; make

Proving Process

Given a contract in Solidity, the proving process can be divided into following steps and may involve the change of the contract as shown in the following diagram. We take an ERC20 contract and its proof in erc20/ as an example to explain the process.

Proving Process

Define the Contract Model

The contract model abstracts the storage, the events, the message calls, and the external environment. The specification, high-level properties and proofs are all based on the contract model.

The model of different contracts can be defined in a similar form, so we separate the common definitions into the contract-independent part or the abstract model in AbsModel.v and the contract-specific part or the concrete model in Model.v under each contract directory. When proving a contract, we only need to generate the concrete model from the reused abstract model.

For example, the state of every contract can be composed of a contract address and values of storage variables, while the latter component is contract-specific. Thus, the contract state in the abstract model can be defined as below in AbsModel.v :

(* Abstract type of the contract *)
Record TContract(TState: Type): Type :=
  mk_contract {
      w_a: address; (* contract address *)
      w_st: TState; (* contract storage state *)
    }.

which requires a state TState of concrete storage variables to instantiate.

Correspondingly, the concrete contract state of a ERC20 can be defined from the abstract one as below in Model.v:

(* State of storage variables in ERC20 contract. *)
Record state: Type :=
  mk_st {
      st_symbol     : string;  (* symbol      *)
      st_name       : string;  (* name        *)
      st_decimals   : uint8;   (* decimals    *)
      st_totalSupply: uint256; (* totalSupply *)

      st_balances: a2v;        (* balances    *)
      st_allowed: aa2v;        (* allowed     *)
   }.

(* ERC20 contract state instantiated from TContract with state. *)
Definition contract := TContract state.

Note The current model in this repository only covers components that are neccesary to define and prove the following specifications and high-level properties. Other components, such the gas price and limit, nonce and a comprehensive block descriptions, will be added later.

Represent the Solidity Implementation in Coq

In order to prove a contract, we need to first represent it in Coq. Instead of supporting every syntax structure of Solidity, we choose to design a domain specific language in Coq whose syntax is simple but enough to express most Solidity contracts. DSL.v includes a definition of such domain specific language. By carefully manipulating notations in Coq, DSL can event present a close look as Solidity. For example, transfer() in DSL is defined as below in DSL.v:

  (* DSL representation of transfer(), generated from solidity *)
  Definition transfer_dsl : Stmt :=
    ((@require(balances[msg.sender] >= value)) ;
     (@require((msg.sender == to) || (balances[to] <= max_uint256 - value))) ;
     (@balances[msg.sender] -= value) ;
     (@balances[to] += value) ;
     (@emit Transfer(msg.sender, to, value)) ;
     (@return true)
    ).

Besides the syntax, it also needs to define the semantics of DSL as close to Solidity as possible. Because DSL is now generated per-contract, its semantics only needs to model a small portion of Solidity, such as dsl_exec and dsl_exec_prim in DSL.v.

Both the generation of DSL definition and the conversion from Solidity to DSL can be automated.

Define the Contract Specification

The specification in this repo defines the expected behavior of each contract function. The specification is defined in a form like Hoare tuple composed of two parts:

Prove Against the Specification

Proofs in this step is to show each contract function in DSL does implement the corresponding specification. For example, we prove the following lemma in DSL.v to verify transfer() function.

  Lemma transfer_dsl_sat_spec:
    forall st env msg this,
      spec_require (funcspec_transfer _to _value this env msg) st ->
      forall st0 result,
        dsl_exec transfer_dsl st0 st env msg this nil = result ->
        spec_trans (funcspec_transfer _to _value this env msg) st (ret_st result) /\
        spec_events (funcspec_transfer _to _value this env msg) (ret_st result) (ret_evts result).

The proving is accomplished by constructing the starting state, the ending states and the logged events from definitions of dsl_exec and transfer_dsl, and then checking whether those states and events can satisfy the conditions required by the specification spec_trans and spec_events.

If the proving cannot be accomplished, it may imply bugs in the Solidity implementation. By analyzing the location where the proving gets stuck and the reason, we can get what modifications are required. After the necessary update, we can restart from the first step.

Define the High-level Properties

The high-level properties define the expected behavior when all functions in a contract work as a whole. For example, the total supply in a ERC20 contract should always be the same as the sum of all balances, which can be defined as below in Prop.v:

Theorem Property_totalSupply_equal_to_sum_balances :
  forall env0 env msg ml C E C' E',
    create env0 msg C E
    -> env_step env0 env
    -> run env C ml C' E'
    -> Sum (st_balances (w_st C')) (st_totalSupply (w_st C')).

Prove Against the High-Level Properties

The proving of high-level properties is accomplished upon specifications. Because it has been proved that each contract function does implement its specifications, we can imply that the contract as a whole satisfies the high level properties. The proofs of above properties and other high-level ERC20 contract properties can be found in Prop.v.

If the proving cannot be accomplished, it may imply bugs in the Solidity implementation. By analyzing the location where the proving gets stuck and the reason, we can get what modifications are required. After the necessary update, we can restart from the first step.

How to Contribute

The correctness of proofs in this repo still relies on the correctness of all definitions, the conversion from Solidity to DSL, and Coq, which can not be verified in the same logical system. If you find any errors and/or have any suggestions, you are very appreciated to open issues and/or send us pull requests.

Related Work

Acknowledgement

We would like to thank Yi Tang (ConsenSys), Yuhui Wu (轻信科技), and Zhong Zhuang (DEx.top) for their suggestions and help.

Disclaimers

This repository is to demonstrate how the real world smart contracts can be formally proved in Coq, rather than providing smart contracts that can be used in arbitrary usage scenarios.

  1. The correctness of every proved contracts in this repo is defined against the given specifications and high-level properties, which may or may not fit a specific usage scenarios.
  2. The proof is only valid for the given contract implementation. Any changes in the contract implementation may invalidate the proof.
  3. The reliability and the correctness of proved contracts depend on the correctness of all definitions in this repo, the conversion from Solidity to DSL, and Coq, which cannot be verified in the same logical system where proofs are checked. Any errors in those components would invalidate the contract correctness.

In addition, as licensed as LGPL v3, all artifacts in this repository are distributed in the hope it will be useful, but without any warranty, without even the implied warranty of merchantability or fitness for a particular purpose.