Formal verification of smart contracts in the ConCert framework

Hey! My name's Kirill Ziborov and I'm a member of the Distributed System Security team at Positive Technologies. In this article, I'll be continuing the discussion of methods and tools for the formal verification of smart contracts and their practical application to prevent vulnerabilities. The main focus will be on the deductive verification method, or more precisely, the ConCert framework for testing and verifying smart contracts.

What is formal verification?

Formal verification is a mathematical method of proving that a program model satisfies a given specification (or formal description). There are several main ways to construct formal proofs that a program model does or doesn't match its specification, including model checking and the deductive method using interactive or automatic theorem provers. 

The main advantage of the deductive verification method over model checking is that the programming languages used have a fairly limited set of operators. They only allow to model a small subset of the language in which the source code is written. Also, in some cases, a program model can be translated into the language of a theorem proving environment by special formally verified software.

Today, formal verification of smart contracts is relevant because the current methods of auditing and testing smart contracts can detect errors, but not guarantee their absence. Only formal methods can help prove the correctness of a program in a strictly mathematical way.

Interactive proof environments

Deductive verification of software is usually performed in automated or interactive theorem proving environments, or proof assistants. In automatic proof environments (Why3, PVS, Z3), proofs (or counterexamples) are generated automatically using SAT and SMT solvers, and the user doesn't take part in the deduction directly. The main issue with this method is the limited class of statements that can be proven automatically. Also, if an automatic proof fails, it's often hard to figure out what went wrong and whether the property is provable at all.

As for interactive proofs in proof assistants (the most popular of which include Coq, Lean, Isabelle, and the HOL family), they're generated through human-computer interaction (often in an IDE). Interactive proof environments differ from each other in the language they use (usually functional), degree of automation, and the use or absence of dependent types.

Coq

The framework I'm discussing here is implemented in Coq, an interactive theorem proving environment using Gallina, which is a dependently typed functional programming language used to express both programs and their properties. Proof automation is also possible in Coq through tactics and metaprogramming using MetaCoq. Coq has been successfully used in various projects in the industry, including to:

• Check JavaCard security. 

• Create a formally verified CompCert compiler for C.

• Prove the four-color theorem and Feit–Thompson theorem.

• Verify smart contracts in the Pruvendo and Formal Land projects (ConCert is used for the latter as well).

The ConCert framework

Architecture

The framework includes the entirety of the smart contract execution environment model in Coq and the tools for modeling and testing smart contracts and code generation. ConCert supports two methods for developing secure smart contracts: you can either model the smart contract based on the source code in ConCert, or extract the verified smart contract code from Coq.

First, the smart contract functions are written in Gallina. These are common functions that use predefined blockchain primitives provided by the ConCert framework. Then the specification is written and the contract functions are tested semi-automatically thanks to the integration of QuickChick. The framework also allows the proving of smart contract properties using the ConCert infrastructure. Proofs use a model of the execution environment to reason about how contracts interact with each other. This allows proving properties beyond the simple correctness of a single contract function.

Figure 1. ConCert architecture

After testing and verification, code can be extracted to obtain an executable implementation in any supported smart contract language. This is accomplished by MetaCoq erasure procedures with verified optimizations and preprocessing in ConCert, which provides a code generation procedure with a strong guarantee of correctness.

A few installation tips

ConCert is developed in Coq 8.17 and depends on MetaCoq and std++. To work with tests, the QuickChick library is required. All dependencies can be installed with opam, the OCaml package manager:

sudo apt install opam
opam switch create . 4.10.2 --repositories
default,coq-released=https://coq.inria.fr/opam/released
eval $(opam env)

Installing ConCert and its dependencies:

git clone https://github.com/AU-COBRA/ConCert.git
cd ConCert
opam install ./coq-concert.opam

Building examples from the repository:

git clone https://github.com/AU-COBRA/ConCert.git
cd ConCert
opam install ./coq-concert.opam --with-test

Smart contract model and execution environment

The smart contract execution environment model facilitates reasoning about the results of executing a sequence of smart contract calls (traces). The smart contract itself is represented in the model as a pair of functions: init and receive.

init : Chain -> ContractCallContext -> Setup -> option State

The init function is used when deploying a contract to set its initial state. The first Chain type parameter transmits blockchain data: the number of blocks and mapping from addresses to their balances. The ContractCallContext parameter transmits data about the current call: the addresses of the caller and called party and the amount sent to the contract. Setup includes the initialization parameters.

receive : Chain -> ContractCallContext -> State -> option Msg -> option (State ∗ list ActionBody)

The receive function is used to implement user calls and executed every time the contract is accessed. State is the current state of the contract. Msg is the user-defined type of message that the contract accepts (its entry points). The result of successful execution is a new state and list of actions represented by the ActionBody type. Actions can fund transfers, calls to other contracts, and contract deployments.

