Certora Bug Disclosure: Lost Signer Fees in the TBTC system

Another use case for formal verification

Thomas Bernardi, Nurit Dor, Anastasia Fedotov, Shelly Grossman, Alexander Nutz, Lior Oppenheim, Or Pistiner, Mooly Sagiv, John Toman, James Wilcox

TBTC is a system built on top of the Keep network, which provides users the ability to deposit their Bitcoin tokens (BTC) in exchange for a 1:1 Bitcoin-backed ERC-20 token in the Ethereum blockchain (TBTC). This lets BTC owners interact with the diverse world of DeFi. On June 29th, 2020, Lior Oppenheim discovered a bug in the protocol (git commit 91100a69d70acdba738c9feffcbf85fb39147ab2) where a key invariant of the code is broken. This bug was confirmed by the Keep team on June 30th, 2020. Notably, this bug was discovered after the Keep team suggested not to use the version of the protocol that exists in mainnet. Malicious users can prevent the signer group from getting the signer fee for this deposit.

General Description

When a user (the "depositor") creates a deposit, the Keep network assigns a "signer group" which is in charge of keeping the deposited BTC in the BTC-chain, while providing collateralization for the TBTC minted on the ETH-chain. To compensate signers for providing liquidity and taking the associated risks, they are entitled to a "signer fee", which is given in TBTC. Once the depositor creates a deposit, she gets a non-fungible ERC-721 token (TDT) which provide her the ownership of that deposit. After the deposit is confirmed, the depositor can use the TDT she owns to mint the corresponding TBTC amount. In this process, she loses the ownership of the deposit to a contract called "VendingMachine". Any other user with the required amount of TBTC can now gain ownership of this deposit (by buying the TDT from the VendingMachine) and redeem it for the underlying BTC. It is important to mention that the signer fee is not escrowed for the signers from the start of the deposit process, but only in the following cases:

  1. For the first time the TDT is being used for minting TBTC, when a portion of it would be given to the deposit contract for escrow.
  2. If no TBTC was ever minted using this TDT - It will be escrowed when the TDT owner redeems her TDT for the actual BTC. The TDT owner must provide this extra TBTC amount in the process of redemption.

Usually, one of these cases will occur during the deposit's lifetime.

The Bug

By deliberately losing ownership of a TDT in a non-trivial way, a malicious user can prevent either of the above cases from ocurring, so the signer group will not get the signer fee for this deposit.

Technical Description

If a user sends her owned TDT to the VendingMachine using standard ERC-721 transfer function, the system is tricked to assume that the signer fee had already been escrowed, since VendingMachine ownership usually means that someone must have already minted TBTC at least once. Thus, she can start a redemption process where there is no escrowed signer fee in the deposit contract. The signer group must follow the protocol and release the deposited BTC, or they will be slashed. Only on the final step (when the signer group provides a proof that the BTC was released), it will be discovered that they are unable to get the signer-fee, since it was never escrowed.

Invariant-Based Bug Finding

One way to detect bugs in code in general and in smart contracts in particular is by looking for common valnerebilities, e.g., overflow errors.

We argue that a complementary way to increase code security is to specify desired correctness rules of the code and then identify input scenarios which violate these rules. This can be done manually or using tools such as the Certora Prover or the Soldity SMTchecker to automoatically detect potentially rare and hard to find scenarios which viloate the rules. When the code is fixed, the tool is executed again to see if the rules hold after the change or to uncover another potential bug.

The following rule is expected to hold in TBTC.

invariant canOwnTTDTOnlyIfHasTBTC(uint256 tdtId)
  isOwnedByVendingMachine(tdtId) => 
  tbtc.balanceOf(tdtAddress(tdtId)) > 0

This rule checks that if the VendingMachine owns a TDT, then the corresponding deposit must have some TBTC escrowed for the signer-fee. The invariant is violated in case a user calls transfer(tdtId,vendingMachine) instead of the function that is used in the normal flow, tdtToTbtc(uint256 _tdtId) (which sends the TDT to the VendingMachine and mint the corresponding TBTC)

Conclusion

One of the most difficult tasks in formal verification is understanding what specification the code should obey. This bug shows that very simple rules can be used to automaticaly detect easy to miss corner cases leading to very subtle bugs.

Contact Certora at info@certora.com to find out how we can help.