Introduction

In this blog, we'll explore how Certora leverages formal verification to protect Uniswap v4 from malicious hooks. We'll also explore how Certora's unique tool, Certora Prover, can precisely define and prove correctness rules, ensuring robust security for smart contracts.

We established the Uniswap v4 threat model in previous blog posts, detailing vulnerabilities around malicious hooks, insolvency risks, and various potential attack vectors. We also covered bugs identified by other audit firms, highlighting how Certora’s security approach addresses those challenges.

Let's explore how formal verification with the Certora Prover strengthens Uniswap v4’s defenses, providing comprehensive protection against hidden threats.

Jumpstarting Formal Verification from Fuzzing

One of the biggest challenges in fuzzing and formal verification is considering the code's security-assuring properties. Fortunately, when the Certora audit began, the Uniswap team had already developed numerous tests using Foundry.

One particular test, named test_fuzz_swap_beforeSwap_returnsDeltaSpecified, included an assertion that checked whether the amount received during the swap matched the amount specified. This test successfully passed during the fuzz testing.

Then, when our team ran the Certora Prover on this test, the assertion was violated according to the corresponding CVL rule.

The violation occurred because the router might have had a native token balance before executing the test. As a result, it sent the entire balance to the swap receiver. This means the user would receive the proceeds from the swap and any preexisting funds in the router.

Fuzzing tools could not have found this case, regardless of how long the buzzer ran. The problem stems from the test's setup, specifically its initial conditions. Fortunately, CVL and the Certora Prover do not start from a specific starting state, so they can consider situations where the router contract has a non-zero native balance and provide a counter-example.

This test case is somewhat artificial, and the violation found does not indicate a bug in the code but rather an imprecision in the test. The Certora Prover started from a more generalized precondition than the fuzzer.

Nevertheless, if we disregard that case, the Prover verified the test in its CVL form. The benefit is twofold: The test was refined to account for any initial state and was also proven to work with any test input. In contrast, a fuzzer only covers a limited range of possible inputs.

Beyond Solidity: Showing Interesting Properties of Uniswap v4 Protocols

Users can concisely use the Certora Verification Language (CVL) to express rules, which are robust and comprehensive tests for smart contracts. Although the rules may be brief, their security benefits are substantial. One of the advantages of using CVL is that its syntax closely resembles that of Solidity or Forge tests. You can write tests in CVL instead of Solidity while leveraging the capabilities of the Certora Prover for formal verification.

We will show an example of a rule we proved and how it can provide assurance against one of our concerns: the potential exploitation of a malicious hook.

We previously described how malicious hooks could manipulate accounting in their favor, misleading the Pool Manager into believing it owes the user (or the hook contract) more than the expected value. Suppose the standard hook-free accounting reflects the original Uniswap v3 logic, based on the piecewise constant product pool. In that case, we require that the total accounting for both the hook and the user is equivalent to the default accounting for any logic the hook introduces. In other words, the hook must not create "extra" balances for itself or the user.

The hook can apply an arbitrary balance change to both itself and the user. Due to its arbitrary nature, the rule also takes into account the default hook, which applies no balance change when it lacks permission.

