Formal Verification (FV) for smart contracts has never realized its potential adoption due to three prevalent misconceptions:

1. It is hard to use
2. It is only viable on trivial systems
3. It cannot be used as a security tool

We show how our specification language, CVL, breaks those myths.

The main tool implemented by Certora is the Certora Prover. The tool uses formal verification to prove properties on smart contracts written in Solidity.

Formal verification is the process of mathematically checking that the behavior of a program adheres to its specifications. It is one of the recommended techniques for improving smart contracts' security. A more detailed explanation of the theory behind formal verification can be found in our white-paper.

This all sounds great, so why isn’t everyone writing or auditing smart contracts using formal verification?

This may be partly due to some persistent myths about formal technology that make it seem too difficult to implement or not effective enough. This article examines these myths and explains why they should not be cause for concern.

Myth number 1 — You need a Ph.D. to use Formal Verification

There is a prevalent misconception that writing formal specifications is difficult due to the math and logic involved.

Writing in our specification language Certora Verification Language (CVL) can be as easy as writing unit tests.

Let’s start with an example:

contract ERC20 is IERC20, IERC20Metadata {
  function transferFrom(address sender, address recipient, uint256 amount)
    public virtual override returns (bool) {
    …  
  }
  {…}
}

One of the properties that we may be interested in checking is the integrity of transfer. This means that the transferFrom function does not affect the sum of the balance of the sender and the recipient.

This is how the rule looks when writing this property in CVL:

rule integrityOfTransfer(address sender, address recipient, uint256 amount) {
  env e;
  uint256 balanceSender = balanceOf(e, sender);
  uint256 balanceReceiver = balanceOf(e, receiver);
  transferFrom(sender, receiver, amount);
  assert balanceSender + balanceReceiver == balanceOf(e, sender) + balanceOf(e, receiver);
 }

a). Initialize the env e which represents the Solidity global variables related to the environment, such as the msg.sender (see the documentation).
b). Sample the balance of the sender and of the recipient of the transfer.
c). Assert that the sum was not affected by the transferFrom function.

The Certora Prover will use formal verification to test the rule on all valid inputs and starting states. In our case, this means:

1. All possible initial storage states will be checked.
2. All the valid addresses for the sender and recipient will be checked.
3. Any transfer amount will be checked.

As seen here, the rule looks just like a simple unit test. However, it still contains the exhaustiveness of FV which may be critical when verifying the correctness of smart contract code.

Myth number 2 — Formal Verification Can’t Prove Fundamental Invariants

The example above could be considered simple and perhaps not enough to convince you about the power of using CVL on real code and with more complicated properties.

One of the findings describing the usability and need for using formal verification tools was made in May 2022 by the Formal Verification team of Maker. Using the Certora Prover, they discovered an issue in their protocol. This issue was live since their first launch in November 2019 (more details here).

The Multi-Collateral DAI (MCD) is the stable coin implemented by Maker. One of the most crucial properties of the protocol is an invariant called the “Fundamental Equation of DAI”. This invariant ensures the DAI balances are always backed by debt. This invariant can be expressed by the equation:

The Fundamental Equation of DAI

The Maker team implemented this invariant in their specification written in CVL. They surprisingly discovered that it did not always hold on the code deployed for almost three years. Fortunately, this bug was not exploitable and no funds were at risk. Still, this exemplifies why FV tools should be used to ensure that important protocols’ properties hold for all possible inputs and states.

Myth number 3 — Formal Verification Cannot Find Sophisticated Vulnerabilities

Though we have only talked about Certora FV tools to check for properties that are specific to the protocol being checked, this is not enough. A good security review must also check smart contracts' code for common but dangerous vulnerabilities.

A novel vulnerability presented by the ChainSecurity team one year ago is the Read Only Reentrancy. This vulnerability was discovered initially on the Curve protocol. It was then found on several other contracts and it’s estimated that more than $100 million was at risk due to this attack vector.

Diagram of the Real Only Reentrancy attack

This vulnerability allows potential attackers to expose dirty states of a vulnerable contract to a third party exploited contract. This possibility exists as view functions usually lack reentrancy guards as they are not state-altering.

A property that checks this vulnerability would be:

“Every time an external function is called, all the view functions return a valid state.”

In this case, a valid state is the function's initial state or the function's final state.

Writing this rule in CVL is straightforward as it is presented in this code snippet.

ghost bool no_ro_reentrancy;

rule no_read_only_reentrancy(method f) 
{
  env e;
  env e_external;
  calldataarg data;
  require no_ro_reentrancy;
  require before_func1 == view_func_caller(e_external);
  f(e, data);
  require after_func1 == view_func_caller(e_external);
  assert no_ro_reentrancy, "Found a read-only reentrancy vulnerability";
}

Here, we use a parametric rule to run our rule on any external method f of our contract and use a wrapper function view_func in the Solidity original code to call any view function.

We checked this property on the Curve protocol and it not only found the specific vulnerable lines but also the specific view functions which return an inconsistent state. The exhaustiveness of FV, together with its precision surely make it an indispensable tool when speaking about code security.

Conclusion

In this article, we presented three examples showing how our language CVL is accessible and intuitive, while still being expressive enough to check very interesting properties and vulnerabilities.

Many more examples are publicly available in our examples repo.