Medjai: Protecting Cairo code from Bugs

In this blog post, we will take you on a tour of how we developed Medjai, a new symbolic execution tool for finding bugs in Cairo programs. We’ll begin our journey with a quick tour by helicopter over Cairo. On the way, we’ll peer out at the grand famous OpenZeppelin and take a look at how one peculiar bug was handled in the ancient forums of GitHub. We will then discuss how Medjai can ensure such a bug is gone, and how Medjai could have helped those developers uncover such a bug in the first place. No grand tale is without its backstory though: we’ll explain how Medjai overcomes the unique hurdles of symbolically executing Cairo programs. While our journey today will be short, fear not! There is much of Medjai to explore, and there shall be more to see another day in another blog post.

Helicopter Tour over Cairo

First on our docket is Cairo. While many languages today allow developers to write and deploy smart contracts, a handful of these languages (including Cairo) are distinct in that they can facilitate the construction of zero-knowledge proofs. Zero-knowledge proofs (ZKPs) allow one party (the “prover”) to prove to another party (the “verifier”) that they know some piece of information without revealing any secret information. This is particularly useful for smart contracts because it allows anyone to verify the validity of some computation without accessing personal information about participants of the computation.

Cairo is the programming language for StarkNet contracts and is the backbone for several important exchanges such as Immutable X, Sorare, and DeversiFi, which handle millions of dollars in assets. When a programmer wishes to deploy their smart contract to StarkNet, they first execute their program and get a proof of validity for their program trace using SHARP: the shared prover for StarkNet. After a separate proof verifier checks the validity of the generated proof, the fact that the program trace is valid is added to StarkNet’s fact registry.

The restrictions on Cairo contracts imposed by both SHARP and the proof verifier force Cairo’s language syntax and semantics to take on a variety of quirks. For example, assertions and assignments are treated almost identically in Cairo. The statement x = y + z could be an assignment to x if y and z are defined, an assignment to z if x and y are defined, or an assertion when all three have set values. The semantics of the statement depend on the state of memory with respect to these three variables. Later on, we’ll discuss a few more quirks of the Cairo language and why they posed a challenge when building Medjai.

Cairo Workflow

To understand how the prover and verifier work over Cairo programs, we will take a look at an example from the Cairo tutorial. Specifically, we will consider the following snippet of code, which computes and outputs the positive square root of 25.

func main{output_ptr : felt*}():
    [ap] = 25; ap++
    %{ memory[ap] = 5 %}
    [ap - 1] = [ap] * [ap]; ap++
    serialize_word([ap-1])
    return ()
end

The code in the curly braces %{ ... }% is a hint. We will discuss hints in more detail later, but for now, just know that they are code that is only executed locally and ignored by the prover (when generating proofs) and verifier.

Now let’s examine how the code is handled from three perspectives: the programmer, the prover, and the verifier. When a programmer writes this code on their own machine, she has the ability to run the code locally and confirm that the program outputs what it expects. For our example, doing so yields the following output (note that the line serialize_word([ap-1]) is performing the output).

Program output:
  5
Number of steps: 9
...

Along with printing the output 5, Cairo also generates a program trace which is called a Cairo PIE (Position Independent Execution). The PIE encodes the step-by-step execution of the program. When the programmer is reasonably confident that her program does what she wants, she can send the PIE to the shared proving service SHARP. At this stage, the prover generates a STARK proof describing this computation and sends the proof to the verifier to get checked. Finally, SHARP sends the programmer back something called a fact hash which they can use to see if their computation was verified.

Job fact: 0xf0f1aa66c31a056b486bee8f7157a07567196960370e63740c6857ac733327e1

Once the verifier receives the proof, it checks to see if all the steps of the proof are correct. Afterwards, it publishes the fact, along with its verification status (valid, invalid), to a fact registry for anyone to see.

Bugs in Cairo Programs

It is important to stress that a verified proof does not mean the actual Cairo program is correct (i.e. bug free). In fact, all it really means is that someone ran the Cairo program with some inputs and obtained an output. Hence, if the program itself has bugs, then people can still exploit those bugs to obtain values not intended by the programmer and get that computation verified. For example, suppose someone implements an ERC20 token in Cairo and their widthdraw method has an arithmetic overflow. Then a malicious user could exploit that overflow, obtain a larger balance, and get it stored on the blockchain. Thus, just like in other domains, it is important that Cairo developers themselves verify that their program does what they intended.

