Saving Millions in 2023 with Specification-Guided Fuzzing
Introduction
2022 has been called the “biggest year for hacking on record” by ChainAnalysis, and other recent statistics confirm it: based on the annual report from Immunefi, 134 attacks have caused over $3 billion in total losses in 2022. In this blog post, we will show how OrCa, Veridise’s specification-guided fuzzer, could have been used to avoid two notable hacks of 2022.
What is OrCa?
OrCa is a fuzzer, a type of automated testing tool which discovers bugs by generating and running thousands of (pseudo-) random inputs against a target application. Unlike other Web3 fuzzers, such as Echidna and Foundry, OrCa allows users to write concise but expressive temporal specifications that express properties of a blockchain protocol over time. As discussed in a previous blog post, these temporal specifications are expressed in our [V] specification language. Given a dApp and a [V] property to check, OrCa then looks for inputs (i.e., series of transactions with suitable inputs) that violate the specification. If the protocol is buggy, OrCa will eventually output a counterexample to the specification.
The Hacks
To give a sense of the power of OrCa and specification-guided fuzzing, we will discuss two very different hacks from 2022 and show how OrCa could have been used to prevent them.
XCarnival
XCarnival is an NFT lending platform that got hacked in June 2022 for $3.8 million. Under this protocol, borrowers are allowed to utilize their NFTs as collateral to obtain asset loans. To get a complete picture of the attack, let’s take a closer look at the internals of this protocol.
Inside XCarnival. While interacting with the protocol, users invoke three contracts: XNFT, which implements the NFT management logic, XToken, which implements the lending logic and P2Controller, which enforces the lending validation checks.
A user can add collateral to the protocol by calling one of the functions used for pledging inside the XNFT contract (i.e., pledgeAndBorrow, pledge, pledge721, and pledge1155). Doing so creates a new Order instance for the NFT added as collateral, which can later be referenced using its corresponding orderId.
struct Order {
address pledger;
address collection;
uint256 tokenId;
uint256 nftType;
bool isWithdraw;
}The Order’s field values are important because they are used inside the lending validation checks. For instance, after a user withdraws their collateral by calling the withdrawNFT function from the XNFT contract, the isWithdraw field is set to true. Consequently, this field’s value is critical for validating the borrowing logic; however, we’ll see that a missing check for this field’s value is what facilitated the attack.
Understanding the attack. Below, we can see the implementation of the borrow function. To borrow, a user must provide the orderId corresponding to the collateral, which is further checked for validity inside the borrowInternal function. Even though borrowAllowed and borrowVerify enforce several restrictions for lending, none of them check if the NFT the user is borrowing against has been withdrawn.
function borrow(uint256 orderId, address payable borrower, uint256 borrowAmount) external {
require(msg.sender == borrower || tx.origin == borrower, "borrower is wrong");
accrueInterest();
borrowInternal(orderId, borrower, borrowAmount);
}
function borrowInternal(uint256 orderId, address payable borrower, uint256 borrowAmount) internal nonReentrant {
controller.borrowAllowed(address(this), orderId, borrower, borrowAmount);
...
controller.borrowVerify(orderId, address(this), borrower);
emit Borrow(orderId, borrower, borrowAmount, vars.orderBorrowsNew, vars.totalBorrowsNew);
}Attackers exploited this vulnerability by taking millions of dollars in borrows using orderIds corresponding to withdrawn collateral — with no collateral on the line, they had no incentive to pay back their loans.
How can OrCa deal with this attack? This bug could have been avoided by specifying a fundamental property of lending protocols, which is that a user should not be able to borrow against withdrawn collateral. We can capture the expected behavior of the XCarnival protocol using the following [V] specification:
vars: XNFT nft, XToken xtok
spec: []!finished(xtok.borrow(orderId, _, _), nft.getOrderState(orderId) = OrderState.NORMALWITHDRAW)In plain English, the specification states that a borrow never successfully completes when the corresponding collateral (indicated by orderId) has already been withdrawn (for XCarnival, an orderId corresponding to withdrawn collateral has the “order state” NORMALWITHDRAW).
If we feed OrCa this specification, it produces the following counterexample:
Deployments
%%
1. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys ERC20_0 with constructor(QgFbYwT, DfTaUeT) at address 0xF2E246BB76DF876Cef8b38ae84130F4F55De395b
2. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys SimpleToken_1 with constructor(rPFAULP, DGaATLT, 1) at address 0x2946259E0334f33A064106302415aD3391BeD384
3. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys AddressUpgradeable_2 with constructor() at address 0xDe09E74d4888Bc4e65F589e8c13Bce9F71DdF4c7
4. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys Exponential_3 with constructor() at address 0x51a240271AB8AB9f9a21C82d9a85396b704E164d
5. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys P2ControllerStorage_4 with constructor() at address 0xB9816fC57977D5A786E654c7CF76767be63b966e
6. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys SafeMath_5 with constructor() at address 0x6D411e0A54382eD43F02410Ce1c7a7c122afA6E1
7. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys Address_6 with constructor() at address 0x5CF7F96627F3C9903763d128A1cc5D97556A6b99
8. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys SafeERC20_7 with constructor() at address 0xA3183498b579bd228aa2B62101C40CC1da978F24
9. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys SafeMathUpgradeable_8 with constructor() at address 0x63f58053c9499E1104a6f6c6d2581d6D83067EEB
10. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys ERC20Storage_9 with constructor() at address 0x66a15edcC3b50a663e72F1457FFd49b9AE284dDc
11. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys XTokenStorage_10 with constructor() at address 0x00De48310d77A4d56aa400248b0B1613508f5B73
12. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys XToken_11 with constructor() at address 0xe69a847CD5BC0C9480adA0b339d7F0a8caC2B667
13. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys P2Controller_12 with constructor() at address 0xD30C8839c1145609E564b986F667b273Ddcb8496
14. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys XNFT_13 with constructor() at address 0xD24260C102B5D128cbEFA0F655E5be3c2370677C
15. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys NFT_14 with constructor() at address 0x7758F98C1c487E5653795470eEab6C4698bE541b
16. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys InterestRateModel_15 with constructor() at address 0x510C6297cC30A058F41eb4AF1BFC9953EaD8b577
17. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf deploys Oracle_16 with constructor() at address 0xcbD945E77ADB65651F503723aC322591f3435cC5
%%
Transactions
%%
1. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends P2Controller_12.initialize(0x0000000000000000000000000000000000000000)
2. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends XNFT_13.initialize()
3. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends XToken_11.initialize(1, 0xD30C8839c1145609E564b986F667b273Ddcb8496, 0x510C6297cC30A058F41eb4AF1BFC9953EaD8b577, 0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE, Token, TOK, 100)
4. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends P2Controller_12.setXNFT(0xD24260C102B5D128cbEFA0F655E5be3c2370677C)
5. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends P2Controller_12.setOracle(0xcbD945E77ADB65651F503723aC322591f3435cC5)
6. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends P2Controller_12.addPool(0xe69a847CD5BC0C9480adA0b339d7F0a8caC2B667, 0, 0)
7. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends P2Controller_12.addCollateral(0x7758F98C1c487E5653795470eEab6C4698bE541b, 1000000000000000000, 0, [])
8. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends XToken_11.mint(100) with value 100
9. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends XNFT_13.setCollectionlWhitList(0x7758F98C1c487E5653795470eEab6C4698bE541b, True, 0, 0, 0)
10. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends XNFT_13.setController(0xD30C8839c1145609E564b986F667b273Ddcb8496)
11. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends XNFT_13.pledge721(0x7758F98C1c487E5653795470eEab6C4698bE541b, 113696046406969068659845517905149556298109036848145834250498029495931765144848)
12. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends XNFT_13.withdrawNFT(1)
13. Address 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf sends XToken_11.borrow(1, 0x7E5F4552091A69125d5DfCb7b8C2659029395Bdf, 5)
%%The “Deployments” section comprises a list of contracts that have been deployed, including XNFT, XToken, and P2Controller, and their corresponding deployment addresses. It is followed by the “Transactions” section, which corresponds to the ordered set of transactions that lead to a violation of the specification (i.e., a counterexample).
The most interesting part of the counterexample consists of the last three transactions, as the first 10 transactions correspond to basic contract and environment set-up and are derived from deployment scripts. Here, transaction #11 corresponds to a call to the pledge721 function, which allows the user to add an NFT as collateral. As it was the first NFT added to the protocol, it has an associated orderId equal to 1. Next, transaction #12 shows the user calling withdrawNFT to withdraw the collateral with the orderId equal to 1. And finally, transaction #13 illustrates that the user is able to borrow using the orderId equal to 1, even though the corresponding NFT was previously withdrawn.
Using the counterexample produced by OrCa, developers can reproduce the bug step-by-step and understand its root cause.
SheepFarm
SheepFarm is a blockchain investment game on the BNB chain that was hacked in November 2022. As with any game, there is a registration step the users need to go through in order to play the game. One particular feature of SheepFarm is that freshly registered users get bonus gems as an incentive for joining the game. We’ll see in a second why this feature is relevant for the attack.
Understanding the attack. To register, users have to call the register function from the SheepFarm contract. Even though it is supposed to be called only once during account creation, the attackers exploited a simple mistake in the register function, allowing them to call it multiple times and, therefore, illegally collect bonus gems.
As we can see from the following code, the register function does not update the users’ timestamps (a user that has never registered before has a timestamp equal to 0, but after registration their timestamp should be updated to reflect the time at which they registered); therefore, users can call it arbitrarily many times.
function register(address neighbor) external initialized {
address user = msg.sender;
require(villages[user].timestamp == 0, "just new users");
uint256 gems;
totalVillages++;
if (villages[neighbor].sheeps[0] > 0 && neighbor != manager) {
gems += GEM_BONUS * 2;
} else {
neighbor = manager;
gems += GEM_BONUS;
}
villages[neighbor].neighbors++;
villages[user].neighbor = neighbor;
villages[user].gems += gems;
emit Newbie(msg.sender, gems);
}How did attackers drain the funds? As mentioned previously, freshly registered users get bonus gems. Given the game’s rules, users can eventually convert the gems into funds. The attackers took advantage of the vulnerability in this function by repetitively registering to collect a large amount of bonus gems, converting their gems into funds, and finally withdrawing them by calling the withdrawMoney function from the SheepFarm contract.
OrCa in action. Again, OrCa can come to the rescue for catching a vulnerability like this. In this case, our specification mirrors the intent behind the require statement on line 2 (i.e., require(villages[user].timestamp == 0, …)). However, because [V] enables users to express high-level, temporal specifications, we can express this in [V] without needing to reference the villages data structure or timestamp field as follows:
vars: SheepFarm sf, address addr
spec: []!(finished(sf.register, addr = sender) && X<>finished(sf.register, addr = sender))In plain English, the specification says the following: given an arbitrary user addr, it is never the case that, after a successful registration, the user can eventually register again. Note that this specification avoids referencing the particular data structures / logic used in SheepFarm by taking advantage of temporal operators like always (denoted by “[]”), next (denoted by “X”), and eventually (denoted by “<>”).
Since SheepFarm does not conform to the specification, OrCa finds a violation. Specifically, it produces the following counterexample:
Deployments
%%
1. Address 0xd41c057fd1c78805AAC12B0A94a405c0461A6FBb deploys SheepFarm_0 with constructor() at address 0x83C82edd1605AC37D9065d784fdC000B20e9879d
%%
Transactions
%%
1. Address 0xd41c057fd1c78805AAC12B0A94a405c0461A6FBb sends SheepFarm_0.initialize()
2. Address 0x1efF47bc3a10a45D4B230B5d10E37751FE6AA718 sends SheepFarm_0.register(0x0000000000000000000000000000000000000000)
3. Address 0x1efF47bc3a10a45D4B230B5d10E37751FE6AA718 sends SheepFarm_0.register(0x2B5AD5c4795c026514f8317c7a215E218DcCD6cF)
%%The counterexample illustrates that the same user (address 0x1efF47bc3a10a45D4B230B5d10E37751FE6AA718 in this particular case) can perform consecutive successful calls to the register function. This is clearly a violation of the property discussed above, and the OrCa produced counterexample illustrates exactly how it can be violated.
Conclusion
If we learned one lesson through these examples, it is that even innocuous-looking mistakes can result in not-so-innocuous exploits. Furthermore, not all attacks exploit a common vulnerability like reentrancy. Rather, they are enabled through a logical bug in the protocol. This is exactly why formal specifications and automated analysis tools are crucial for preventing exploits. Beyond its ability to check the code against custom specifications, a key advantage of a tool like OrCa is that it can produce counterexamples that constitute tangible evidence of exploitability!
OrCa will be part of our SaaS platform. Visit this page to learn more about OrCa and SaaS. If today’s blog post didn’t convince you that OrCa can be very useful for securing your DeFi project, there is more to come: In one of our future blog posts, we will show how OrCa can deal with even more intricate hacks!
About Veridise
Veridise is a blockchain security company that provides audits and software analysis tools for all layers of the blockchain ecosystem, including smart contracts, web3 applications, zero-knowledge circuits, and blockchain implementations. Co-founded by a team of formal verification and software security researchers, Veridise provides state-of-the-art tooling for hardening blockchain security. Our clients can work with us in a variety of ways, including hiring us for security audits, using our automated security analysis tools (for testing, static analysis, formal verification), or a combination of these.
If you’re interested in learning more information, please consider following us on social media or visiting our website:
Website | Twitter | Facebook | LinkedIn | Github | Request Audit
