Avoided Solidly Voting System Manipulation

“premature optimization is the root of all evil (or at least most of it) in programming.”
— Donald Knuth

Author: Ori Dabush

Editors: Sameer Arora, Uri Kirstein

In this blog I will write about a bug found in a past version of Solidly, an exchange on the Fantom Mainnet, using the Certora Prover. This bug was found and fixed before the contracts were deployed on the mainnet.

Solidly is a system that allows low-cost, near 0 slippage trades on uncorrelated or tightly correlated assets. Liquidity providers (LPs) are given incentives in the form of tokens. The amount received is 100% of the weekly distribution weighted on votes from ve-token holders.

Vested Escrow (ve) is the core voting mechanism of the system, that is used to gauge rewards and voting.

The mechanism for voting is:

1. Create a lock (NFT) using the create_lock or create_lock_for functions, which deposit tokens and lock them for a given amount of time.
2. Call the vote or voteMixed function from the BaseV1Voter contract with your NFT’s token id and vote for the pools you would like to incentivize.

The ve.sol contract indicates whether a token id has voted or not. This data structure could be easily implemented by a uint256 to bool mapping, but here we see a delicate optimization — instead of saving a whole byte (8 bits) for every token id, only 1 bit is saved.

The voted mapping from uint256 to uint256 saves a bit for every token id: for an NFT with token id x, its bit will be the x % 256 bit of the voted[x / 256] element. 256 token ids’ voting states are saved in one uint256 variable.

On a call to vote, the bit of the token that voted is set to 1 (assuming a non zero vote). Similarly, on a call to reset (a function that removes a given token id’s votes), the mentioned bit is set to 0.

This is a nice optimization that does the same actions with 12.5% of the storage compared to a mapping from a token id to a boolean value. However, as you might have noticed, it is much harder to understand the code when it uses complicated data structures and bitwise operations. It is even harder to review and audit it that way. Also, when writing complex code, you are more likely to do something wrong.

The Bug

Let’s see how a bug in this optimization can be exploited to manipulate votes in the Solidly system.

Let’s look at the internal function that sets the values of the voted mapping:

function updating the votes mapping

This function is eventually called by vote and reset functions, and it receives two parameters — a token id and a boolean value hasVoted. If the hasVoted parameter is true, it sets the bit that belongs to the given token id to 1 (other bits are unaffected). This is done by calculating a mask with 1 at the (tokenId % 256)th position and zeros at the rest and performing a bitwise OR operation between the previous value of voted[tokenId / 256] and this mask.

Similarly, if the hasVoted parameter is false, it should set ONLY the mentioned bit to 0, leaving all other bits unaffected. To do that, the function performs a bitwise AND operation between the previous value of voted[tokenId / 256] and the mask 0 << _tokenId % 256. However, this is incorrect as the above operation zeroes out ALL the bits of the uint256 value! Left shifting 0, by any value, is still 0! And thus, performing a bitwise AND operation with 0 sets all the bits of voted[tokenId / 256] to 0.

Exploiting The Bug

This bug might lead to various exploits. Let’s take a look at one of them:

The exploit is in the merge function. The merge function in the ve.sol contract receives two token ids — from and to, and assures that the from token id hasn’t voted yet by checking

the _tokenHasVoted function returns a boolean based on the token id’s bit

It then merges the NFTs — transfers all the amount of ve token deposited for the from token to the to token (there is no actual token transfer, it just changes the inner data) and burns the from token. As you can see, this function shouldn’t be executed if the from token has already voted. However, because of the above bug, an NFT that has already voted can be reset to 0 without removing its votes, and, therefore, can be used again with this function.

Now let’s assume that an attacker manages to create 2 NFTs, id0 and id1, where id0 / 256 = id1 / 256 (integers division, obviously). Their bit is represented in the same uint256 in the voted mapping. Let’s assume for simplicity that the ids are 1 and 2 and that both NFTs have a starting value of 100 tokens.

The attacker can now call vote with token id 1 and the appropriate vote data (pools and weights). In the vote function, the voting data will be updated, as well as the voted mapping data. That means that the second bit (index 1 is the second bit) of voted[0] is 1 now.