We built Medjai to help Cairo developers ensure that their programs are bug-free. Medjai uses a static analysis technique called symbolic execution to explore all possible executions of a Cairo program and find logical bugs. Specifically, developers can specify their intent as a set of program properties, and Medjai can either prove that those properties always hold, or construct an example where some property is violated.

In the next section of our journey today, we will take a look at a real world example of how Cairo programmers can encode unintended behavior in their programs. We will see how the problem is fixed manually before explaining how symbolic execution works and how Medjai’s symbolic execution engine could have helped these developers.

Starboard Side View: OpenZeppelin and _mint

If you now point your binoculars to the right-hand side, you’ll catch a glimpse of the elegantly-flying OpenZeppelin. In this section of our tour, we will take a look at an old bug in the OpenZeppelin _mint function as an example of how Cairo programmers can encode behavior that is mismatched from the programmer’s intent. The bug is shown below as a snippet from the ERC20.cairo contract.

func _mint{
        syscall_ptr : felt*, 
        pedersen_ptr : HashBuiltin*,
        range_check_ptr
    }(recipient: felt, amount: Uint256):
    alloc_locals
    assert_not_zero(recipient)
    uint256_check(amount)
    let (balance: Uint256) = balances.read(account=recipient)
    let (new_balance: Uint256, _) = uint256_add(balance, amount)
    balances.write(recipient, new_balance)
    let (local supply: Uint256) = total_supply.read()
    let (local new_supply: Uint256, _) = uint256_add(supply, amount)
    total_supply.write(new_supply)
    return ()
end

At a high level, mint adds amount to the user’s balance and the total_supply of currency. Note that it does not check to see whether the addition overflows after/in uint256_add. An overflow in mint is very problematic because a malicious user could call mint with an amount that decreases the supply of the currency (potentially setting total_supply to 0 for example). Eventually, OpenZeppelin developers realized this unintended consequence.

The Fix

Once the bug was made clear, the developers patched the behavior out, as shown below. The fixed version adds checks that ensure no overflow results when computing new_supply.

func _mint{
        syscall_ptr : felt*, 
        pedersen_ptr : HashBuiltin*,
        range_check_ptr
    }(recipient: felt, amount: Uint256):
    alloc_locals
    assert_not_zero(recipient)
    uint256_check(amount)
    let (balance: Uint256) = balances.read(account=recipient)
    let (new_balance: Uint256, is_overflow) = uint256_add(balance, amount)
    assert is_overflow = 0
    balances.write(recipient, new_balance)
    let (local supply: Uint256) = total_supply.read()
    let (local new_supply: Uint256, is_overflow) = uint256_add(supply, amount)
    assert is_overflow = 0
    total_supply.write(new_supply)
    return ()
end

While this bug might not seem particularly interesting at first glance, the discussion between the OpenZeppelin developers on GitHub gives this story a bit more nuance. Of course arithmetic operations can overflow, but checking for overflows requires gas. If developers naively check for overflow on every operation, this cost adds up and the expense difference of executing the contract becomes significant. Additionally, reasoning about when these checks are necessary is not easy. Even for this simple case, understanding how Uint256 and uint256_add are implemented is important for understanding why these checks are needed.

This is exactly where program analysis can help! As we mentioned previously, symbolic execution can reason about all program paths in a symbolic way and cover edge cases that humans have a hard time reasoning about. Hence, symbolic execution can help Cairo developers find vulnerabilities in their code as well as help them gain confidence that a given bug fix is correct.

Later on, we will show how our symbolic execution tool, Medjai, is able to detect this bug and confirm that the fix is correct. For now though, we’ll make a quick pit stop to explain how symbolic execution works at a high level.

A Small Excursion: Symbolic Execution

As part of our sight-seeing adventure, we’ll take a look at how symbolic execution works as a program analysis technique. If you’re not ready for a full scuba-diving excursion through the workings of symbolic execution, don’t worry. Today’s activities will be more akin to snorkeling.

While ordinary program execution performs computations over concrete values from registers or memory, symbolic execution generalizes these computations to operate over symbolic values that represent many possible concrete values. To do so, symbolic execution encodes every program path as a logical formula over these symbolic inputs, thereby constraining the possible values of the output for that program path. Then, checking whether there is a bug in that execution path boils down to querying the satisfiability of a logical formula (typically represented in some first-order logical theory). Furthermore, to get a concrete input that triggers that bug, we can simply query an SMT solver for a satisfying assignment of the resulting logical formula!

As an example, let’s consider how a symbolic execution tool might find bugs in the following Cairo function.