The Chain type doesn't contain enough information to model the execution of actions on the blockchain. We need to be able to see information about currently deployed contracts, or more specifically, their functions and states. That's where the Environment type comes into play, which describes the state of the environment as a whole:

Record Environment :=
    { env_chain :> Chain;
      env_contracts : Address -> option WeakContract;
      env_contract_states : Address -> option SerializedValue; }.

The state of the environment changes as a result of transactions, which are defined in ConCert with the Action type:

Record Action := { act_from : Address; act_body : ActionBody; }.

When receive returns a new list of actions, the execution environment needs to evaluate their result. This evaluation is made using the ActionEvaluation relation in Coq with Environment -> Action-> Environment -> list Action -> Type. It contains the requirements for executing a transaction in the environment and its consequences.

receive and init are functions in Coq, which makes them convenient for verification. However, simply reasoning about the functions of a specific contract is often not enough, as many deployed contracts involve interactions with other contracts. Calling the receive function once can potentially result in multiple calls, creating complex call graphs between deployed contracts. Therefore, the sequence of execution calls must be taken into consideration. The ChainTrace execution trace is a reflexive transitive closure of the ChainStep relation that essentially reflects the addition of a block to the blockchain and has the ChainState -> ChainState -> Type type in ConCert where: 

Record ChainState := { chain_state_env :> Environment;
                       chain_state_queue : list Action; }

Property-based testing

Property-based testing is a technique where data is generated pseudo-randomly and checked against a certain property. The PBT QuickChick library is integrated in ConCert, which supports testing the functional correctness of contracts and the properties of execution traces. The testing framework is shown in Figure 2.

Figure 2. PBT ConCert diagram

In short, here's how the PBT framework works. The user writes message generators (functions that create pseudorandom values ​​of a given type) for the contracts being tested. Then the generators are used to create random execution traces with pseudorandom contract calls. The user also sets up the initial blockchain configuration consisting of address balances and deployed contracts. 

Here's an example of a token smart contract with a type of possible messages:

Inductive Msg :=
    transfer of (address * address * nat)
  | approve of (address * address * nat).

It has two entry points: one for transferring tokens between two given addresses, and one for approving an address to spend a given amount of tokens on behalf of another address. Then the generation of pseudo-random Msg values results in the generation of transfer or approve and their parameters using the generators for address and nat. 

For example, we want to check that "transfer" correctly updates internal balances. In ConCert, this functional correctness property is specified using pre- and postconditions. Testing this property using QuickChick could look like this:

QuickChick ({{msg_is_transfer}} Token.receive {{transfer_correct}}).

This is the test code we use to check if the incoming message is "transfer," then after executing the "receive" function of the token smart contract its state should match the transfer_correct predicate we wrote manually. By default, QuickChick will generate 10,000 tests and check that the property is satisfied in all of them or report a counterexample. The resulting counterexamples are automatically minimized by the PBT framework to make them easier to understand. Developers claim that these tests typically take less than a minute.

Application example for iToken

ConCert developers have already shown a good amount of successful use cases of the framework for testing and verifying smart contracts. For example, ConCert was used to find new vulnerabilities in a Basic Authentification Token smart contract, a DAO Attack was formalized, and the Dexter exchange contract was modeled on the Tezos blockchain, an early version of which also had a vulnerability.

Now let's check out an example of a vulnerability in the Solidity contract of the iToken token used on the bZx platform. Due to misplaced lines of code, an attacker managed to steal $8 million in September 2020.

Here's the code with the vulnerability:

Figure 3. Vulnerable code

The smart contract logic would be correct if line 6 was moved after line 8. But what if _from = _to? In this case, the transferred amount will be deducted from the sender's balance in line 8. However, in line 9, the sender's original balance is used to add the transferred amount to the sender's balance, resulting in the sender sending all the tokens to themselves.

This vulnerability was also found using ConCert. Below is what the function looks like in the framework.

Figure 4. Implementation of the bugged iToken _internalTransferFrom function

This bug can be found using the PBT framework by writing a test that checks if the balance remains unchanged after a self-transfer. However, this specification assumes that we know about the potential of an error. Instead, we can formulate a more general property that the sum of all balances must remain unchanged after a call, except for the mint and burn function calls. In ConCert, this property looks as follows:

Figure 5. Predicate on the invariance of balance totals of iToken users

QuickChick ({{msg_is_not_mint_or_burn}} iTokenContract {{sum_balances_unchanged}})

Running this test will result in a counterexample where the property is not executed:

Figure 6. Test results. The property is violated when calling transferFrom with identical _from and _to parameters

Modeling the AMM/DEX smart contract and verifying function properties

We experimented with using ConCert to model and verify an automated market maker smart contract during a Russian hackathon in 2023 (project front available here).

