Under-constrained computation, a new kind of bug
Learn how provers can exploit under-constrained Cairo programs!
Introduction
Cairo is a programming language for building zero-knowledge programs. These programs allow you to prove the result of a computation without asking other people to re-run the computation.
Proofs of correct computation are awesome! Let’s assume you have a Cairo program to compute all prime numbers up to 1,000. When you run Cairo, you’ll get both the prime numbers and proof that those prime numbers are the result of running the program. If you give the numbers and proof to someoneone else they can be 100% sure that you’ve given them all the primes up to 1,000 without having to also compute those prime numbers; all they need to do is check the proof!
This technology is at the core of zk-rollups. Cairo itself is the programming language used for StarkNet!
Cairo is a bit different from other (imperative) programming languages. This article will explore an interesting new type of bug that can happen in under-constrained, zero-knowledge programs.
Background
Let’s take a step back and look at Cairo as a language.
Cairo separates the perspective of the computer (prover) from the result user (verifier). Because of this, Cairo’s primary goal is not to describe how to compute something, but to describe valid computations.
Let’s explore that idea using an ERC20 transfer example:
In imperative programming languages like Solidity, you’d write something roughly equivalent to: “Take my balance and remove x from it, then take the recipient balance and add x to it.” However, in Cairo you’d write: “You can increase someone’s balance by however much you like, if you decrease your own balance by the same amount.”
In Cairo programs, you write what results are acceptable, not how to come up with results.
Constraining
by Joshua Hoehne on Unsplash
You end up with programs that might be non-deterministic when you write code that describes acceptable results.
Take the following code for example. The function example() can return any number up to and including 10. It’s totally up to the prover to pick one.
func example() -> felt:
alloc_locals
// Here we create a variable x. Unlike solidity which would initialize x at 0, it's up to the prover to choose a value for x
local x
// Here we add an assertion which says that the program should only "accept" computations where x <= 10.
// It's impossible to create a proof for a computation where this condition isn't satisfied.
assert_le(a=x, b=10)
return x
end
It’s like speed limits: the road sign gives you the limit, but ultimately you choose your speed. Officer Cairo :cop: won’t allow you to break the rules .
The following is an example from Hints — Cairo documentation:
// set (constrain) memory location at ap to 25 and increment ap
[ap] = 25; ap++
// constrain the memory location at ap to be the root of memory location at ap - 1 (25)
[ap - 1] = [ap] * [ap]; ap++
In this example, the authors first say that a memory location must be equal to 25. Then they say that the following memory location, when squared, must be equal to it.
There are two possible values for this following location in memory -5 and +5, and the prover gets to pick!
Hints
But how does the prover choose the values?
That’s where hints come into play!
Hints are snippets of Python code that help the prover determine the value for variables that can have multiple values.
For example, we can add %{ ids.x = 1 %} after local x in the first example, which will suggest to the prover pick 1 for the value of x.
A valid set of inputs (and the unique execution trace that will be followed with those inputs) is called a valid witness.
Hints are only suggestions though! A prover can decide to choose any value as long as it satisfies the rules described in the Cairo program. The prover will be unable to produce a proof if the Cairo constrains are not satisfied!
Real world example
Hints can be handy! Take the following code from the Cairo standard library:
func find_element{range_check_ptr}(array_ptr : felt*, elm_size, n_elms, key) -> (elm_ptr : felt*):
alloc_locals
local index
%{
# Some python code to find an index where array[index] == value
%}
assert_nn_le(a=index, b=n_elms - 1)
tempvar elm_ptr = array_ptr + elm_size * index
assert [elm_ptr] = key
return (elm_ptr=elm_ptr)
end
All of the complex (and expensive) logic has been moved into a hint. All that’s left is code that ensures the resulting index points to the sought after value in the array! This results in a much smaller proof.
Under-constrained
To summarise:
Cairo -> Describe what’s okay. Hint -> Describe how to come up with something that’s okay.
Now let’s review potential bugs.
If there is a bug in one of the hints, it will be detected by the Cairo code; since buggy hints won’t always produce acceptable results!
What if the hint is correct, but the Cairo code is not? What if it allows too much? There won’t be a problem executing the code because the bug-free hint will provide desirable results.
But what if someone else runs the code? They don’t have to use your hint! Instead, a malicious prover might trick the program into using the wrong values, resulting in an undesirable execution!
Take the find_element() function above. Let’s assume the developer forgot to add the following line, which asserts the key points to the returned element pointer.
assert [elm_ptr] = key
Now, everything would still work and the unit tests would indicate everything is still working as it should.
However, everything is not okay! A prover can decide to return any arbitrary element in the list. This can easily trigger adverse effects in the code that depend on this function to produce the right element pointer!
The problem occurs in the situation where an untrusted actor executes the code and constructs a proof. The actor can, but doesn’t have to follow the advice of the hint that suggests the right index. Instead, the prover can choose for the function to return an arbitrary element in the array.
The attacker could further exploit this to trigger unwanted behaviours in other parts of your Cairo code.
Conclusion
Luckily you don’t need to worry much about this type of bug when you’re just developing StarkNet contracts. As only a few trusted standard library are allowed to use non-deterministic code and hints.
However, if you’re writing Cairo code, you’ll have to make sure that you sufficiently constrain the output of your hints.
As a rule of 👍: don’t assume that the prover uses your hints and add sufficient assertions to ensure that provable executions are correct regardless.
Thinking about smart contract security? We can provide training, ongoing advice, and smart contract auditing. Contact us.