func my_mint(amount : felt):
    alloc_locals
    let MAX_BALANCE = 2 ** 128
    assert_lt(amount, MAX_BALANCE)
    let (balance : felt) = accounts.get_balance(...)
    let (newBalance : felt) = amount + balance
    accounts.set(newBalance)
    VERIFY(newBalance < MAX_BALANCE)
end

This code snippet adds amount to an account’s balance. It also (erroneously) ensures that the balance remains under the maximum balance. The problem here is that the check is only performed on amount, not newBalance. To illustrate how symbolic execution works, we will run through the execution of the mint function with a symbolic input amount. We’ll refer to this value as sym_amount. Now let’s step through the program:

1. The first time sym_amount will be used is in assert_lt(amount, MAX_BALANCE), which effectively halts the program whenever amount >= MAX_BALANCE. Since Medjai should consider both branches (halting and not halting), we continue execution, but add the statement sym_amount < 2 ** 128 to our path condition. Any code we execute after assert_lt(amount, MAX_BALANCE) can assume that this path condition holds.
2. sym_amount is next used in let (newBalance : felt) = amount + balance. Let’s assume that accounts are concrete, and that balance is set to 100. Since we’re symbolically executing this program, the value of newBalance is set to the symbolic value sym_amount + 100.
3. Finally, let’s consider the verification query at the end of the mint function. If we want to verify newBalance < MAX_BALANCE, our symbolic execution determines that we need to verify sym_amount + 100 < 2 ** 128. Moreover, due to the assertion earlier in the code, our path condition allows us to assume that sym_amount < 2 ** 128. Then the query that we can send to a solver would look like ∀a. (a < 2^128 → a + 100 < 2^128), where a represents sym_amount. The solver could then return the counter-example sym_amount = 2 ** 128 - 100.

The counterexamples generated by symbolic execution are particularly useful because they can be used to construct failing inputs. In this example, we can run my_mint(2 ** 128 - 100) and observe that the resulting new balance for the account is in fact too big. Additionally, once we remove the bug, we can be confident in our fix since the SMT solver proves the absence of the old bug (i.e. proves that for any input, newBalance < MAX_BALANCE).

Next, let’s return to our OpenZeppelin overflow bug, this time examining how the developers might handle the situation with Medjai.

Rediscovering the Bug and Verifying the Fix Using Medjai

Once again, let’s examine the bug from the mint function in OpenZeppelin, now through the lens of verification with Medjai.

To symbolically execute mint we only needed to add two lines to tell Medjai the property we want to verify. Here is the instrumented version of the buggy code:

func _mint{
        syscall_ptr : felt*, 
        pedersen_ptr : HashBuiltin*,
        range_check_ptr
    }(recipient: felt, amount: Uint256):
    alloc_locals
    assert_not_zero(recipient)
    uint256_check(amount)
    let (balance: Uint256) = balances.read(account=recipient)
    let (new_balance: Uint256, _) = uint256_add(balance, amount)
    VERIFY(new_balance > balance) # prove balance doesn't overflow
    balances.write(recipient, new_balance)
    let (local supply: Uint256) = total_supply.read()
    let (local new_supply: Uint256, _) = uint256_add(supply, amount)
    VERIFY(new_supply > supply) # prove supply doesn't overflow
    total_supply.write(new_supply)
    return ()
end

We can symbolically execute this function with Medjai by replacing all the argument values and storage variables with symbolic values of the same type. By doing so, Medjai will automatically issue a query to the SMT solver to check the properties at both VERIFY statements.

Results

Rediscovering the Bug: When we ran Medjai on the buggy version of mint, it reported that an overflow was possible and gave a counterexample assigning concrete values for balance, total_supply, and amount that triggered the overflow. Below is the counterexample Medjai generated:

recipient = 0
balance = Uint256(high=0, low=1) // balance = 1
total_supply = Uint256(high=1, low=0) // total supply = 2**128
amount = Uint256(high=2**128-1, low=0) // amount = 2**256 - 2**128

We used this counterexample to generate a concrete test case for _mint and found that if we execute _mint with these values as input, then new_supply indeed overflows during execution and total_supply is set to 0 after calling _mint.

Confirming the fix: Afterwards, we ran Medjai on the fixed version (with the VERIFY statements inserted) and it reported that all the properties we specified were verified, confirming that the fixed version is sufficient to prevent an overflow.

