fix: issues found by Diligence

[felicityin]

Fix issues found by Diligence: https://tintinweb.github.io/minr/#/p/ProjectZKM/Ziren/88e0521b82d3ed4c28005fbe220066c8ec76b31a

[felicityin]

Issue 009

op_a_value is unconstrained when op_a_0 = 1, enabling forged branch direction (control-flow hijack).

The bug is that Ziren keeps two versions of operand A:

• op_a_access.value(): the value actually read from or written to the register file.
• op_a_value: the logical operand sent to instruction chips like Branch and TEQ.

When op_a is register $zero, the CPU AIR forced only op_a_access.value() to be zero. It did not also force op_a_value to zero for read-source instructions.

That left op_a_value free whenever an instruction read $zero as operand A. Branch instructions and TEQ consume this free op_a_value, so a malicious prover could fake comparisons involving $zero.

Example: beq $0, $0, label should always branch. But the prover could keep the real register access value as 0 while setting the free op_a_value to 1, making the branch chip believe the operands are unequal and accept a fallthrough path.

So this is a soundness bug: the verifier could accept a proof of an execution path that does not match real MIPS semantics.

Fix

Add a CPU AIR constraint for the vulnerable case:

builder
    .when(local.instruction.op_a_0 * local.op_a_immutable)
    .assert_word_zero(local.op_a_value);

This binds the free instruction-tuple operand op_a_value to zero when op_a is $zero and the instruction treats A as an immutable read source, covering branches, stores, and TEQ. It deliberately does not constrain ordinary writes to $zero, where a nonzero computed result is allowed to be discarded.

[felicityin]

Issue 213

Critical — Branch/Jump delay-slot target (next_next_pc) is not carried across shard boundaries, allowing control-flow forgery

MIPS branches and jumps use a delay slot, so Ziren tracks:

pc
next_pc
next_next_pc

For a jump at B to target T:

pc = B
next_pc = B + 4 // delay slot
next_next_pc = T // post-delay-slot target

Inside one shard, next_next_pc is correctly propagated to the delay-slot row. But across shard boundaries, public values only carry next_pc, not next_next_pc.

So a malicious prover could end a shard on a branch/jump row. The shard exports only B + 4, the delay-slot address. The next shard starts at B + 4 and re-derives next_pc = B + 8, silently dropping the true target T.

Result: a taken branch or unconditional jump can be forged as fallthrough, letting the prover create an execution trace that violates the real program control flow while still verifying.

Fix

Add verifier-side AIR constraints that forbid a shard from ending on a branch or jump row:

  builder
      .when_transition()
      .when(local.is_real - next.is_real)
      .assert_one(local.is_sequential + local.is_halt);

  builder
      .when_last_row()
      .when(local.is_real)
      .assert_one(local.is_sequential + local.is_halt);

Why this fixes it: branch/jump rows are real, non-halt, non-sequential rows. They carry the post-delay-slot target in next_next_pc, but shard public values only export next_pc. By requiring the last real CPU row to be either sequential or halt, the AIR now enforces the executor’s intended invariant that branch/jump and their delay slot cannot be split across a shard boundary. That prevents next_next_pc from being dropped.

[felicityin]

Issue 016

High - syscall/precompiles/u256x2048_mul/air.rs - U256x2048Mul lo_ptr/hi_ptr constrained only via reduce()

The chip reads lo_ptr and hi_ptr from memory, then constrains them only by comparing against:

lo_ptr_memory.value().reduce()
hi_ptr_memory.value().reduce()

But reduce() maps a 32-bit word into the KoalaBear field, whose modulus is smaller than 2^32. So two different 32-bit words can reduce to the same field element.

Because lo_ptr and hi_ptr are later used as base addresses for output memory writes, a non-canonical pointer word could collide with another address after reduction. That lets the proof write the multiplication result to a different memory address than the raw pointer word represents.

The fix is to range-check the raw pointer words with KoalaBearWordRangeChecker before reducing them, making the reduction injective for those values.

Fix

Add local KoalaBearWordRangeChecker columns for both pointer reads:

pub lo_ptr_range_checker: KoalaBearWordRangeChecker<T>,
pub hi_ptr_range_checker: KoalaBearWordRangeChecker<T>,

