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.

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.

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:

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:

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.

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:

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:

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!