Progress report on the verification of Liquidity Baking smart contracts

Context

Liquidity baking is one of the main features of the Granada proposal. The feature itself has been well explained by others (initial proposal on Agora, TZIP, Presentation by Midl-dev, Presentation by XTZ.news) so we won’t present it here in details.

An original aspect of this feature is that it depends on a smart contract that will likely hold a very high balance. For this reason, the security of this smart contract is extremely important and we have devoted a lot of efforts into checking that the contract is safe.

We have used formal verification to prove that the compiled Michelson code for the CPMM contract is valid with respect to functional specification. As was shown in the past, this approach increases our confidence in the correctness of the implementation, but says little about the properties of its specification. In particular, the specification of Dexter was flawed. To avoid similar pitfall, we also have proven higher-level, security properties for the CPMM contract, and we have subjected the overall Liquidity Baking feature to thorough testing.

Overview: smart contracts involved in Liquidity Baking

Three smart contracts are involved in the Liquidity Baking feature: a Constant Product Market Maker (CPMM for short), one FA1.2 contract managing a pool of tzBTC, and another FA1.2 contract managing liquidity tokens.

The main contract is the CPMM; a kind of contract deeply inspired by Ethereum’s Uniswap decentralized exchange. Two kinds of users interact with this contract.

The first kind of users are called traders; they can use the contract to trade tez for a particular FA1.2 token called tzBTC (using the xtzToToken entrypoint) and vice versa they can trade tzBTC tokens for tez (using the tokenToXtz entrypoint). Traders can also use the CPMM to trade tzBTC tokens for other FA1.2 tokens (using the tokenToToken entrypoint).

In order to perform the trade without waiting for another trader wanting to do the symmetric trade, the CPMM contract holds both tez and tzBTC tokens that are provided by the second kind of users, called liquidity providers. By maintaining in its storage the number of tokens available, the CPMM is able to compute an exchange rate for the current trade (independently from the other trades).

Liquidity providers deposit tez and tzBTC tokens simultaneously in a so-called liquidity pool (using the addLiquidity entrypoint). The share of the liquidity pool that each liquidity provider owns is materialized using a FA1.2 token contract (called the liquidity token contract) administered by the CPMM. Each time addLiquidity is called new liquidity token are minted and credited to the liquidity provider that called it. Liquidity providers can also withdraw an amount of tez and tzBTC token by burning their liquidity tokens (using the removeLiquidity entrypoint).

Finally, anyone can make a donation in tez to the CPMM contract (using the default entrypoint). This donation goes to the tez part of the liquidity pool but no liquidity token is minted for it so users have no reason to call this entrypoint; the sent tez are effectively shared between the liquidity providers. The default entrypoint is used by the Tezos protocol to send the liquidity baking subsidy (2.5 freshly minted tez) to the contract in each block.

This subsidy is meant to incentivize liquidity providers. To further incentivize them, for each trade, a 0.1% fee of the traded amount is also sent to the liquidity pool.

Verified properties

For each property, we will explain the potential risk if it did not hold, we give an informal description of the checked property, we show the verification technique used to check that this property holds, and we provide pointers to online resources for more details.

Notations

• \(L\) : number of liquidity tokens accounted in the CPMM storage.
• \(X\) : number of xtz tokens accounted in the CPMM storage.
• \(T\) : number of tzBTC tokens accounted in the CPMM storage.
• \(\gamma\) is equal to 1 minus the fee (a constant equal to \(0.999\) in the CPMM).

