Underconstrained output in felt_to_bytes_little() allows contract deployments to incorrect addresses

[c4-bot-10]

Lines of code

https://github.com/kkrt-labs/kakarot/blob/7411a5520e8a00be6f5243a50c160e66ad285563/src/utils/bytes.cairo#L80

Vulnerability details

To explain this finding, we compare two utility functions that are very similar in their implementation: load_bytecode() in kakarot/src/kakarot/accounts/library.cairo and felt_to_bytes_little() in kakarot/src/utils/bytes.cairo. Both contain logic for un-packing up to 31 bytes from a felt into an array of single bytes.

If we isolate only the few interesting lines of the inner loop in load_bytecode(), we have the following:

File: library.cairo
531:         tempvar count = BYTES_PER_FELT;
---
541:         body:
---
576:         tempvar value = (value - [output]) / base;
---
582:         tempvar count = count - 1;
---
593:         jmp body if count != 0;
---
594:         with_attr error_message("Value is not empty") {
595:             assert value = 0;
596:         }

The loop starts with count = BYTES_PER_FELT (which is 31), then at every cycle count is decreased by 1, and when it reaches the value 0, the loop ends, finally asserting that value = 0.

This correctly ensures the [output] values provided by the prover are honest, because if [output] wasn't effectively containing the last byte of value, the field division at L576 would have increased value (instead of decreasing it) to a value that couldn't be brought down to 0 with at most 31 iterations of chopping off the least significant byte.

To summarize, load_bytecode is safe because:

1. [output] is checked to be between 0-255 values (code omitted for brevity)
2. no more than 31 iterations are allowed
3. value is checked to be 0 at the end of the loop.

Now, we compare this to the corresponding loop in felt_to_bytes_little():

File: bytes.cairo
57:     body:
---
70:     let byte = [output];
---
74:     tempvar value = (value - byte) / base;
---
78:     tempvar bytes_len = bytes_len + 1;
---
80:     jmp body if value != 0;

This time, the terminating condition is value = 0, where value is the input felt after the iterative field divisions. Also in this case, value can not only shrink, but also grow larger at L74 if the [output] provided by the prover is not honest.

If we compare with the three conditions that make load_bytecode safe, we see that the second condition 2. no more than 31 iterations are allowed does not hold in this case, so the prover is effectively allowed to provide an arbitrary number of bytes, as long as these are followed by more bytes that bring value back to zero.

In other words, the lack of check that bytes_len is at most 31 leaves space for the prover to provide arbitrary bytes in output, making the load_bytecode function under-constrained and un-sound.

For an exploit to happen, however, bytes_len cannot be purely arbitrary, because this value serves as a lookup index into the pow256_address table to enforce this other constraint:

File: bytes.cairo
091:         let lower_bound_ = pow256_address[bytes_len - 1];
---
098:     let upper_bound = pow256_address[bytes_len];
099:     with_attr error_message("bytes_len is not the minimal possible") {
100:         assert_le_felt(lower_bound, initial_value);
101:         assert_le_felt(initial_value, upper_bound - 1);
102:     }

This is, however, not a strong requirement, because the pow256_address can be looked up out-of-bounds (as proven in the below PoC), effectively looking up values from portions of the bytecode that have a different purpose.

Within Kakarot, the felt_to_bytes_little function is used to calculate addresses of contract creation with all methods (CREATE, CREATE2, and EOA transactions without to). While the CREATE2 path is not exploitable for external constraints (most notably a memset call exploding in gas consumption in case of an exploit), the other methods are vulnerable. A malicious prover can therefore artificially alter the address created from EOAs and from contracts using the CREATE opcode.

This can cause users loss of funds because they may create and fund a contract, but the contract may end up being deployed at a different address, causing the provided funds to be permanently locked. While users may be on the guard for this address change to happen with contracts created via the CREATE opcode (that is notably vulnerable in case of block reorgs), this would certainly be a behavior that can't be predicted in case of creation from EOA where the caller has direct control over the nonces.

Proof of Concept

The below test patches the felt_to_bytes_little prover hint to show how malicious data can be passed via arbitrary execution and still meet all the assert statements coded:

def test_does_not_raise_when_byte_value_not_correct(
	self, cairo_program, cairo_run
):
	with (
		patch_hint(
			cairo_program,
			"memory[ids.output] = res = (int(ids.value) % PRIME) % ids.base\nassert res < ids.bound, f'split_int(): Limb {res} is out of range.'",
			"memory[ids.output] = 2 if ids.bytes_len < 3 else (int(ids.value) % PRIME) % ids.base\nprint(f'[DEBUG] Byte value: {memory[ids.output]}')",
		)
	):
		cairo_run("test__felt_to_bytes_little", n=3)

In particular, with value = 3, while an honest prover would provide output = [ 3 ], the test demonstrates how a malicious prover can provide the following output consisting of 34 bytes:

Recommended Mitigation Steps

Consider adding an additional constraint to felt_to_bytes_little for the final value of bytes_len not to exceed 31.

Assessed type

Other

[ClementWalter]

Severity: High

Comment: Ok
dup 118, dup QA #126

[c4-judge]

dmvt marked the issue as satisfactory

[c4-judge]

dmvt marked issue #118 as primary and marked this issue as a duplicate of 118