Formal Verification for Loopring Protocol Smart Contract version 2
This repository contains the Coq code used in the formal model and the formal proofs of Loopring Protocol Smart Contract version 2 (LPSC).
Quote from Loopring whitepaper:
Loopring Protocol Smart Contracts (LPSC): A set of public and free smart contracts that checks order-rings received from ring-miners, trustlessly settles and transfers tokens on behalf of users, incentivizes ring-miners and wallets with fees, and emits events.
Why Formal Verification
Formal verification describes the target systems by mathematical models, and proves their correctness and security by mathematical proofs. It is based on the strict and rigorous mathematics and logic, and therefore can cover all behaviors of the system (e.g., all possible combinations of inputs, all code path, etc.) and strictly guarantee the correctness and security which are precisely defined. Formal verification has been applied successfully in critical areas including astronautics, high-speed railway, nuclear power and aeronautics.
Smart contracts, especially those processing a large amount of assets, always puts high requirement for the correctness and security, which, we think, the formal verification can help a lot.
Formal Verification of LPSC
The formal verification of LPSC is composed of two parts - a formal model of LPSC, and a bundle of formal proofs of properties about the correctness and security of LPSC.
The formal model describes the behaviors of LPSC. It models LPSC by an abstract state machine. The machine state or world state models storage variables of contracts in LPSC. The state transition describes how a message call to LPSC changes the storage (i.e., the world state), emit events and return values.
Then we define a list of correctness and security properties of LPSC on the formal model, and prove they can be guaranteed by the formal model. As the formal model describes the behaviors of LPSC, we can imply LPSC can guarantee those properties as well.
The machine state is defined by following files:
The top-level state transition is defined by:
The state transition is further defined per contract:
Files in Libs/ are libraries which define types and structures used in the formal model and proofs.
Quick Check Proofs
Both the formal model and the formal proofs are implemented in the interactive proof assistant Coq. You can use Coq to automatically check the correctness of proofs.
Install opam by following official instructions.
Install Coq and other dependencies via opam.
$ opam init $ opam repo add coq-released http://coq.inria.fr/opam/released $ opam install coq.8.8.2 $ opam install coq-mathcomp-ssreflect
Clone this repository.
$ git clone https://github.com/sec-bit/loopring-protocol2-verification.git
Run Coq to check proofs.
$ cd loopring-protocol2-verification $ make
If you have any questions or suggestions for this repository, welcome to send them to following emails.