In this rule, we call the swap() function from the Pool Manager twice, using the same initial state (represented by initState in the rule's body, which reflects the storage state of all contracts involved in this test). The two scenarios differ only in the arbitrary hook data bytes argument we provide to the swap function.

Unlike standard variable declarations in other programming languages or fuzzing programs, where values are typically initialized or randomized, CVL behaves differently. In CVL, all declared variables (unless explicitly assigned a value during their declaration) are entirely arbitrary. This means they can take on any value of their type, subject to the constraints specified by the user through require statements.

However, something is missing here. We haven't defined the hook contract or how it calculates the balance delta based on the input we provided. The good news is that we don't need to specify these details. CVL offers a unique feature that allows us to replace contract invocations and return values with non-deterministic behavior. In CVL terminology, replacing a function call with an unspecified value is known as summarization. We utilized this technique extensively while verifying Uniswap v4. The more general a summarization is, the more broadly applicable the proof of a rule becomes, thereby enhancing the assurance of its correctness.

Regardless of the hook's functionality in practice, we replace its return data with arbitrary values that may vary between different invocations. The two parallel scenarios below may appear equivalent, but they behave differently behind the scenes due to the hook's random behavior. Although the hook deltas differ, the shared state of both invocations remains consistent, including the pool key, contract state, and virtual balances.

The rule flow is as follows:

1. Call swap() from the initial state with arbitrary function arguments.
2. Fetch the currency deltas for the pool hook address and the msg.sender after swapping both pool tokens.
3. Call swap() again from the original initial state, using different hook arguments, as if the first swap() had not been invoked.
4. Fetch the currency deltas for this second scenario.
5. Assert that the sum of the currency deltas for the hook address and the msg.sender is the same for both pool tokens in both scenarios.

Rule: 
The sum of currency deltas is independent of the hook's behavior given the same initial state.

rule swap_hook_sender_deltas_sum_is_preserved() {
    /// Environments (env) are internal structs that include the blockhain and transacation context.
    env eA;
    env eB;
    /// The msg.sender is the same in both cases.
    require eA.msg.sender == eB.msg.sender;

    /// Declare swap arguments (generic)
    PoolManager.PoolKey key;
    IPoolManager.SwapParams params;
    address hookAddress = key.hooks;
    PoolManager.PoolId poolId = PoolGetters.toId(key);

    bytes hooksA;   /// Hook data for scenario A.
    bytes hooksB;   /// Hook data for scenario B.

    /// This is a storage "checkpoint", that could be reverted to anytime.
    storage initState = lastStorage;

   /// It's necessary to neutralize the before_swap hook so it won't change the
   /// swapped amount.
   require !CVLHasPermission(hookAddress, BEFORE_SWAP_RETURNS_DELTA_FLAG());
    
    swap(eA, key, params, hooksA) at initState;

    /// Fetching the virtual balance state for scenario A, post-swap.
    int256 deltaSender0_A = PoolGetters.currencyDelta(e1.msg.sender, key.currency0);
    int256 deltaSender1_A = PoolGetters.currencyDelta(e1.msg.sender, key.currency1);
    int256 deltaHook0_A = PoolGetters.currencyDelta(hookAddress, key.currency0);
    int256 deltaHook1_A = PoolGetters.currencyDelta(hookAddress, key.currency1);

    /// Calling swap in scenario B, from the initial state of the rule.
    swap(eB, key, params, hooksB) at initState;

    // Fetching the virtual balance state for scenario B, post-swap.
    int256 deltaSender0_B = PoolGetters.currencyDelta(e1.msg.sender, key.currency0);
    int256 deltaSender1_B = PoolGetters.currencyDelta(e1.msg.sender, key.currency1);
    int256 deltaHook0_B = PoolGetters.currencyDelta(hookAddress, key.currency0);
    int256 deltaHook1_B = PoolGetters.currencyDelta(hookAddress, key.currency1);

    /// Assert that the sums of currency deltas for the two scenarios are equal, for both tokens.
    assert 
        deltaSender0_B + deltaHook0_B == deltaSender0_A + deltaHook0_A
        &&
        deltaSender1_B + deltaHook1_B == deltaSender1_A + deltaHook1_A;
}

The Certora Prover successfully proved this rule with SMT solvers. What are the implications of this verification?

Regardless of the data returned by the hook during the swap operation, it is guaranteed that the sum of currency deltas of both the hook address and the user (msg.sender) is preserved and remains equal to the delta in the default case (the naive hook), which is based on the standard Uniswap v3 logic. Therefore, if we trust that the deltas attributed to the user are accurate, we can confidently say that no hook can produce deltas that deviate from the correct values.

A meticulous reader might argue that this rule alone is insufficient to ensure security against malicious hooks. For instance, we haven't considered the virtual balances of other users for different tokens. This observation is valid, and we have an additional rule in place that ensures the swap() function only alters the balances of the msg.sender and the hook, specifically for the two tokens involved in the pool.

The main point is that sometimes a single rule alone cannot completely eliminate potential attack vectors. It is crucial to understand the set of assumptions and assertions that contribute to a valid proof.

Conclusion

In this blog, we highlighted the benefits of using formal verification to enhance the coverage of fuzz testing and demonstrated its ability to identify non-trivial edge cases. We also illustrated how to implement a rule in CVL to detect the improper behavior of a generic hook. Our efforts successfully proved a crucial property that holds true regardless of the hook's implementation. This underscores the significant potential of formal verification in securing smart contracts and ensuring the solvency of funds in lending protocols or decentralized exchanges (DEXs) such as Uniswap.

We will soon publish a comprehensive set of CVL rules for the v4-core in an external Git repository, detailing essential properties concerning the correct handling of funds within the Pool Manager.