Certora Bug Disclosure: Lost Signer Fees in the TBTC system

TBTC is a system built on top of the Keep network, which allows users 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) that breaks a key invariant of the code. The Keep team confirmed this bug 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 the 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”. The signer group 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”, given in TBTC.

Once the depositor creates a deposit, she gets a non-fungible ERC-721 token (TDT) which provides 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 occurring, so the signer group will not get the signer fee for this deposit.

Technical Description

Suppose a user sends her owned TDT to the VendingMachine using the standard ERC-721 transfer function. In that case, the system is tricked into assuming 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 with 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 proof that the BTC was released) will it be discovered that they cannot 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 is by looking for common vulnerabilities, 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 that violate these rules. This can be done manually or using tools such as the Certora Prover or the Solidity SMTchecker to automatically detect potentially rare and hard-to-find scenarios which violate 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, 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 mints the corresponding TBTC)

Conclusion

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

Contact Certora at info@certora.com to find out how we can help you find bugs in your smart contracts.