Kontrol and Term Finance: Formal Verification Success Story Working with Bounded Loops

Over the last 6 weeks, Runtime Verification and Term Finance have worked together to formally verify a series of properties that play a key role in the Term Finance’s Tokenized Strategy Protocol. We decided to highlight this engagement with a blog post, because we believe it’s a success story for Kontrol, a formal verification tool we have been developing since 2023. This specific portion of the protocol involves lists and loops, a thorn in the side for most formal methods tools. We welcomed the challenge and have been able to design proofs that identified crucial bugs missed by previous manual audits, and likely to have been missed by most Solidity formal verification tools available today. Let’s dive in 👇

Formal Verification Scope

Together with the Term team we decided that the engagement would consist of verifying the correctness of two implementations of linked lists in Solidity. More concretely, we aimed to verify that the insertion and removal algorithms of both implementations preserved desired properties.

The first linked list is the `RepoTokenList`, which is a list of `RepoToken` addresses. The second list is `TermAuctionList`, which is a list of offers for auctions. Both of these are deeply connected and crucial to the correctness of the entire protocol. After our initial design review, here is a list of properties we set out to prove:

• RepoTokenList

  1. Unique entries: there should be no duplicated `repoToken` addresses in the list
  2. Sorted: the list should be sorted by `repoToken` maturity
  3. Maturity Validity:  all repoTokens in the list should have a maturity timestamp greater than the current block timestamp.
  4. Balance Consistency: The Strategy's balance for each repoToken in the list should be greater than zero.

• TermAuctionList

  1. Unique entries: there should be no duplicated `offerIds` in the `TermAuctionList`.
  2. Sorted: the list should be sorted by offer auction address
  3. Auction Status consistency: there should be no offers in the list for completed or canceled auctions
  4. Offers consistency: all offers in the list have a positive balance and the offer amount stored in the list for each offer should match the amount locked in the corresponding TermAuctionOfferLocker contract
  5. Valid RepoTokens consistency: for any offer in the list its corresponding repoToken is valid according to the checks performed by the function validateRepoToken

After identifying the correctness properties, it was necessary to prove that the functions that change the state of the lists preserve these properties. Specifically,  it was essential to prove Insert Operation Correctness and Removal Operation Correctness for both lists.  Since these functions can change the state of the list, they can potentially lead to states where the properties are violated. Besides, it's crucial to prove that these functions implement their specification, i.e., they change the state according to the intended functionality.

Try Formal Verification with Kontrol for Yourself

Formal Verification is the only available technique to ensure that a desired property holds in every possible state, not only in one particular case but under all possible inputs and scenarios.

Kontrol is designed to integrate seamlessly with Solidity-based projects. The tool enables developers to write property-based tests in Solidity. We wrote tests for Term Finance that can be concretely executed or fuzzed with Foundry, but Kontrol can take them a step further and symbolically execute them, proving that the properties hold for any possible state and any possible input. 

Initialization process

The foundry `setUp` function allows to define a concrete initial state against which all the tests will run. Within this `setUp` function we call the Kontrol cheatcode `symbolicStorage` which makes all the storage for the test contract symbolic. This allows us to run the tests with the most arbitrary possible initial state, instead of a concrete initial state. After setting the storage to symbolic, we create a list of elements (repoTokens or offers respectively) with an arbitrary size. Given time constraints to finish the engagement we decided to perform bounded model checking. This means that there is a `bmc-depth` parameter that can be defined in the `kontrol.toml` file and the arbitrary lists will have sizes between 0, 1, …, `bmc-depth`. The proofs therefore offer a bounded verification guarantee, for lists of sizes up to and including bmc-depth.

All the tests follow a similar architecture. We assume the necessary pre-conditions, using the foundry cheatcode `vm.assume(condition)`, we call the respective function and then we assert that the desired properties are holding using the native `assert` statement. 

Insert Operation Correctness

To prove that the insert functions of both lists preserve the desired correctness properties, we defined two tests per list. In one test, we insert a new element into the list, i.e., an element that was not in the list before. In the second test, we try to insert an element that is already in the list. 

Following is the overview of both proofs.

• Insert a new element

  • Assume that all the invariants are holding before calling the insert function
  • Assume that the element to be inserted is not in the list
  • Assume the new element to be inserted does not violate the desired conditions:
    • In the case of RepoTokenList, the new repoToken to be inserted has not matured yet and has a positive balance
    • In the case of TermAcutionList, the new offer to be inserted is not for a completed or canceled auction, has a positive offer amount and its repoToken is valid
  • Call insert function with the new element as an argument
  • Assert that:
    • The newly inserted element is in the list
    • The size of the list increased by 1
    • All invariants are still holding
    • The original list is preserved: all elements in the list before the function call are still in the list after calling the insert function. 

