This report represents work and conclusions based on Term Labs using Certora’s Prover tool to formally verify security properties of Term's smart contracts. Term finalized formal verification of the protocol's smart contracts using Certora's Prover solutions with guidance and technical support provided by the Certora team. The work was undertaken from Dec. 1, 2023 to Mar. 23, 2024. Some of these tests were verified using beta and staging versions of Certora's Prover, which are scheduled to be deployed to their production service in the near future. The latest commit that was reviewed and ran through the Certora Prover was 831292726cdc22e9d4d2953d59051fa00fbd4f72.
The scope of this verification includes all Term Servicer contracts within Term Protocol. This includes the following.
TermRepoToken.sol
TermRepoLocker.sol
TermRepoServicer.sol
TermRepoCollateralManager.sol
TermRepoRolloverManager.sol
Auction Contracts within Term Protocol were partially verified, with coverage on all functions except for those related to auction clearing, whose loop complexity is too elevated for formal verification. Runtime Verification was previously engaged to focus specifically on auditing and manually verifying this small but critical part of the codebase, see here. Contracts with partial coverage include:
TermAuction.sol
TermAuctionBidLocker.sol
TermAuctionOfferLocker.sol
The Certora Prover proved the implementation of the protocol is correct with respect to formal specifications written by the Term Labs team.
List of Main Issues Discovered
Severity: Low
Disclaimer
The Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of the Certora Prover are scoped to the provided specification, and the Certora Prover does not check any cases not covered by the specification.
We hope that this information is useful, but provide no warranty of any kind, explicit or implied. The contents of this report should not be construed as a complete guarantee that the contract is secure in all dimensions. In no event shall Term, Certora or any of its or their respective employees be liable for any claim, damages or other liability, whether in an action of contract, tort or otherwise, arising from, out of or in connection with the results reported here.
Overview of the verification
Description of the system
The Term Finance Protocol enables noncustodial fixed-rate collateralized lending on-chain (Term Repos) modeled on tri-party repo arrangements common in TradFi. Borrowers and lenders are matched through a unique recurring auction process (Term Auctions) where borrowers submit sealed bids and lenders submit sealed offers that are used to determine an interest rate that clears the market for participants of that auction. Participants who bid more than the clearing rate receive loans and participants willing to lend below the clearing rate make loans, in each case at the market-clearing rate. All other participants’ bids and offers are said to be “left on the table.” At the conclusion of an auction, borrowers receive loan proceeds and lenders receive ERC-20 tokens (Term Repo Tokens), which are receipts that lenders will burn to redeem for principal plus interest at maturity. Protocol smart contracts service these transactions by ledgering repayments and monitoring collateral health and liquidations.
Description of the specification files
For each contract, spec rules are divided into separate spec files per business logic function type (separate spec for state variable rules), but during runtime are compiled together in a rules.spec file. For the termRepoCollateralManager, the rules.spec is further divided into a rules.spec and other spec files for liquidations and state variables, due to the nature of high verification fun times for those functions.
Assumptions and Simplifications
Some loops were run with a fixed size of 1 in able to enable formal verification. Verifying beyond a 1st loop would have cause formal verification to time out.
Token prices are fetched from a constant mapping in CVL instead of a live price feed. This enables easier comparison of expected calculations and actual token amounts.
Some of the multiplications and divisions in liquidation functions in the smart contracts inherit a contract called ExponentialNoError, which scales and truncates multiplications and divisions in Solidity in a way that precision is not lost. The calculations in these functions were replaced with CVL equivalents in order to prevent timeouts of FV rules.
Contract Invariants and Rules
Common Rules
Applied to every contract in the protocol.
Rule: pairTermContractsRevertsWhenAlreadyPaired - constrain input space to only include contracts that have already been paired.
requireisTermContractPaired(); pairTermContracts@withrevert(e, args);assert lastReverted,"pairTermContracts(...) should revert when calling it on an already paired contract";assertisTermContractPaired(),"termContractPaired should not change when calling pairTermContracts(...) on an already paired contract";}
Rule: onlyPairTermContractsChangesIsTermContractPairedRule - ensures that only pairTermContracts(...) can change state of termContractPaired
bool isTermContractPairedBefore =isTermContractPaired();f(e, args);bool isTermContractPairedAfter =isTermContractPaired();assert isTermContractPairedBefore == isTermContractPairedAfter,"termContractPaired should not change when calling methods other than pairTermContracts(...)";
TermRepoToken.sol
Invariant totalSupplyIsSumOfBalances - ensures that the total supply of tokens always equals the sum of individual account balances, maintaining the principle of token conservation.
to_mathint(totalSupply()) == sumOfBalances
Rule: totalSupplyNeverOverflow - guarantees that the total supply of tokens cannot exceed the maximum value allowed by the system, preventing overflow errors.
assert totalSupplyBefore <= totalSupplyAfter;
Rule: noMethodChangesMoreThanTwoBalances - ensures that no single operation can alter more than two account balances at once.
Rule: onlyAllowedMethodsMayChangeAllowance - verifies that changes to token allowances are restricted to approved methods, ensuring that delegated spending limits are securely managed.
Rule: onlyAllowedMethodsMayChangeBalance - verifies that token balance changes within accounts can only be done through approved methods, preventing unauthorized modifications.
Rule: onlyAllowedMethodsMayChangeTotalSupply - verifies that changes to the total supply of tokens are conducted only through authorized methods, maintaining supply integrity.
Rule: onlyHolderOfSpenderCanChangeAllowance - verifies that changes to spending allowance, which is the limit set by the token holder for how much another account can spend on their behalf, can only be made by the token holder or a designated spender
Rule: mintRedemptionValueIntegrity - ensures that after minting tokens and returning a value, the balance of the minter and the total supply are correctly increased.
Rule: mintRedemptionValueDoesNotAffectThirdParty - verifies that when one account invokes mintRedemptionValue, this action does not affect third-party balances.
require addr1 != addr2;uint256 before =balanceOf(addr2);mintRedemptionValue(e, addr1, amount);assertbalanceOf(addr2) == before;
Rule: mintTokensDoesNotAffectThirdParty - verifies that when one account invokes mintOpenExposure, this action does not affect third-party balances.
require addr1 != addr2;uint256 before =balanceOf(addr2);mintTokens(e, addr1, amount);assertbalanceOf(addr2) == before;
Rule: burnIntegrity - ensures that after burning tokens, the balance of the burner and the total supply are correctly decreased.
Rule: burnAndReturnValueIntegrity - ensures that after burning tokens and returning a value, the balance of the burner and the total supply are correctly decreased.
Rule: burnRevertingConditions - checks conditions under which a burn operation should revert, such as not having enough balance, the contract being paused, etc.
Rule: burnDoesNotAffectThirdParty - verifies that burning tokens from one account does not affect third party balances.
assertbalanceOf(addr2) == before;
Rule: burnAndReturnValueDoesNotAffectThirdParty - confirms that burning tokens and returning a value from one account does not impact the balance of an unrelated account.
assertbalanceOf(addr2) == before;
Rule: transferIntegrity - asserts that after a transfer, the balances of the sender and recipient are updated correctly, respecting the case when sender and recipient are the same.
Rule: transferIsOneWayAdditive - demonstrates that if a transfer of a combined amount succeeds, individual transfers of the components should also succeed without affecting the final state.
transfer(e, recipient,assert_uint256(sum));storage after1 = lastStorage; transfer@withrevert(e, recipient, amount_a) at init; // restores storageassert!lastReverted; //if the transfer passed with sum, it should pass with both summands individually transfer@withrevert(e, recipient, amount_b);assert!lastReverted;storage after2 = lastStorage;assert after1[currentContract] == after2[currentContract];
Rule: transferRevertingConditions- identifies conditions under which a transfer should revert, such as the sender not having enough balance.
Rule: transferDoesNotAffectThirdParty - ensures that a transfer between two accounts does not affect the balance of a third party.
assertbalanceOf(addr2) == before;
Rule: transferFromIntegrity - confirms that after a transferFrom operation, the balances of the holder and recipient are correctly adjusted, and the allowance is updated appropriately.
Rule: transferFromIsOneWayAdditive - shows that if a transferFrom for a combined amount is successful, then separate transferFrom operations for each component of the amount should also succeed, without altering the final state.
transferFrom(e, owner, recipient,assert_uint256(sum));storage after1 = lastStorage; transferFrom@withrevert(e, owner, recipient, amount_a) at init; // restores storageassert!lastReverted; //if the transfer passed with sum, it should pass with both summands individually transferFrom@withrevert(e, owner, recipient, amount_b);assert!lastReverted;storage after2 = lastStorage;assert after1[currentContract] == after2[currentContract];
Rule: approveIntegrity - ensures that the allowance is correctly set after an approve operation.
assertallowance(holder, spender) == amount;
Rule: approveRevertingConditions - identifies scenarios in which an approve operation should revert, such as when trying to approve from a zero address.
Rule: onlyAllowedMethodsMayChangeMintExposureCap - ensures that only specific methods can modify the mint exposure cap. Methods like minting, burning, or resetting the cap are allowed to change it.
Rule: mintExposureCapNeverOverflow - verifies that when the mint exposure cap is increased, this action does not cause it to overflow, ensuring the cap's value remains within safe limits.
Rule: noMethodChangesRedemptionValue - confirms that the redemption value remains unchanged across transactions, except by methods explicitly intended to modify it. This rule ensures stability in the redemption value.
Rule: onlyRoleCanCallRevert - checks if a method call that is not a view and requires specific roles to execute successfully, does not revert if the caller has the necessary role.
Rule: onlyRoleCanCallStorage - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications.
Rule: onlyAllowedMethodsMayChangeTransfersPaused - ensures that the state of transfers being paused can only be altered by specific methods designated for pausing or unpausing transfers.
Rule: noMethodChangesTermRepoId - confirms that the Term Repo ID remains constant and is not changed by any method calls, ensuring its immutability post-initialization.
Rule: onlyAllowedMethodsMayChangeEmitter - verifies that the emitter's address can only be changed through specific methods, preserving the integrity and security of the emitter identification.
Rule: reachability - verifies that all non-initialization and non-upgrade methods can be executed, ensuring contract functionality is accessible.
f(e,args);satisfy true;
Rule: transferTokenFromWalletIntegrity - validates the integrity of transferring tokens from the wallet, checking the update in treasury and sender balances post-transaction.
Rule: transferTokenToWalletIntegrity - ensures the correct adjustment of balances when tokens are transferred to the wallet, factoring in role permissions and pause status.
Rule: pauseTransfersIntegrity - validates that transfers can be paused correctly by the authorized role, ensuring the state is changed as expected.
pauseTransfers(e);asserttransfersPaused();
Rule: unpauseTransfersIntegrity - confirms that transfers can be unpaused accurately, reverting the paused state and allowing transactions to proceed.
unpauseTransfers(e);assert!transfersPaused();
Rule: onlyRoleCanCallRevert - ensures that methods not related to initialization, upgrade, or role management only revert if the caller lacks the necessary roles. This rule safeguards against unauthorized actions while allowing legitimate operations.
currentContract.f@withrevert(e,args);// Verification if the method didn't revert, the caller must possess one of the specified roles.assert!lastReverted =>hasRole(SERVICER_ROLE(),e.msg.sender)||hasRole(ADMIN_ROLE(),e.msg.sender)||hasRole(DEVOPS_ROLE(),e.msg.sender)||hasRole(INITIALIZER_ROLE(),e.msg.sender);
Rule: onlyRoleCanCallStorage - verifies that storage modifications by non-view methods are properly guarded by role checks, preventing unauthorized changes to the contract's state. This rule enforces role-based access control for sensitive operations.
storage storeBefore = lastStorage;currentContract.f(e,args);storage storeAfter = lastStorage;// Conditionally asserts that if storage was altered, the action must have been performed by an entity with an appropriate role.
assert storeBefore != storeAfter =>hasRole(SERVICER_ROLE(),e.msg.sender)||hasRole(ADMIN_ROLE(),e.msg.sender)||hasRole(DEVOPS_ROLE(),e.msg.sender)||hasRole(INITIALIZER_ROLE(),e.msg.sender);
TermRepoServicer.sol
Invariant: totalOutstandingRepurchaseExposureIsSumOfRepurchases - asserts that the total outstanding repurchase exposure is equal to the sum of all individual repurchase exposures, ensuring consistency within the ledger.
Rule: onlyAllowedMethodsMayChangeTotalOutstandingRepurchaseExposure - specifies that only particular methods can increase or decrease the total outstanding repurchase exposure, aligning changes with expected business logic operations.
Rule: totalOutstandingRepurchaseExposureNeverOverflows - ensures that actions intended to increase the total outstanding repurchase exposure do not result in an overflow, preserving the integrity of financial calculations.
Rule: onlyAllowedMethodsMayChangeTotalRepurchaseCollected - identifies methods permitted to increase or decrease the total repurchase collected, ensuring that financial metrics reflect actual repurchase activity accurately.
Rule: totalRepurchaseCollectedNeverOverflows - verifies that the total repurchase collected metric cannot overflow as a result of any operation, maintaining the system's financial stability.
Rule:shortfallHaircutMantissaAlwaysZeroBeforeRedemptionAndLessThanExpScaleAfter - confirms the shortfall haircut mantissa remains zero before the redemption timestamp and falls within expected bounds after, ensuring fair and predictable financial adjustments.
Rule: totalRepurchaseCollectedLessThanOrEqualToLockerPurchaseTokenBalance - ensures that the total repurchase collected does not exceed the locker's purchase token balance, preventing overestimation of collected repurchases.
require(termRepoLocker() == stateLocker); // bounds for test
require(purchaseToken() == stateToken); // bounds for test
require(totalRepurchaseCollected() <= stateToken.balanceOf(stateLocker)); // starting condition
require(e.msg.sender != stateLocker); // repo locker contract does not have calls to servicer
require(!isTokenCollateral(stateToken)); // token will not be both purchase and collateral token
f(e, args);
assert (totalRepurchaseCollected() <= stateToken.balanceOf(stateLocker));
Rule: noMethodsChangeMaturityTimestamp - validates that no method changes the maturity timestamp, ensuring consistency in the term's length and financial obligations.
Rule: noMethodsChangeEndOfRepurchaseWindow - confirms the end of the repurchase window is immutable across all contract interactions, preserving the predetermined timeframe for repurchases, which is critical for contractual agreements.
Rule: noMethodsChangeRedemptionTimestamp - ensures the redemption timestamp remains constant across all contract interactions, guaranteeing the redemption period's stability and predictability.
Rule: noMethodsChangeServicingFee - verifies that the servicing fee rate is maintained across all transactions, ensuring consistent fee calculations and financial expectations for parties involved.
Rule: onlyAllowedMethodsChangeShortfallHaircutMantissa - restricts adjustments to the shortfall haircut mantissa to specific authorized methods, safeguarding the metric's integrity against unauthorized modifications.
Rule: noMethodChangesPurchaseToken - confirms the purchase token's address remains unaltered through contract operations, ensuring continuity and reliability in financial mechanisms involving the token.
Rule: onlyAllowedMethodsMayChangeTermContracts - specifies that term contract addresses can only be modified through designated methods, preventing unauthorized updates and maintaining contract ecosystem integrity.
Rule: onlyAllowedMethodsMayChangeRepurchaseExposureLedger - limits the conditions under which the repurchase exposure ledger can be altered, ensuring that changes are strictly governed and reflect actual repurchase activities.
Rule: burnCollapseExposureMonotonicBehavior - verifies that burning to collapse exposure reduces the caller's repo token balance, their repurchase obligation, and the total outstanding repurchase exposure monotonically, ensuring systemic risk reduction and individual accountability.
Rule: burnCollapseExposureIntegrity - ensures that burning for exposure collapse adjusts the repo token balance, repurchase obligation, and total outstanding repurchase exposure by the expected amounts, reflecting accurate and fair financial adjustments.
Rule: burnCollapseExposureDoesNotAffectThirdParty - confirms that an individual's action to burn repo tokens to collapse exposure does not impact the financial positions (token balances or repurchase obligations) of unrelated third parties, maintaining isolation of financial activities.
Rule: mintOpenExposureMonotonicBehavior - ensures that minting open exposure increases the minter's repo token balance, their repurchase obligation, and the total outstanding repurchase exposure, as well as the minter's collateral balance, indicating correct operation and accountability in minting activities.
Rule: mintOpenExposureIntegrity - confirms that minting for open exposure results in expected increases in the minter's repo token balance and repurchase obligation, as well as the total outstanding repurchase exposure, demonstrating the transaction's impact aligns with predefined financial mechanisms.
Rule: mintOpenExposureDoesNotAffectThirdParty - verifies that a minter's action to open exposure does not alter the repo token balances of unrelated third parties, ensuring the isolation of minting effects within the financial ecosystem.
Rule: redemptionsMonotonicBehavior - verifies that redemption operations result in expected changes to the balances and obligations involved, ensuring that the redeemer's repo token balance decreases, their purchase token balance increases, and the overall repurchase obligations and available tokens within the locker adjust accordingly.
Rule: redemptionsIntegrity - confirms that the redemption of repo tokens by a redeemer leads to the precise adjustments in the total repurchase collected, the repo token balance of the redeemer, and the purchase token balance in accordance with the redemption value and terms defined, reflecting the accurate financial transaction and impact.
Rule: redemptionsDoesNotAffectThirdParty - ensures that a redemption action taken by one participant does not inadvertently alter the financial position or balances of unrelated third parties, maintaining the integrity and isolation of individual transactions within the ecosystem.
Rule: redemptionsRevertConditions - evaluates whether the operation correctly reverts under the prescribed conditions, ensuring compliance with defined contractual behaviors and protections.
Rule: repaymentsMonotonicBehavior - validates that repayments lead to expected monotonic changes in borrower obligations and system totals, ensuring borrower balances and overall repurchase exposures decrease as payments are made, while the total repurchase collected and potentially the collateral values adjust accordingly.
Rule: repaymentsIntegrity - ensures the integrity of repayments by verifying that the repayments correctly decrease the borrower's obligations and appropriately adjust the system's repurchase exposure and collected totals, with specific attention to the treatment of collateral in the event of complete repayment.
Rule: repaymentsDoesNotAffectThirdParty - confirms that a borrower's repayment activity does not inadvertently affect the financial obligations or collateral standings of any unrelated third parties, preserving the isolation and accuracy of individual account statuses within the system.
Rule: repaymentsRevertingConditions - check if the operation correctly reverts under specified conditions, ensuring adherence to defined contractual behaviors and safeguards.
Rule: liquidatorCoverExposureIntegrity - validates the integrity of a liquidation process where a liquidator covers the exposure of a borrower using purchase tokens. It checks that balances and obligations adjust correctly, reflecting the liquidation payment in system totals and individual accounts.
Rule: liquidatorCoverExposureDoesNotAffectThirdParty - ensures that the liquidation process does not inadvertently impact the financial status or obligations of any third parties, maintaining the precision and isolation of account transactions within the system.
Rule: liquidatorCoverExposureRevertConditions - evaluate if the transaction reverts as expected under identified conditions, ensuring compliance with system rules and safeguards.
Rule: liquidatorCoverExposureWithRepoTokenIntegrity - examines the proper functioning of liquidation via repo tokens, verifying that such transactions correctly reduce borrower obligations and adjust system and participant balances in accordance with the repo tokens used in the liquidation.
Rule: liquidatorCoverExposureWithRepoTokenRevertConditions - define conditions that would lead to a transaction revert; aggregate revert conditions to determine expectation; eliquidation attempt with potential revert and validate against expected outcome; ensure actual revert aligns with expectations based on identified conditions.
Rule: openExposureOnRolloverNewIntegrity - ensures that all relevant balances properly accounted for after opening a repoExposure on account of a successful rollover.
Rule: openExposureOnRolloverNewDoesNotAffectThirdParty - verifies that rolling over loan exposures from one account does not affect third-party balances.
Rule: openExposureOnRolloverNewRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: closeExposureOnRolloverExistingIntegrity - ensures that all relevant balances properly accounted for after closing a repoExposure on account of a successful rollover.
Rule: closeExposureOnRolloverExistingDoesNotAffectThirdParty - verifies that rolling over loan exposures from one account does not affect third-party balances.
Rule: closeExposureOnRolloverExistingRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.