Underconstrained hints in initailize_jumpdests, risk of manipulation of valid_jumpdests

[c4-bot-4]

Lines of code

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

Vulnerability details

Proof of Concept

In a deployment tx, initialize_jumpdests will be called in interpreter::execute flow. It loops through the bytecode byte by byte and writes to jumpdests dictionary. (dict_write{dict_ptr=valid_jumpdests}(i, TRUE))

To determine whether to exit the loop, it compares the iterator(byte index) next_i and bytecode length (bytecode_len). It only exits the loop when next_i >= bytecode_len. (0<= tempvar a = next_i - bytecode_len < range_check_builtin.bound)

The issue is the checking of next_i - bytecode_len is done in hint, but the hint result memory[ap] is never checked to be correct. As a result, a malicious prover can assign any value as continue_loop. For example, a malicious prover assigns 1 to continue_loop after the next_i equals bytecode_len, which keeps the loop running longer while increasing next_i to read unsafe memory location after bytecode.

//kakarot/src/utils/utils.cairo

    func initialize_jumpdests{range_check_ptr}(bytecode_len: felt, bytecode: felt*) -> (
        valid_jumpdests_start: DictAccess*, valid_jumpdests: DictAccess*
    ) {
...
        body:
        let bytecode_len = [fp - 4];
        let bytecode = cast([fp - 3], felt*);
        let range_check_ptr = [ap - 3];
        let valid_jumpdests = cast([ap - 2], DictAccess*);
        let i = [ap - 1];

        tempvar opcode = [bytecode + i];
        let is_opcode_ge_0x5f = Helpers.is_le_unchecked(0x5f, opcode);
        let is_opcode_le_0x7f = Helpers.is_le_unchecked(opcode, 0x7f);
        let is_push_opcode = is_opcode_ge_0x5f * is_opcode_le_0x7f;
        let next_i = i + 1 + is_push_opcode * (opcode - 0x5f);  // 0x5f is the first PUSHN opcode, opcode - 0x5f is the number of arguments.

        if (opcode == 0x5b) {
            dict_write{dict_ptr=valid_jumpdests}(i, TRUE);
            tempvar valid_jumpdests = valid_jumpdests;
            tempvar next_i = next_i;
            tempvar range_check_ptr = range_check_ptr;
        } else {
            tempvar valid_jumpdests = valid_jumpdests;
            tempvar next_i = next_i;
            tempvar range_check_ptr = range_check_ptr;
        }

        // continue_loop != 0 => next_i - bytecode_len < 0 <=> next_i < bytecode_len
        tempvar a = next_i - bytecode_len;
        //@audit hint is used to check whether tempvar a is in range, and assign the result to [ap]. but there is no check on the assigned result after the hint. `continute_loop` value can be manipulated. 
  |>    %{ memory[ap] = 0 if 0 <= (ids.a % PRIME) < range_check_builtin.bound else 1 %}
        ap += 1;
  |>    let continue_loop = [ap - 1];
        tempvar range_check_ptr = range_check_ptr;
        tempvar valid_jumpdests = valid_jumpdests;
        tempvar i = next_i;
        static_assert range_check_ptr == [ap - 3];
        static_assert valid_jumpdests == [ap - 2];
        static_assert i == [ap - 1];
        jmp body if continue_loop != 0;

        end:
        let range_check_ptr = [ap - 3];
        let i = [ap - 1];
        // Verify that i >= bytecode_len to ensure loop terminated correctly.
        let check = Helpers.is_le_unchecked(bytecode_len, i);
        //@audit note that if a malicious prover assigns 1 to `continue_loop` to allow the loop to run after `i` exceeds `bytecode_len`, assert check = 1 will still pass. Because it only checks whether bytecode_len <= i. This allow i to read unsafe memory slots.
  |>    assert check = 1;
        return (valid_jumpdests_start, valid_jumpdests);
    }
...

(https://github.com/kkrt-labs/kakarot/blob/7411a5520e8a00be6f5243a50c160e66ad285563/src/utils/utils.cairo#L922-L925)

As seen above, in the end section, it verifies loop termination by checking whether bytecode_len <= i. This is also insufficient considering a malicious prover can extend the loop resulting bytecode_len < i and reading unsafe memory regions while still passing the check.

POC:

1. A malicious prover input 1 to memory[ap] when the next_i == bytecode_len
2. loop will continue to access byte next_i of bytecode, which exceeds the scope of bytecode [0, bytocde_len). In the new loop, the memory slot following bytecode will be interpreted as an opcode.
3. The malicious prover can repeat the above to continue the loop. Potentially reading a value that matches the condition to keep writing to the dictionary.

Recommended Mitigation Steps

Consider adding check after the hint to ensure when continue_loop !=0 , (bytecode_len - 1 - next_i) is in range and when continue_loop == 0, (next_i - bytecode_len) is in range.

Assessed type

Other

[ClementWalter]

Severity: Informative

Comment: There are no alteration of the logic or the specs. The prover can charge arbitrary amount for this kind of tx. But this is a centralisation risks with external dependencies (assuming the prover is malicious)

[c4-judge]

dmvt changed the severity to QA (Quality Assurance)