The smart contract is written in Solidity. Users can create liquidity pools, add tokens to them, earn commissions on deposited assets, and withdraw earnings. A fee is charged for using the protocol. 

The contract has five entry points: pool creation, depositing funds to the pool, withdrawing funds from the pool, withdrawing commissions, and swapping:

 Inductive Msg :=
  | createPair : Address -> Address -> N -> bool -> Msg
  | deposit : N -> N -> N -> Msg
  | withdrawFees : N -> Msg 
  | withdraw : N -> Msg
  | swap : N -> Address -> Msg

The following is the source code of the createPair function. Any network participant can create a pool if the pair isn't already represented on the DEX.

function createPair(address token0, address token1, uint _fee, bool _isStable) external returns (uint) {
        require(token0 != token1, "two identical addresses");
        require(token0 != address(0), "Zero Address tokenA");
        require(token1 != address(0), "Zero Address tokenB");
        require(getPool[token0][token1][_fee][_isStable] == 0, "Pair already exists");

        PIDs++;
        uint PID = PIDs;

        Pools[PID].token0 = token0;
        Pools[PID].token1 = token1;
        Pools[PID].feeRate = _fee;
        Pools[PID].isStable = _isStable;

        getPool[token0][token1][_fee][_isStable] = PIDs;
        getPool[token1][token0][_fee][_isStable] = PIDs;

        return PID;
    }

Here's how this function is formalized in ConCert:

Figure 7. Implementation of the createPair function in the sberAMM smart contract

We already covered testing smart contracts in ConCert using PBT, so now we'll transition to proving theorems about the correctness of smart contracts.

In general, three theorems can be proven for a smart contract function: that the state variables are updated correctly, that the sequence of generated transactions is correct, and that the function will be executed successfully if and only if it's called with the correct parameters.

For example, let's consider proving the first theorem for createPair. First you need to define a correctness predicate for the function, or a predicate signaling that its state variables were updated correctly. Then formulate the theorem: if for any parameters and initial and final states the createPair function was called and executed successfully, then the variables will be updated correctly. Coq tactics are used to prove it (this topic can be a whole separate article, but here all I'll note is that you can use internal tactics and others you write yourself).

Figure 8. Correctness predicate and theorem about createPair

As I noted above, ConCert lets you prove theorems for individual functions and sequences of transactions. For example, for this smart contract I could prove that the user will always be able to withdraw the funds they deposited. However, when proving the correctness of the swap function, there was an issue involving overflow in the original contract.

function swap(uint PID, address tokenIn, uint amount) external pidExists(PID) PIDstatus(PID) returns (uint) {
        require(tokenIn == Pools[PID].token0 || tokenIn == Pools[PID].token1, "Wrong token address");
        require(IERC20(tokenIn).transferFrom(msg.sender, address(this), amount));

        address tokenOut = _getOtherTokenAddr(PID, tokenIn);
        uint fee = (ud(Pools[PID].feeRate) * ud(amount)).unwrap();
        uint amountMinusFee = amount - fee;
        uint amountOut = _calculateAmounts(PID, tokenIn, amountMinusFee);

        _handleFees(PID, tokenIn, fee);
        IERC20(tokenOut).safeTransfer(msg.sender, uint(amountOut));

        return uint(amountOut);
    }

The error is that in the createPair function, there's no check for feeRate variable limits. This variable stores the value (as a percent based on the contract logic) of the swap fee. So in the seventh line of the swap function, the amountMinusFee variable value of the uint type equal to amount – fee can be negative. This smart contract uses Solidity version 0.8.19, which means that revert will happen if there's overflow and the swap transaction will not be executed. The swap function doesn't contain a vulnerability, but not checking the value of the _fee variable in createPair function may result in malicious users setting an arbitrary fee for swapping a pair without other users being able to create a new pool with it.

As I already noted, this vulnerability was discovered during a check of the correctness of the swap function where Coq tactics couldn't resolve equality with a positive amountMinusFee variable because it ceased to be positive in general.

Conclusion

While ConCert can't verify the correctness of a smart contract's source code written in Solidity directly, we've found it well suited for testing and formally proving the correctness of a contract's logic. However, other tools can also do the same, even Coq has several other projects for the formal verification of smart contracts. Beyond Coq, there are also projects like Certora (the focus of my colleague Sergey), Isabelle/Solidity, Solidity SMTChecker, and KEVM.

Our goal isn't just to follow the trends, but to be part of the development of blockchain technologies. Despite the resources this method requires, we believe that as current tools improve and new ones are created, formal methods will play a key role in the blockchain industry. 

Our company researches and applies the formal verification of smart contracts and blockchain applications, so we know how important and effective they can be. We also research and implement other tools and techniques to improve the quality and security of our own programs, including the latest developments in formal verification and time-tested methods of static analysis, testing, and fuzzing. 

Questions? Feedback? Email us at: [e-mail].