# Formal verification of smart contracts in the ConCert framework

Medium
11 min
277

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.

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 opamopam switch create . 4.10.2 --repositories default,coq-released=https://coq.inria.fr/opam/releasedeval \$(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.

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 :=

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:

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.

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:

``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:

## 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(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:

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).

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");

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: web3@ptsecurity.com.

+5

## Information

Website
www.ptsecurity.com
Registered
Founded
2002
Employees
1,001–5,000 employees
Location
Россия