This is not a problem for the attacker because he holds the NFT with token id 2. The attacker can now call the reset function with token id 2, which will reset all the voting data of token id 2 — both the data saved in the BaseV1Voter and the voted data in the ve.sol contract. But because of the bug, it will not only set the third bit of voted[0] to 0; it will set the whole voted[0] value to 0. In particular, the second bit (which belongs to token id 1) is 0 too.

After that, the attacker can call merge with from = 1 and to = 2, which will deposit the value from token id 1 to token id 2. But it will not delete the voting data of token id 1, meaning that even though the tokens deposited have already been used to vote, nothing stops the attacker from using them again to vote with token id 2.

The attacker can use the exploit to vote type(uint256).max — 1 times, as long as he has at least 2 NFTs in the same range. It can be done with multiple NFTs — every time the attacker can vote, call reset with a non voted NFT token id (that will also zero the value of the voted token id in the voted mapping), merge the voted token to the new NFT, and repeat.

Using that exploit, an attacker can easily manipulate the voting system to incentivize the pools he wants and get 100% of the fees on behalf of other Solidly users.

In the current version of Solidly, the bug was resolved by removing the above optimization and changing the voted variable back to mapping(uint => bool) .

Using formal verification to catch the bug

The first step towards formally verifying a system is to design a specification for the system. You can think of a specification as a set of properties (or rules) you would like your system to adhere to. So what are some of the rules that we can write for the _setTokenHasVoted function to help catch the above bug?

We know that the function _setTokenHasVoted(_tokenId, _hasVoted) updates the mapping bit corresponding to the _tokenId. Furthermore, we would want the function to leave the remaining bits, those not belonging to the _tokenId, unaffected by the invocation. Thus, we can write the following rule:

_setTokenHasVoted only updates the bit corresponding to the _tokenId, leaving other bits unaffected.

Now that we have a rule description, we need to write it formally using a specification language. Here we’ll translate the above rule into Certora’s formal specification language CVL. CVL currently has no single instruction to specify our above property directly. Thus, we would first need to break the above rule down into simpler statements with a direct CVL analog.

Let’s consider two different token ids: tId1 and tId2. Then, when we invoke _setTokenHasVoted(tId1, _hasVoted), we want it to only update the bit corresponding to tId1, leaving the bit for tId2 unaffected. Thus, the bit for tId2 before the function invocation (call it tId2Before) should be equal to the bit for tId2 after the invocation ( tId2After). Here are the steps we would need to perform to verify our rule:

• Let tId1 and tId2 be two token IDs such that tId1 != tId2
• Let tId2Before be the state of the bit corresponding to tId2 before the function invocation
• Invoke _setTokenHasVoted(tId1, _hasVoted)
• Let tId2After be the state of the bit corresponding to tId2 after the function invocation
• Assert tId2Before == tId2After

Each of the above statements have a direct CVL instruction we can use. Hence, we can now write the above rule in CVL as:

rule to check tId2Before == tId2After

(Note: tId1, tId2, and _hasVoted are symbolic values, i.e., the Certora Verification Prover checks the rule with all possible value combinations of tId1, tId2, and _hasVoted and returns the values that result in a violation of the rule. If no such value combinations exist, then the rule is verified successfully!)

Running the above rule with Certora Prover we get the following results back:

Certora Prover run for noChangeToOtherBits

Understanding the above counterexample:

• The prover runs the rule with all possible value combinations for the input parameters and shows the values causing a violation. In this case, a violation is found for tId1 = 0, tId2 = 41, _hasVoted = false

• Initially, tId2’s bit (stored at tId2Before) is set to 1 (hasVoted(tId2=41) returns true)

• We then invoke the function setVote(tId1=0, _hasVoted=false)

• Checking tId2’s bit again (and storing at tId2After), it is now set to 0 (hasVoted(tId2=42) returns false)

• Hence, the rule is violated!

Check out demo.certora.com. Here you can also find examples of other interesting bugs that Certora prover has found in the past. You can also design and play with your own rules!