We write \(L'\), \(X'\), and \(T'\) for these values after the execution of the entrypoint under focus.

\(X\) and \(T\) are called the supplies of the CPMM and their product \(X \cdot T\) is called the product of supplies.

Verification tools

Our main verification tool is the Mi-Cho-Coq library that allows to verify Michelson programs with the Coq proof assistant. Coq is a very expressive system in which essentially any mathematical theorem can be stated and proved. However, Mi-Cho-Coq has some limitations, the most important one in the context of this work is that it cannot currently be used to prove properties about contract interactions.

In that situation, to get more confidence in the validity of properties where Mi-Cho-Coq cannot be used to get a mechanically verified mathematical proof, we use a testing framework based on property-based random testing named QCheck. We have extended the test framework which has been developed to test Tezos protocols in two directions: (1) execute arbitrary sequences of Liquidity Baking contract calls on top of arbitrary contexts, and (2) simulate the execution of these contracts.

Both calling the real contracts and simulating them have benefits. Executing the real contracts improves our confidence in the tests results, but has proven to be time-expensive. Simulating the execution addresses this limitation and allows to execute many more test cases, but the results obtained with this approach are only valid if the simulation is trustworthy.

To get the best of both worlds, we have validated our simulation against the contracts implementation, by executing the same sequences of contracts calls using both approaches. During this process, we check after each baked blocks if the simulation state is an abstraction of the blockchain context. In the process, we have both ironed out bugs from our simulation and improved our confidence in the contract implementation.

Correctness of compilation

The CPMM and the FA1.2 liquidity token contract have been developed using the LIGO language and compiled to Michelson scripts. Compilers are complex programs and bugs inside them are commonly found.

Property

The semantics of the Michelson scripts matches the semantics of the source LIGO scripts.

Risk

Most compiler bugs are benign but in the worst case a bug in the LIGO compiler could introduce a security risk if the semantics of the LIGO scripts was not preserved through compilation.

Verification technique

Using the Mi-Cho-Coq framework and the Coq proof assistant, we formally prove that the Michelson scripts are semantically equivalent to a high-level specification arguably equivalent to the source LIGO scripts. During this verification work, no bug in the LIGO compiler was found.

Resources:

• Coq statements
• Coq proof repository

Safety of execution

All the entrypoints of the CPMM, except default, involve divisions. We make sure that the script never divides by zero. As a matter of fact, the contracts divide by the number of tokens of the pools (the pool depending on the entrypoint in question).

Property

\(L\), \(X\), and \(T\) should always be strictly positive. This is an obvious consequence of the following property:

In plain english: the square of the total number of liquidity tokens is always positive and the product of xtz tokens and FA1.2 tokens is always greater or equal to this value.

Risk

If \(L\), \(X\), or \(T\) ever reaches zero, some entrypoints of the CPMM cannot be called anymore so the functionality they provide is lost. In particular, some funds would be frozen and the subsidy would also be minted for nothing.

Verification technique

Using the Mi-Cho-Coq framework and the Coq proof assistant, we formally prove that all the entrypoints preserve this relationship between \(L\), \(X\), and \(T\) and that this property is sufficient to show that the token pool never reaches 0 (hence, the contract never divides by zero and never gets stuck).

The case for removeLiquidity is interesting because it can lead to \(L = 0\) in the edge case of all liquidity providers choosing to remove all their liquidities. To guarantee that this case never happens, a tiny initial liquidity deposit is done with the null address so that it can never be removed in the future. This external assumption has been taken into account in the formal proof.

Resources:

• Coq statements
• Coq proof repository

Evolution of the product of supplies

Despite its name, the CPMM does not preserve a constant product of supplies. Indeed, the default entrypoint is increasing \(X\) with no change to \(T\). The fees and the rounding in division also prevent the product of supplies to be constant.

As a matter of fact, the product of supplies generally increases. This is true for allthe entrypoints, except, of course, for removeLiquidity that decreases both \(X\) and \(T\).

In order to take the removeLiquidity case into account, we need to track not only \(X\) and \(T\) but also \(L\). The correct invariant is a property named “Ratio between Product and Squared Liquidity Increases” and it holds for all entrypoints:

This property is important because it guarantees that there is an incentive for providing liquidity: whatever the users of the contract do, liquidity providers are guaranteed that the amount of tez and tzBTC tokens that they will be able to withdraw in the future always have a greater product than what they originally deposited.

Property

• addLiquidity of \(A\) tez increases the product of supplies as follows:

  $$ X' \cdot T' = (X + A) \cdot (T + {\left\lceil {{T \cdot A} \over X} \right\rceil}) \ge X \cdot T $$
  and \(L' = L + { { L \cdot A } \over X }\).

• removeLiquidity of \(A\) liquidity tokens decreases the product of supplies as follows:

  $$ X' \cdot T' = (X - { { X \cdot A } \over L}) \cdot (T - { { T \cdot A } \over L}) \le X \cdot T $$
  and \(L' = L - A\).

• xtzToToken of \(A\) tez increases the product of supplies as follows:

  $$ X' \cdot T' = (X + A \cdot \gamma) \cdot (T - {{ \gamma \cdot A \cdot T } \over {X + \gamma \cdot A}}) \ge X \cdot T $$
  and \(L' = L\).

• tokenToXtz of \(A\) tzBTC tokens increases the product of supplies as follows:

  $$ X' \cdot T' = (X - { { A \cdot \gamma \cdot X } \over { T + A \cdot \gamma } }) \cdot (T + A) \ge X \cdot T $$
  and \(L' = L\).

• tokenToToken of \(A\) tzBTC tokens increases the product of supplies as follows:

  $$ X' \cdot T' = (X - { { A \cdot \gamma \cdot X } \over { T + A \cdot \gamma } }) \cdot (T + A) \ge X \cdot T $$
  and \(L' = L\).

• default of \(A\) tez increases the product of supplies as follows:

  $$ X' \cdot T' = (X + A) \cdot T \ge X \cdot T $$
  and \(L' = L\).

Risk

A strict decrease in the product of supplies means that value is taken out of the liquidity pool. The only case where such a decrease is expected is the removeLiquidity entrypoint. A decrease in any other entrypoint means that an attacker has found a way to steal value from the liquidity pool.

Verification technique

Using the Mi-Cho-Coq framework and the Coq proof assistant, we formally prove that each entrypoint satisfies its corresponding property. We also formally proved that each property implies the property \(RPSLI\).

Resources:

• Coq statements
• Coq proof repository

Consistency between the contracts’ internal state

As explained in the overview, there are three contracts involved in Liquidity Baking: they must have a consistent image of the token distribution. The CPMM storage contains the CPMM’s view on both parts of its the liquidity pool (\(X\) and \(T\)) and also the total supply \(L\) of the liquidity token contract. The liquidity token contract also stores this value alongside the token balances of all the liquidity providers. The tzBTC contract stores the tzBTC balances of all tzBTC holders, in particular the CPMM.

Properties

• \(L\) should always be equal to the total supply of the liquidity token contract.
• \(X\) should always be equal to the tez balance of the CPMM contract,
• \(T\) should always be smaller or equal to the tzBTC balance of the CPMM in the tzBTC contract.

Remark that \(T\) could become strictly smaller than the tzBTC balance of the CPMM contract if a tzBTC holders were to directly call the tzBTC contract to transfer tokens to the CPMM (instead of calling the tokenToXtz or the addLiquidity entrypoint of the CPMM); in that case the CPMM contract can not reject the transfer or even discover that the transfer happened. Users have no reason to donate tzBTC tokens to the CPMM but when reasoning about the security of Liquidity Baking we need to consider this edge case.

Risk

An inconsistency between the states of the three contracts could lead the CPMM to incorrectly compute exchange rates and liquidity payback.

Verification technique

The test framework of the Tezos protocol has been extended to originate three contracts: the CPMM, the FA1.2 contract to deal with liquidity tokens, and another FA1.2 contract to act as a replacement for tzBTC (the latter being way more complicated to originate than the former).

We generate sequences of calls to the three contracts involved in Liquidity Baking, and apply the transactions on top an initial context provided by the test framework. After each baked block, we check that the contracts’ storage remain consistent with each other, i.e., (1) the tez balance stored in the ledger, (2) the storage of the FA1.2 contract, and (3) the storage of the tzBTC replacement contract.

Resources:

• The implementation of our property-based tests can be found in a dedicated branch in the Nomadic Labs repository of Tezos

No global gain

Assuming an attacker with an arbitrary balance of tez, tzBTC, and liquidity token, we do not expect the attacker to be able to gain value through its interactions with the CPMM contract alone. Each call to an entrypoint of the CPMM requires a payment in at least one of the assets but we could imagine, if a vulnerability was present in the CPMM code, that a sequence of calls resulted in the attacker increasing their holding in all three balances. This is what we call a global gain.

Property

For any sequence of calls from a fixed attacker to the CPMM, the global effect of the sequence of calls on the balances of the attacker in tez, tzBTC, and liquidity tokens is such that at least one of the balances decreases.

Note that we are assuming that the attacker is the only entity interacting with the contract. In fact, if we take the subsidy into account a global gain is possible by adding liquidities, waiting a few blocks (during which the subsidy is received by the CPMM and shared between the liquidity providers), and finally removing the liquidities. But this global gain coming from the subsidy is not an attack on the CPMM, it is the purpose of the Liquidity Baking subsidy!

Risk

Even a very small global gain is very dangerous for the security of the contract because an attacker able to exploit a global-gain vulnerability can likely exploit it many times in a row and the total loss for the contract can be dramatic.

Verification technique

We have looked for global-gain attacks using our property-based testing framework. More precisely, the test consists in generating 100 initial contexts, and for each of these contexts, generating and executing a sequence of 100 valid contracts calls performed by the same implicit account \(c\). Note that the execution is done with a subsidy equal to \(0\), because the objective of this test is to discover if an attacker can become richer by exploiting the CPMM, not by depositing funds against liquidity tokens. After each contract call, the balance of \(c\) is checked to assert that either one of its balances (xtz, tzBTC or lqt) has decreased, or they all remained constant.

QCheck has not being able to find a counter-example to this property.

Resources:

• The commit introducing the test

Trust base

Our verification and property-based testing efforts have mostly been directed to the liquidity token FA1.2 and CPMM scripts because these two scripts are new to the Tezos blockchain; the Granada protocol, if activated, will originate these scripts during the migration from Florence. The third contract involved, the tzBTC FA1.2 contract, is however already used onchain, it has been audited and it is has been traded on Tezos decentralized exchanges (Dexter and Quipuswap) for months.

The security of Liquidity Baking relies on the assumption that the bahavior of the tzBTC contract is consistent with the one of the FA1.2 contract that we have used as a replacement for it in our property-based testing context.

We also assume that Mi-Cho-Coq correctly defines the semantics of the Michelson language. If this was not the case, we could have missed compilation bugs.

Conclusion

Since the very beginning, we were aware Liquidity Baking is a sensitive feature, even more due to the mechanisms implemented to encourage traders to use it. This is why we have devoted a significant amount of effort to increase our confidence in its implementation. The formal verification effort of the CPMM contract includes key functional properties. The complete architecture (the three contracts, and the changes integrated to the Granada protocol) has been challenged with unit testing and property-based testing. Finally, the proposal comes with two halting mechanisms that further reduce the risk of a malicious actor taking advantage of the CPMM contract, and let the bakers be the final arbiters of Liquidity Baking’s fate.

Overall, we feel confident that all components of the Liquidity Baking features are sound and secure.

While the Granada election takes its course, we plan to continue our effort on asserting the economic properties of Liquidity Baking. The latter are reminiscent of game theory properties where actors aim to maximize their gains by responding to incentives in the contracts. We believe we now have a strong foundation for tackling this additional challenge.