Preventing reentrancy bugs — another use case for formal verification

Reentrancy bugs are well known to put smart contracts at risk of severe financial losses, yet many smart contract developers still find it challenging to protect their code from such attacks. In December 2019, the Certora Prover detected such a reentrancy bug in the Synthetix Depot contract. Synthetix have fixed the bug since. The Certora Prover caught this bug with a generic property defined in the ECF paper without the need for specifying properties of the Depot contract. The old and vulnerable code is available here.

Reentrancy Bug in the Depot Contract — General Description

To allow the sUSD minters to easily sell their minted coins for Ether, the Synthetix system provides a simple platform for depositing sUSD tokens into a deposit box Depot, which will sell the tokens on their behalf in the Synthetix exchange. The Depot implements a queue to keep track of all the deposits. When someone wishes to exchange Ether for sUSD, the Depot iterates over the queue from its start:

• In the simple case, the first entry in the queue has more than enough sUSD to completely fulfill the requested amount. In that case, the Depot updates the record with the reduced amount, transfers the Ether of the sUSD to the entry’s user, transfers the requested amount of synth to the sUSD buyer, and exits the function.
• In the more complex case, there isn’t enough sUSD in the first entry of the queue. The Depot pops the record out of the queue, transfers a proportional amount of Ether to the entry’s user (according to the deposit amount), transfers the synths in the entry to the sUSD buyer, reduces the amount of requested sUSD accordingly, and continues to iterate to the next deposit entry. In the end, the requested sUSD will be equal to 0, meaning that the request was fulfilled (the entire amount of Ether was converted to sUSD). However, the amount of sUSD requested may be larger than the sum of all deposits. In that case, the queue will be completely emptied, and the function’s initiator will get back any amount of Ether left (not converted to sUSD).
• Also, an sUSD depositor can decide she wishes to withdraw the amount she deposited. In that case, the Depot scans the entire queue, deleting deposit entries that belong to the depositor (nulling the user & amount fields of those entries). Therefore, the Depot may encounter a null record during the processing of the exchange request. In that case, the Depot will skip that record. The bug lies in the fact that a callback function can initiate another call to the Depot during the Ether transfer to the depositor (by a send function). With the queue correctly formed, one can make the pointer to the start of the queue skip over a valid deposit entry, thus losing the owner of this entry the money she deposited.

Technical Description and Example

When the contract exchangeEtherForSynths is called, the Depot iterates over the queue, from depositStartIndex, a global variable of the contract, until the requested amount of synth is fulfilled. For every null entry or an entry without enough synths (which will be emptied soon), the Depot immediately advances depositStartIndex by 1.

Let’s assume that Eve, Alice, Bob & Carol have all deposited 100 sUSD to the Depot (in that order). The slides illustrate the exec ution of this example.

In the first step, Alice changed her mind and withdrew her deposits. Therefore the deposit will look like this

deposit[] = [
    {owner: Eve, amount:100},
    {owner: "", amount:0},
    {owner: Bob, amount:100},
    {owner: Carol, amount:100}
]

with depositStartIndex=0 (Slide 4). Dave wishes to transfer his 150 sUSD worth of Ether to sUSD, and he calls exchangeEtherForSynths. At first, since Eve’s entry has only 100 sUSD, it will be deleted, and the depositStartIndex will advance by 1 (Slides 5–8). During the Ether send operation, Eve uses the callback function to call exchangeEtherForSynths once again (with 1 sUSD worth of Ether) (Slide 9). Now, since depositStartIndex=1 (it’s a global variable), Depot will first encounter the empty entry left by Alice, so it will skip it, making depositStartIndex=2 (Slides 10–12). The next entry (of Bob) has more than enough sUSD to fulfill Eve’s request, and the function will exit (Slides 13–16). Now, when we return to the original call (by Dave), the queue looks like this:

[
    {owner: "", amount:0},
    {owner: "", amount:0},
    {owner: Bob, amount:99},
    {owner: Carol, amount:100}
]

with depositStartIndex=2 (Slide 17). Since we are back to the first iteration over the queue, the next entry is again Alice’s empty entry (the same one processed in the callback). Once again the Depot advances depositStartIndex by 1, resulting in depositStartIndex equals 3 (Slides 18–20). In the next entry (Bob’s entry), Dave’s request will be fulfilled (it only needed another 50 sUSD), and the function will exit (Slides 21–24). The final state of the Depot is problematic — the double-counting of Alice’s empty entry caused Depot to skip over Bob’s entry (2), and now depositStartIndex points to Carol’s entry (3). In theory, this method allows us to skip an arbitrary amount of entries, according to the number of empty entries after the entry owned by Eve, even to the point where the depositStartIndex is larger than the deposit queue size.

This bug is hard to exploit directly. For the attack to work, we must carry out the second call to exchangeEtherForSynths consuming only 2300 gas (the amount of gas allowed for a callback). According to our tests, this call demands approximately 80k. This makes the above attack unrealistic in the current gas metering scheme. However, even in the existing gas constraints, there might still be a different scenario to exploit the bug.

Possible Mitigation

There are different ways to assure that the code cannot suffer from reentrancy attacks, including:

• Completely prevent callback execution in the contract.
• Change the for loop into a while loop and access the start of the queue each time with deposits[depositStartIndex], which is always up to date.
• Allow users to extract their synths from a specific index in the deposits array (even outside the queue range). This will help ensure that even when the queue indices’ consistency is violated, a depositor can still gain back the sUSD she deposited in a particular entry.

Outcome

Since we reported the bug in December 2019, the Synthetix team promptly addressed the issue and deployed a fix to the mainnet. The official response said that because of the current gas limitation, the attack is theoretical. Nevertheless, the finding is a legitimate vulnerability. Synthetix added reentrancy protection to avoid possible attacks in the future.

Techniques for Verifying Absence of Reentrancy Attacks

The ECF paper describes a method for dynamically checking at the EVM level that an execution trace does not suffer from a reentrancy attack. The Certora company is developing a unique product for formally verifying that a given contract cannot suffer from a reentrancy attack. We used the tool to detect the above vulnerability.

Conclusion

One of the most challenging tasks in formal verification is understanding what the code needs to obey. This bug shows that even without formal specification, tools such as Certora Prover can be used to automatically detect severe bugs in the code before the code is deployed.

Contact Certora at info@certora.com to find out how we can help to verify your smart contract.