Preventing Reentrancy bugs

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

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 such a reentrancy bug was detected by the Certora Prover in the Synthetix Depot contract that has since been fixed. The Certora Prover detected 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:

Technical Description and Example

When exchangeEtherForSynths is called, the Depot iterates over the queue, from depositStartIndex, a global variables of the contract, or 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 illustrates the execution 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 2). 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 advanced by 1 (Slides 3-6). During the Ether send operation, Eve uses the callback function to call exchangeEtherForSynths once again (with 1 sUSD worth of Ether) (Slide 7). 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 8-10). The next entry (of Bob) has more than enough sUSD to fulfill Eve's request and the function will exit (Slides 11-14). 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 15). 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), so once again the Depot advances depositStartIndex by 1, resulting with depositStartIndex equals 3 (Slides 16-18). In the next entry (Bob's entry), Dave request will be fulfilled (it only needed another 50 sUSD) and the function will exit (Slides 19-22). 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. In order for the attack to work, we must be able to 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 current gas constraints, there might still be a different scenario that can exploit the bug.

Possible Mitigation

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

Outcome

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

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 Reentrancy attack. The Certora company is developing a unique product for formally verifying that a given contract cannot suffer from reentrancy attack. The tool was used to detect the above vulnerability.

Conclusion

One of the most difficult 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.