Trace generation now populates them from the raw memory-read pointer words, and the AIR range-checks both values before the existing reduce() binding:

KoalaBearWordRangeChecker::<AB::F>::range_check(
  builder,
  *local.lo_ptr_memory.value(),
  local.lo_ptr_range_checker,
  local.is_real.into(),
);

Same for hi_ptr_memory. This makes the pointer word canonical before reduction, so lo_ptr_memory.value().reduce() and hi_ptr_memory.value().reduce() cannot collide with a different 32-bit word.

[felicityin]

Issue 020

MULT/MULTU HI-register write is skippable, forging the value read by MFHI.

The MUL chip allowed real MULT/MULTU instructions to skip writing the MIPS HI register.

The HI write was gated by hi_record_is_real, but that column was not forced to be 1 for hardware MULT/MULTU rows. A malicious prover could set it to 0, causing the product high word to be computed but not written to register 33.

Then a later MFHI would read the old/stale HI value instead of the true multiply high word. This lets the prover forge computations that depend on 64-bit multiplication results, while still satisfying the memory argument because the skipped write simply never enters the memory multiset.

Fix

Add a MUL AIR constraint that forces hardware MULT/MULTU rows to write HI, while preserving dependency-only multiply rows used by DivRem and MADD/MSUB:

builder.when(local.is_mult + local.is_multu).assert_zero(
(local.pc - AB::Expr::from_canonical_u32(UNUSED_PC))
    * (AB::Expr::one() - local.hi_record_is_real),
);

Meaning:

• If the row is MULT/MULTU
• and pc != UNUSED_PC meaning it is a real program instruction row
• then hi_record_is_real must be 1

Delegated multiply rows use pc = UNUSED_PC, so they can still keep hi_record_is_real = 0 and avoid writing register 33.

This closes the attack because a real MULT/MULTU row can no longer match a MUL-chip row that skips the HI memory write. Since hi_record_is_real is also the is_check_memory slot in the instruction tuple, this also forces the CPU side to send the real shard/clk for hardware multiplies.

[felicityin]

Issue 036

Medium - Verifier trusts proof-supplied chip_ordering indices without bounds validation.

The shard proof contains a prover-supplied chip_ordering map from chip name to opened-values index.

The verifier used this map directly to index opened_values.chips and order the chip list, but did not validate that the indices were in bounds, unique, or a valid 0..n permutation.

A malicious proof could therefore provide malformed ordering metadata, causing verifier panics through out-of-bounds indexing, or making multiple chips reuse the same opened values. That can misalign chip constraints with the data being opened.

The fix is to validate chip_ordering before use and reject malformed proofs with a verification error instead of trusting the prover-supplied map.

Fix

Fixed the native shard verifier path.

• Added InvalidChipOrdering(String) verification error.

• Validates prover-supplied chip_ordering before use:

  • length matches opened chip values
  • all chip names are known/expected
  • every index is in bounds
  • indices are unique
  • indices form a contiguous 0..n range
  • required preprocessed chip names are present

• Calls validation before shard_chips_ordered in StarkMachine::verify.

• Also validates inside Verifier::verify_shard to protect direct callers.

[felicityin]

Issue 037

INS instruction integer underflow when msb < lsb.