• Insert a duplicated element

  • Assume that all the invariants are holding before calling the insert function
  • Assume that the element to be inserted is already in the list
  • Call insert function with the duplicated element as an argument
  • Assert that:
    • All invariants are still holding
    • The original list is preserved: all elements in the list before the function call are still in the list after calling the insert function and the size of the list didn’t change, therefore guaranteeing that the duplicated element was not inserted in the list

Removal Operation Correctness

The strategy to prove the correctness properties for the remove functions of both lists is slightly different. Notice that it might be the case that some properties don’t hold before the function call. For instance, in the `RepoTokenList`, we cannot assume that there are no matured tokens in the list or that all tokens in the list have a positive balance because the purpose of the `removeAndRedeemMaturedTokens` is to remove these tokens from the list. The same thing applies for invariants 3, 4, 5 and 6 from `TermAuctionListInvariants`. We will instead assert that these invariants hold after calling the `remove` function, ensuring that the `remove` function obeys its specification.

Findings

The specification of desired properties and their formal verification allowed us to identify issues that could potentially go unnoticed with traditional code review. In this section, we will cover the most important findings of this engagement. 

In the `RepoTokenList` insert function, we could identify a potential infinite loop if there are two tokens with the same maturity and we try to insert the second one again. This is a high-severity issue since it would compromise the functionality of the protocol. After having an infinite loop, any function requiring a traverse of the list would consume all the gas and revert in the end with an out-of-gas exception. Regarding the `TermAuctionList` insert function, one desired property states that there should be no offers in the list for completed or canceled auctions. However, there is no check that the new offer being inserted is not for a completed or canceled auction, therefore violating this property. 

Another important two findings of this engagement are related to the `TermAuctionList` remove function. The first one is that the removal operation correctness property was not holding. The specification for the `removeCompleted` function states that after the function is called, all offers in the list for completed or canceled auctions should be removed from the list. However, if the list has more than 3 elements and there are 2 sequential elements whose auctions have been canceled or removed, the second offer to be removed will still be in the list after the function finishes. The second finding relates to the operability of the protocol. The `removeCompleted` function iterates through the list of offers, and if an auction is completed, it will try to insert the offer.repoToken in the RepotokenList by calling the validateAndInsertRepoToken. This function can revert in some cases, for instance, if the token has already matured. That would mean that the removeCompleted would revert forever, and it would become impossible to remove offers for completed or canceled auctions from the list afterward. This also constitutes a high-severity issue since it would impact the protocol’s accounting and functionality. 

 

Reproducing proofs to prove code correctness over time

Similarly to normal testing, these formal verification proofs can also be used in CI. The significant difference is that with these proofs, any code changes will be tested for any possible state and inputs, and if the tests pass we can be confident that the code changes still preserve the desired properties.

Following is the sequence of commands to run the proofs:

Install Kontrol:

bash <(curl https://kframework.org/install)
kup install kontrol

Clone the Test Repository:

git clone git@github.com:term-finance/yearn-v3-term-vault.git
cd yearn-v3-term-vault
git submodule update --init --recursive

Run the Tests:

kontrol build
kontrol prove --config-profile setup
kontrol prove --config-profile tests

View the Results:

kontrol list

Conclusion

This engagement is a good example of how formal verification can be crucial in ensuring the correctness of protocols. The specification of invariants and properties helped not only identify issues but also be confident that the desired properties hold under certain pre-conditions. 

All the properties proven in the tests for the insert and removal operations of both list implementations and the properties for the get functions hold under the assumptions mentioned in each test. It is very important to ensure that when these functions are called the corresponding assumptions hold, otherwise preservation of the invariants is not guaranteed. 

The most interesting issue in this engagement is removeCompleted not preserving the removal operation correctness. First, it is not certain that this issue would be spotted with traditional code review, since it is a subtle bug that only manifests if we have lists with 3 elements or more and we try to remove 2 consecutive elements that are not the head of the list. In addition, and more importantly, the other formal verification tools in the market perform bounded model checking with bmc-depth 1 or at maximum 2. But, as already mentioned, this particular issue only manifests with lists with at least 3 elements.