What does all of this mean for our fateful developers? First and foremost, they can be confident that their fix correctly removed the overflow bug. But perhaps even more satisfyingly, Medjai was able to show that checking for overflows is necessary for the correctness of the mint function. This means that removing the checks to reduce the execution cost of mint would in fact lead to incorrect behavior.

A Treacherous Hike: Supporting Cairo’s Unique Features

Ah, where did all of you park again? Oh that seems a bit far… While we hike over there, I might as well tell you about a few of the interesting features of Cairo that Medjai supports. There are two features in particular that we have time for today: hints and prime field arithmetic.

Hints

Recall our discussion before about zero-knowledge programming, and the distinction between the prover — which executes the code concretely and generates a proof of any transactions — and the verifier — which simply verifies that the proof is correct. Intuitively, the verifier needs much less information than the prover. For example, to compute the square root of a positive number n, the prover must actually find a number sqrt(n), while the verifier needs only confirm that sqrt(n) * sqrt(n) = n.

For this reason, while Cairo forces programs to construct a zero-knowledge proof, the language also allows hints in the form of Python code that can be executed exclusively by the prover. To make our previous example concrete, let’s look at the following function from the Cairo playground which computes the square root of a positive integer:

func sqrt(n) -> (res):
    alloc_locals
    local res
    # Set the value of res using a python hint.
    %{
        import math
        # Use the ids variable to access the value of a Cairo variable.
        ids.res = int(math.sqrt(ids.n))
    %}
    # From the verifier's point of view, the hint is completely transparent.
    # The following line guarantees that `res` is the square root
    # (either the positive or negative) of `n`.
    assert n = res * res
    return (res=res)

Medjai handles hints in two different modes: ambivalent and modeling. In ambivalent mode, Medjai treats the hint as an unknown function that edits some particular memory locations and stores symbolic values to those locations. If Medjai is able to verify that the program is bug-free in ambivalent mode, then any actual hint implementation will not introduce bugs (with respect to the VERIFY statements). If this verification step fails, Medjai switches to modeling mode, where it uses a model of each hint block for symbolic execution. Each model is a function that tells Medjai how the relevant hint block should affect the symbolic state of the program. If Medjai fails to verify the program in this mode, it reports the bug to the developer; otherwise, Medjai recommends adding assertions to the Cairo program so that changes in the hint code don’t cause future bugs.

Prime Field Arithmetic

Unlike traditional imperative programming languages, Cairo has no built-in support for bitwise arithmetic — its only primitive integer type is a felt, an element in a prime field. Therefore, Cairo instead represents Uint256 as a struct containing two felt elements. In simple terms, felt is an unsigned integer in the range [0, P) for some pre-defined prime P. This can lead to some unintuitive behaviors when performing arithmetic, such as division acting differently than traditional integer division. For example, in the prime field, 1 / 2 = (P + 1) / 2.

No special tricks are necessary to support felts, but just like the Cairo interpreter itself, Medjai needs to perform all arithmetic modulo P. Additionally, handling bit manipulations of symbolic field elements is difficult for SMT solvers to handle because (1) they need 252 bits to represent and (2) the bounds of [0, P) add complexity to the constraints. For this reason, Medjai must transform bit manipulations like shifts into equivalent arithmetic like multiplication and division.

Both hints and prime field arithmetic are particularly important for Medjai to support because they can be sources of subtle but impactful bugs in Cairo programs. In the future, we hope to highlight some examples of these unique bugs, as well as other features of Cairo that make developing Medjai challenging and interesting.

A Postcard of Parting Thoughts

That’s all from us today. If anything, we hope that you take away these main points: First, as Cairo and other zero-knowledge languages continue to grow in popularity, supporting these languages with proper tools for bug finding and verification will also become more important. Second, our symbolic execution tool, Medjai, can help Cairo developers catch subtle bugs in their code and gain confidence that their fix is correct.

We hope you’ve had fun exploring Medjai with us. To find about more about our tool, check out Medjai on GitHub here. If you’ve enjoyed your trip today, my name is either Jacob, Shankara, or Yanju. If not, my name is Jon or Ben. Either way, from all of us at Veridise, we hope you’ll join us again soon for another adventure exploring more of Cairo with Medjai!

About Veridise

Veridise offers thorough and comprehensive security audits for blockchain applications. Leveraging our expertise in automated program analysis, Veridise provides state-of-the-art solutions for ensuring security of decentralized finance applications. If you’re interested in learning more information, please consider following us on social media or visiting our website:

Website | Twitter | Facebook | LinkedIn | Github