In this blog post we’re going to deep dive into the Sorra Finance hack, find the root cause of the bug and create a certora rule which could’ve prevented the exploit.
Hack Details
Sorra Staking contract is basically a ponzi scheme. Users deposit ERC20 tokens, wait for some time, and, if there’re funds available, withdraw more ERC20 tokens.
Sorra offers 3 staking tiers (i.e. options for how long to stake ERC20 tokens):
1. 14 days with 5% APY (code)
2. 30 days with 20% APY (code)
3. 60 days with 40% APY (code)
Normal flow example:
1. User deposits 100 ERC20 tokens in tier0 (14 days staking period)
2. User waits for 14 days
3. User withdraws 105 ERC20 tokens (if there were other users who also staked in this ponzi-style contract)
Now check getPendingRewards() and _calculateRewards() methods. The root cause of the issue is that pending rewards don’t take into account already distributed rewards.
The bug in the getPendingRewards() method makes the following buggy flow possible:
1. User deposits 100 ERC20 tokens in tier0 (14 days staking period)
2. User waits for 14 days
3. User withdraws 1 wei and gets 5 ERC20 token rewards (which is expected)
4. User withdraws 1 wei again and suddenly gets ~5 ERC20 token rewards again (remember that pending rewards don’t account for already distributed ones)
5. Loop continues until the contract is out of funds
With all that in mind the Sorra Staking contract was exploited earlier this year.
Certora Rule
Now it’s time to create a certora rule that could’ve caught that bug.
Create empty sorra.conf and sorra.spec files.
Certora Config
Certora config files allow setting all of the certoraRun CLI tool options in a file instead of passing them in the CLI options.
We need to add 2 contracts to our “scene” (i.e. contracts that certora is operating on), sorraStaking (developers chose it to start with lowecase) and MockERC20 (reward token mock):
|
1 2 3 4 |
"files": [ "src/sorra/SorraStaking.sol:sorraStaking", "test/MockERC20.sol", ] |
Next we need to tell certora that it should use our MockERC20 contract for rewardToken implementation:
|
1 2 3 |
"link": [ "sorraStaking:rewardToken=MockERC20", ] |
We should also set which spec should be used for verification of the sorraStaking contract:
|
1 |
"verify": "sorraStaking:test/sorra/certora/sorra.spec" |
We’re going to use the withdrawIntegrity name for the rule that checks the bug:
|
1 2 3 |
"rule": [ "withdrawIntegrity", ] |
Next we add a comment that will be shown in the certora dashboard:
|
1 |
"msg": "Sorra Finance" |
We also set the rule_sanity so that certora could report whether the rule we’ve just created is vacuous:
|
1 |
"rule_sanity": "basic" |
Finally, we set the optimistic_loop because (as far as I understand) here, here or here certora executes the loop too many times thus violating the built-in loop unwinding condition rule:
|
1 |
"optimistic_loop": true |
In the end we get the following certora config:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 |
{ "files": [ "src/sorra/SorraStaking.sol:sorraStaking", "test/MockERC20.sol", ], "link": [ "sorraStaking:rewardToken=MockERC20", ], "verify": "sorraStaking:test/sorra/certora/sorra.spec", "rule": [ "withdrawIntegrity", ], "msg": "Sorra Finance", "rule_sanity": "basic", "optimistic_loop": true, } |
Certora Spec
Now it’s time to modify our empty sorra.spec file.
First of all we import our MockERC20 contract so that we could use it in the spec:
|
1 |
using MockERC20 as rewardToken; |
Next we create a withdrawIntegrity rule and define env (blockchain environment with properties like env.msg.sender, etc…) and amount (specifies the withdraw amount) variables which may take arbitrary inputs:
|
1 2 3 4 |
rule withdrawIntegrity() { env e; uint256 amount; } |
Then we set some sane preconditions in the withdrawIntegrity rule so that certora could provide counterexamples without overflowing (somehow using the mathint type didn’t take any effect):
|
1 2 3 4 5 6 |
// user's balance < 100 mln require rewardToken.balanceOf(e, e.msg.sender) < 100000000000000000000000000; // withdraw amount < 100 mln require amount < 100000000000000000000000000; // users positions < 100 mln require rewardToken.balanceOf(e, currentContract) < 100000000000000000000000000; |
Then we tell certora that there’re no vault extensions, some users have already deposited, pending rewards exist (i.e. staking time passed) and sorraStaking can’t be a msg.sender (which makes sense):
|
1 2 3 4 5 6 7 8 |
// no vault extensions require currentContract.vaultExtension(e) == 0; // there already exists some deposit require rewardToken.balanceOf(e, currentContract) == currentContract.positions[e.msg.sender].totalAmount; // pending rewards exist (i.e. some time passed) require getPendingRewards(e, e.msg.sender) > 1; // current contract can't be a sender require e.msg.sender != currentContract; |
Then we setup some helper variables (most of them for ease of debugging in the certora dashboard) and call withdraw() with arbitrary environment and amount variables so that certora could analyze all possible inputs:
|
1 2 3 4 5 6 7 8 9 10 11 |
uint256 contractBalanceBefore = rewardToken.balanceOf(e, currentContract); uint256 userBalanceBefore = rewardToken.balanceOf(e, e.msg.sender); uint256 pendingRewardsBefore = getPendingRewards(e, e.msg.sender); uint256 userDepositedAmountBefore = currentContract.positions[e.msg.sender].totalAmount; withdraw(e, amount); uint256 contractBalanceAfter = rewardToken.balanceOf(e, currentContract); uint256 userBalanceAfter = rewardToken.balanceOf(e, e.msg.sender); uint256 pendingRewardsAfter = getPendingRewards(e, e.msg.sender); uint256 userDepositedAmountAfter = currentContract.positions[e.msg.sender].totalAmount; |
Finally we set the assert statement which must not violate the User must not withdraw more that expected rule. “More than expected” is actually tricky so I ended up comparing the amount to be withdrawn (plus pending rewards) with the actual withdrawn amount (again plus pending rewards). Both values (before and after the withdaw) must be equal, otherwise there’s something wrong:
|
1 2 |
assert (amount + pendingRewardsBefore) == (userBalanceAfter - userBalanceBefore + pendingRewardsAfter), "User can not withdraw more than expected"; |
In the end we get the following certora spec:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 |
using MockERC20 as rewardToken; rule withdrawIntegrity() { env e; uint256 amount; // user's balance < 100 mln require rewardToken.balanceOf(e, e.msg.sender) < 100000000000000000000000000; // withdraw amount < 100 mln require amount < 100000000000000000000000000; // users positions < 100 mln require rewardToken.balanceOf(e, currentContract) < 100000000000000000000000000; // no vault extensions require currentContract.vaultExtension(e) == 0; // there already exists some deposit require rewardToken.balanceOf(e, currentContract) == currentContract.positions[e.msg.sender].totalAmount; // pending rewards exist (i.e. some time passed) require getPendingRewards(e, e.msg.sender) > 1; // current contract can't be a sender require e.msg.sender != currentContract; uint256 contractBalanceBefore = rewardToken.balanceOf(e, currentContract); uint256 userBalanceBefore = rewardToken.balanceOf(e, e.msg.sender); uint256 pendingRewardsBefore = getPendingRewards(e, e.msg.sender); uint256 userDepositedAmountBefore = currentContract.positions[e.msg.sender].totalAmount; withdraw(e, amount); uint256 contractBalanceAfter = rewardToken.balanceOf(e, currentContract); uint256 userBalanceAfter = rewardToken.balanceOf(e, e.msg.sender); uint256 pendingRewardsAfter = getPendingRewards(e, e.msg.sender); uint256 userDepositedAmountAfter = currentContract.positions[e.msg.sender].totalAmount; assert (amount + pendingRewardsBefore) == (userBalanceAfter - userBalanceBefore + pendingRewardsAfter), "User can not withdraw more than expected"; } |
Running Certora Rule
Now, if we run certoraRun test/sorra/certora/sorra.conf we get the following result: https://prover.certora.com/output/8691664/cc74c97e12b844f099814bdf3aa0cd3a/?anonymousKey=955a9dba9a7a4689097f07ffe84bdbd124058e2c
So the counterexample is:
1. User has a balance of 99999999999999999999999999 tokens
2. User has 2 pending rewards before withdraw
3. User withdraws 3751 tokens
4. After withdrawing user has a balance of 100000000000000000000003752 tokens
Now, if we check our assert statement we get the assertion:
|
1 |
3753 == 3754 |
If we dive deeper we see that the pendingRewardsAfter variable is set to 1 in the counterexample while it must be equal to 0 after the withdraw. That pendingRewardsAfter variable is basically the root cause of the rule violation.
Sources
1. Contract: https://github.com/ryzhak/replaying-bugs-with-certora/blob/389f56905cdc6d170e8f2e4808b00d824eb31439/src/sorra/SorraStaking.sol
2. Foundry tests and certora spec: https://github.com/ryzhak/replaying-bugs-with-certora/tree/389f56905cdc6d170e8f2e4808b00d824eb31439/test/sorra
Conclusion
In this tutorial we covered the Sorra Finance hack and proved it with the Certora Prover which is a great tool (although with a steep learning curve) for catching such bugs. That’s all for today, stay safe.