The execute_ins function in the executor computes msb - lsb + 1 without checking that msb >= lsb. When a malicious guest program encodes an INS instruction where msb < lsb (which is architecturally undefined in MIPS), the subtraction msb - lsb underflows as a u32, producing a very large value. This causes a subsequent 1u32 << (msb - lsb + 1) to either panic in debug mode or produce undefined behavior (shift by >= 32 bits is undefined in Rust's wrapping semantics for << with u32).

The AIR constraints for INS (in misc/others/air.rs) do include a range check lsb <= msb via ByteOpcode::LTU lookup (lsb < msb + 1), but this constraint only validates the trace during proof verification. An honest executor encountering such an instruction will panic before generating a valid trace, constituting a prover denial-of-service.

A malicious guest program can craft an INS instruction with msb < lsb to crash the prover.

Fix

execute_ins now validates msb >= lsb before computing the bit-width mask. If the encoding is invalid, it returns ExecutionError::ExceptionOrTrap() instead of underflowing msb - lsb and panicking. The INS dispatch path now propagates that Result with ?.

[felicityin]

Issue 038

Reachable unimplemented!() panic in ecrecover hook on guest-controlled curve ID.

The hook_ecrecover function in hook.rs contains an unimplemented!() macro call at line 133 that is reachable through guest-controlled input. The curve ID is extracted from the first byte of the guest-supplied buffer (buf[0] & 0b0111_1111), and only values 1 (secp256k1) and 2 (secp256r1) are handled. Any other value (0, 3-127) triggers unimplemented!(), which panics and crashes the prover process.

Hooks are invoked during execution via the WRITE syscall to specific file descriptors. Since the guest program controls the data written, a malicious guest can write a buffer with any curve ID to the FD_ECRECOVER_HOOK file descriptor, triggering the panic.

The hook return values are used as "hints" and are not directly constrained by the AIR -- the precompile circuit re-verifies the computation. However, the panic occurs before any return value is produced, so it is a pure DoS vector against the prover.

Fix

I replaced the reachable unimplemented!() in crates/core/executor/src/hook.rs:118 with a proper error return:

• unsupported curve_id now returns Err(ExecutionError::UnsupportedEcrecoverCurveId(curve_id))

I also added the new executor error variant in crates/core/executor/src/executor.rs:193 so the failure is explicit and non-panicking.

[felicityin]

Issue 039

EXT instruction shift underflow when msbd + lsb > 31.

The execute_ext function in the executor and the corresponding emit_misc_dependencies function compute 31 - lsb - msbd to generate the SLL shift amount. When msbd + lsb > 31 (which is architecturally undefined per the MIPS spec), this subtraction underflows as u32, producing a huge shift amount. This causes incorrect trace generation or a panic.

The AIR constraints for EXT (misc/others/air.rs lines 402-416) verify lsb + msbd < 32 via a ByteOpcode::LTU byte lookup, but this validation occurs only during proof verification. The executor will panic during trace generation on architecturally undefined instruction encodings.

Both the executor (execute_ext at line 1778-1779) and the dependency emitter (emit_misc_dependencies at line 291) perform 31 - lsb - msbd without validating the precondition, making them both vulnerable.

Fix

Add an explicit check in execute_ext to return an ExecutionError when msbd + lsb >= 32, consistent with the AIR constraint.

• executor.rs — execute_ext now returns Result<_, ExecutionError> and returns ExceptionOrTrap when msbd + lsb >= 32, mirroring the existing execute_ins guard. Call site updated with ?.
• dependencies.rs — added a debug_assert!(lsb + msbd < 32) in the EXT branch documenting the invariant the executor now guarantees.
• ext_executor_edge_cases.rs (new) — regression test confirming the undefined encoding traps instead of panicking.

Because the guard fires during execution (before event emission), it also protects the identical subtraction in emit_misc_dependencies and trace generation — the same pattern the existing INS guard uses.

[felicityin]

Issue 040

Division-by-zero AIR constraint forces quotient=0xFFFFFFFF but executor rejects div-by-zero.

Executor/AIR divergence on division by zero. The executor traps on c == 0 for DIV/DIVU/MOD/MODU (execute_alu, executor.rs:1877-1881), but the DivRem AIR accepted div-by-zero rows by forcing quotient = 0xFFFFFFFF and skipping the remainder range check. A malicious prover could thus submit a valid div-by-zero trace that the honest executor would never produce — a path to inject controlled quotient/remainder values into the trace.

Fix

Make the AIR reject division by zero, matching the executor. The existing IsZeroWordOperation already constrains is_c_0.result == (c == 0); I replaced the quotient-forcing block with:

// c must be non-zero on every real divrem row.
builder.when(is_real.clone()).assert_zero(local.is_c_0.result);

This proves c != 0 on every real divrem row, so any trace containing a div-by-zero event is now rejected. Also updated the module doc comment.

[felicityin]

Issue 041

No Independent Range Checking on Bridge Chip Columns.

The MemoryLocalChip is the critical bridge between within-shard memory operations (local Memory lookups from eval_memory_access) and cross-shard memory state (global bus connecting Init/Finalize chips). Despite being foundational to memory soundness, its AIR constraints consist exclusively of four lookup send/receive operations with zero structural constraints on any of its 21 witness columns per entry.

Specifically, the following columns are entirely unconstrained beyond lookup matching:

• addr (memory address) - no range check, no KoalaBear modulus bound
• initial_shard, final_shard - no range check against 24-bit bound
• initial_clk, final_clk - no range check against 24-bit bound
• initial_value[0..3], final_value[0..3] - no byte range check (values should be in [0, 255])

The system relies entirely on transitive constraint propagation: the MemoryGlobalInit chip range-checks values via 32 boolean bits, and this propagates through the lookup chain. However, this creates a fragile dependency where any implementation bug in the logUp/grand-product argument could allow arbitrary field elements to flow through the memory system undetected.

This stands in sharp contrast with the MemoryGlobalChip, which independently:

• Range-checks addr via KoalaBearBitDecomposition
• Constrains value via 32 boolean bit decompositions
• Enforces address ordering via AssertLtColsBits
• Constrains timestamp = 1 for Initialize mode

Fix

Add defense-in-depth constraints within the MemoryLocalChip AIR:

1. Byte range check all 8 value fields (initial_value[0..3] and final_value[0..3]) via byte lookup table
2. Range check addr to be a valid KoalaBear field element (< 0x7F000001)
3. initial_shard, final_shard to be within 16 bits
4. Range check initial_clk, final_clk to be within 24 bits, consistent with the eval_memory_access_timestamp assumption

[felicityin]

Issue 042

Memory Value Bytes Never Range-Checked Within Memory Subsystem.

Throughout the entire memory subsystem (instruction chip, consistency columns, local chip, and eval_memory_access), the 4-byte Word values representing memory contents are never independently verified to be valid bytes (in the range [0, 255]). The memory subsystem trusts that all values entering through the lookup argument are correctly constrained by upstream chips.

The memory value flow works as follows:

1. MemoryGlobalInit creates initial values from 32 boolean bits (range-checked to [0, 255]) and sends them to the global bus
2. MemoryLocalChip bridges global and local bus without any range checking
3. eval_memory_access in air/memory.rs sends/receives memory values through the local Memory lookup without any byte range checking (lines 40-61)
4. The memory instruction chip constructs new values for stores (SB/SH/SW/SWL/SWR/SC) from op_a_value and prev_mem_val, neither of which are byte-range-checked within the memory instruction chip

The memory instruction chip DOES perform a KoalaBearWordRangeChecker on addr_word (ensuring the address is < p), and performs byte range checks on addr_word[1..3] via slice_range_check_u8. But no similar range checking exists for the memory VALUE words.

For reads (LB/LBU/LH/LHU/LW/LWL/LWR/LL), the memory instruction chip constrains mem_access.value == mem_access.prev_value (no modification). For stores, it constructs mem_val from existing bytes. But if any byte value in the chain is not in [0, 255], the field arithmetic in byte selection (e.g., a_val[0] * offset_is_zero + mem_val[1] * ls_bits_is_one) would operate on arbitrary field elements, potentially producing results that appear correct in the field but represent invalid memory states.

The soundness assumption is that the CPU chip and ALU chip properly range-check all register values to be valid 4-byte Words with each byte in [0, 255]. If this assumption is violated anywhere in the constraint system, the memory subsystem would silently propagate and store invalid values.

Fix

Add byte range checks on memory values at the boundary where they enter the memory subsystem. The most effective location is within eval_memory_access in air/memory.rs, which is the single entry point for all memory operations. Add slice_range_check_u8 on the 4 byte elements of both value() and prev_value():

// Within eval_memory_access, add:
self.slice_range_check_u8(&memory_access.value().0, do_check.clone());
self.slice_range_check_u8(&memory_access.prev_value().0, do_check.clone());

This would provide defense-in-depth against any upstream chip failing to properly constrain register/memory values.

[felicityin]

Issue 086

Low - recursion/circuit/machine/ - MaybeUninit::zeroed().assume_init() on Circuit Variables

The recursion circuit's core.rs and compress.rs files use unsafe { MaybeUninit::zeroed().assume_init() } to initialize Felt<_> circuit variables before they are assigned values from proof public values. This pattern is technically undefined behavior (UB) in Rust if the type has any invariant excluding zero-initialized memory. While Felt wraps a field element where zero is valid, the pattern bypasses Rust's safety guarantees.

In the circuit context, these variables are always overwritten in the first loop iteration (i == 0) before being used in constraints. However, if the code were refactored to allow empty proof batches past the assert!(!shard_proofs.is_empty()) guard, the uninitialized values would propagate into constraint assertions.

Fix

Replaced the recursion circuit’s unsafe zero-initialization in core.rs and compress.rs with DSL-managed builder.uninit() for scalar Felt values, and array::from_fn(|_| builder.uninit()) for array-backed locals. This removes the MaybeUninit::zeroed().assume_init() UB pattern while preserving the existing proof-flow semantics.

[felicityin]

Issue 087

Low - recursion/compiler/ir/collections.rs - todo!() on Fixed Array Operations May Cause Panics

Five todo!() macros exist in the recursion compiler's array operations for the Array::Fixed variant. These are in shift(), truncate(), get_ptr(), set(), and set_value() methods. If any circuit code path attempts to perform these operations on a fixed-size array, the compiler will panic during circuit generation, causing a denial of service for the proving pipeline.

While the primary circuit code paths use Array::Dyn (dynamic arrays), the Array::Fixed variant is created via builder.vec() and used for constant-length arrays. Any future refactoring that routes a Fixed array through these methods would silently introduce a crash.

Fix

Fixed the recursion compiler’s Array::Fixed handling in crates/recursion/compiler/src/ir/collections.rs. The todo!() branches are gone: shift, truncate, and get_ptr now fail with explicit unreachable!() messages for unsupported fixed-array semantics, and set / set_value now update fixed vectors directly when given a constant index.

[felicityin]

Issue 088

Low - crates/core/machine/src/utils/mod.rs - zeroed_f_vec relies on debug-only size assertion for transmute safety

The zeroed_f_vec<F: Field> function transmutes Vec<u32> to Vec<F> with only a debug_assert! to verify that size_of::<F>() == 4. This assertion is stripped in release builds, meaning that if this generic function is ever instantiated with a field type whose size is not 4 bytes, it would silently produce undefined behavior. The function is called in 30+ locations across the core machine crate for trace generation, trace padding, and preprocessed trace allocation.

The transmute of zero values is sound for KoalaBear (the production field type) because Montgomery-form zero is represented as 0u32. However, the safety invariant depends entirely on a runtime check that is disabled in production.

Fix

Hardened zeroed_f_vec in crates/core/machine/src/utils/mod.rs by changing the size check from debug_assert! to a normal assert!, so the transmute precondition is enforced in release builds too. I also added a regression test that verifies zeroed_f_vec::<KoalaBear> returns the expected zero-filled vector.

[felicityin]

Issue 089

Low - deserialize.go - Deserialization performs no bounds checking on input data

The deserializeData function in the Go runtime directly indexes into the data byte slice without checking that sufficient bytes remain. A truncated or malformed input will cause a Go runtime panic (index out of range) rather than a graceful error. While this code runs inside the zkVM guest (MIPS target), meaning panics translate to execution failures, the lack of bounds validation means:

1. Slice length as uint64 cast to int (line 84-88): The deserialized length is a uint64 cast to int. On the 32-bit MIPS target, int is 32 bits, so lengths > 2^31-1 silently truncate, potentially causing the slice data[index : index+int(length)] to access an unexpected memory region.
2. No validation that index + size <= len(data): Every type accessor (Bool, Int8, Int16, Int32, Int64, Slice, String) directly reads bytes at computed offsets without checking bounds first.
3. Pointer type deserialization (line 117): When the first byte is nonzero (indicating non-nil), the function recurses into v.Elem(), but for a nil reflect.Value element this will panic.

Fix

Added explicit bounds checks throughout the Go runtime deserializer in crates/goruntime/zkvm_runtime/deserialize.go. All fixed-width reads now go through a shared readBytes helper, slice and string lengths are validated before converting uint64 to int, and nil pointer fields are allocated before recursive decoding instead of panicking on v.Elem().

[felicityin]

Issue 090

Low - runtime.go - RESERVED_INPUT_PTR advances without bounds checking

The Go runtime Read[T]() function allocates memory from a reserved input region by advancing a global pointer (RESERVED_INPUT_PTR). Each call increments the pointer by the padded length of the hint data, but there is no check that the pointer remains within the valid memory region [MAX_MEMORY - EMBEDDED_RESERVED_INPUT_REGION_SIZE, MAX_MEMORY). Successive large reads could advance the pointer beyond MAX_MEMORY (0x7F000000), causing the unsafe.Pointer(uintptr(addr)) to point to invalid memory.

Additionally, the RESERVED_INPUT_PTR is a Go int (32-bit on MIPS32LE), initialized to MAX_MEMORY - EMBEDDED_RESERVED_INPUT_REGION_SIZE = 0x7F000000 - 0x40000000 = 0x3F000000. While the 1GB region is large, there is no guard against reading more total hint data than fits in this region.

This is comparable to the Rust entrypoint (crates/zkvm/entrypoint/src/lib.rs:79-85) which has the same pattern of advancing EMBEDDED_RESERVED_INPUT_PTR without bounds checking.

Fix

Added an explicit bounds check to the Go runtime’s reserved input allocator in crates/go-runtime/zkvm_runtime/runtime.go. Read[T]() now routes pointer advancement through readReservedInput(), which panics with input region overflowed if the hint region would exceed MAX_MEMORY or if the computed capacity is invalid.

[eigmax]

where is the spec to state this? or we just want to reject div-by-zero?

[felicityin]

fn execute_alu(
        &mut self,
        instruction: &Instruction,
    ) -> Result<(Option<u32>, u32, u32, u32), ExecutionError> {
        let (rd, b, c) = self.alu_rr(instruction);
        if matches!(instruction.opcode, Opcode::DIV | Opcode::DIVU | Opcode::MOD | Opcode::MODU)
            && c == 0
        {
            return Err(ExecutionError::ExceptionOrTrap());
        }

[felicityin]

There isn't a spec citation for “trap on div-by-zero” here. The reason for this constraint is that our current executor already rejects DIV/DIVU/MOD/MODU when c == 0, so the AIR should enforce the same behavior instead of accepting impossible rows.

[eigmax]

should update our docs with the latest constraints.

[felicityin]

ok

[eigmax]

Since we have memory range check in GlobalMemoryChip, local memory should be calculated from GlobalMemory, plz check if we already have constraints for the addressing, if we have, we don't need to do range check again.

[felicityin]

This is to fix this issue: 041

Medium - local.rs / MemoryLocalChip - No Independent Range Checking on Bridge Chip Columns

The MemoryLocalChip is the critical bridge between within-shard memory operations (local Memory lookups from eval_memory_access) and cross-shard memory state (global bus connecting Init/Finalize chips). Despite being foundational to memory soundness, its AIR constraints consist exclusively of four lookup send/receive operations with zero structural constraints on any of its 21 witness columns per entry.

Specifically, the following columns are entirely unconstrained beyond lookup matching:

addr (memory address) - no range check, no KoalaBear modulus bound
initial_shard, final_shard - no range check against 24-bit bound
initial_clk, final_clk - no range check against 24-bit bound
initial_value[0..3], final_value[0..3] - no byte range check (values should be in [0, 255])

The system relies entirely on transitive constraint propagation: the MemoryGlobalInit chip range-checks values via 32 boolean bits, and this propagates through the lookup chain. However, this creates a fragile dependency where any implementation bug in the logUp/grand-product argument could allow arbitrary field elements to flow through the memory system undetected.

This stands in sharp contrast with the MemoryGlobalChip, which independently:

Range-checks addr via KoalaBearBitDecomposition
Constrains value via 32 boolean bit decompositions
Enforces address ordering via AssertLtColsBits
Constrains timestamp = 1 for Initialize mode

[eigmax]

check we if we remove boolean circuit garble with Vangher.

[felicityin]

It can be removed by Vangher in the next PR.

[eigmax]

@VanhGer

[VanhGer]

I will make the PR for this.

[VanhGer]

#520
This PR remove the boolean circuit garble precompile
@eigmax @felicityin