[Security] Two Security Issues not covered by PR #101: unconstrained data-memory timestamps and ELF BSS clobber

[liyue-cs]

During a systematic review of Pico’s base-ISA constraints and its ELF-to-committed-program pipeline, we independently reproduced most of the under-constraints addressed by PR #101.

While doing so, we found two additional security-relevant issues that PR #101 does not cover:

1. a malicious-prover soundness issue caused by unconstrained data-memory timestamps; and
2. an ELF loader bug that can make the committed initial memory differ from the ELF contents.

Both issues are present on:

main @ 22b0aae6321c1f63c72aafd0b506b5f45b91ffb1
v2.0.0

PR #101 is currently still open and unmerged.

---

Issue 1: Data-memory timestamps are not bound to CPU execution time

Summary

The MemoryReadWrite chip uses witness-controlled chunk and clk columns as the timestamps of data-memory accesses, but those values are not included in the CPU-to-memory instruction lookup.

As a result, a malicious prover can relabel the logical time of a load or store while preserving:

• the CPU instruction lookup;
• per-address timestamp monotonicity;
• the memory permutation/multiset argument; and
• all existing load/store constraints.

This allows verifier-accepted stale or reordered reads.

Affected component

vm/src/chips/chips/riscv_memory/read_write/
vm/src/machine/builder/riscv_memory.rs
vm/src/chips/chips/riscv_cpu/constraints.rs

Root cause

MemoryReadWrite passes its own witness columns into the memory-access argument:

builder.eval_memory_access(
    local.chunk,
    local.clk
        + CB::F::from_canonical_u32(
            MemoryAccessPosition::Memory as u32
        ),
    [
        local.addr_aligned.0[0],
        local.addr_aligned.0[1],
        local.addr_aligned.0[2],
    ],
    &local.memory_access,
    is_mem.clone(),
);

eval_memory_access checks only that the supplied current timestamp is later than the supplied previous timestamp:

self.eval_memory_access_timestamp(
    mem_access,
    do_check.clone(),
    chunk.clone(),
    clk.clone(),
);

The CPU-to-memory dispatch lookup, however, contains only:

opcode
op_a
op_b
op_c
op_a_0
load/store selector flags

It does not contain the CPU row’s chunk or clk.

Therefore, the lookup proves that a particular load/store instruction occurred, but it does not prove that the corresponding memory access occurred at that instruction’s execution time.

The following columns remain prover-controlled from the constraint system’s perspective:

MemoryReadWrite.chunk
MemoryReadWrite.clk
memory_access.prev_chunk
memory_access.prev_clk

They are constrained relative to one another, but not relative to the CPU execution trace.

Why the existing memory argument does not prevent the attack

The memory argument enforces consistency over tuples containing:

(chunk, clk, address, value)

However, because (chunk, clk) is not tied to CPU execution order, the prover can choose a different valid ordering of the accesses.

For example, consider an honest execution:

1. memory[A] = V1
2. memory[A] = V2
3. result = memory[A]

The architectural result must be:

result = V2

A malicious prover can instead assign the load a timestamp placing it after the V1 state but before the V2 write, so that it reads:

result = V1

The memory chain remains monotone under the forged timestamps, and the load constraint still enforces:

current_value == previous_value

The verifier therefore accepts a stale value even though the CPU instruction occurred after the second store.

End-to-end confirmation

We confirmed this through the full production proving and verification path using:

RiscvChipType::all_chips()

with all lookup arguments enabled.

Using the honest program’s own verifying key, prove -> verify accepts a proof whose committed public output contains the stale value V1, although the architectural execution must return V2.

A negative control that changes only the loaded value, without relabeling the memory timestamp, is rejected.

This isolates the unconstrained memory timestamp as the enabling condition.

Cross-chunk variant

The same missing binding appears to extend across execution chunks.

MemoryReadWrite.chunk is not constrained to equal the CPU execution chunk, and the CPU-to-memory lookup does not transport the chunk value. The memory argument therefore authenticates the prover-selected memory coordinate rather than the CPU instruction’s coordinate.

This appears to permit accesses to be relabeled across chunks, including an acausal ordering in which a load is placed after a write that occurs in a later CPU chunk.

The intra-chunk stale-read forgery is independently sufficient to demonstrate soundness failure.

Why register accesses are not affected in the same way

Register accesses are performed using the CPU row’s own clock and occupy the register-address range.

Data-memory accesses are separated by the stack/address guard, which requires data addresses to be at least 2^16.

Consequently, the correctly clocked register chain does not constrain the timestamps of the data-memory chain.

Reference design: SP1

SP1 also delegates instruction execution to separate operation chips, but it explicitly threads CPU state through those chips.

Its CPUState contains the clock and PC, and the operation constraints call:

receive_state(clk, pc, ...)
send_state(clk + increment, next_pc, ...)

The memory accesses therefore use a clock that is part of the same state transition as the instruction execution.

Pico’s split memory chip has no equivalent state-threading mechanism.

Relation to PR #101

PR #101 fixes the adjacent free-address issue by computing the aligned memory address from the instruction address and offset.

However, its formal-verification-fixes branch still calls:

builder.eval_memory_access(
    local.chunk,
    local.clk + ...,
    ...
);

Therefore, PR #101 removes the free address but leaves the free timestamp unchanged.

Suggested fix

Bind the memory-access time to the CPU instruction that dispatches the operation.

For example, include the CPU row’s chunk and clk in the CPU-to-memory lookup tuple:

CPU:
(opcode, operands, selectors, cpu.chunk, cpu.clk)

MemoryReadWrite:
(opcode, operands, selectors, mem.chunk, mem.clk)

This directly enforces:

mem.chunk == cpu.chunk
mem.clk   == cpu.clk

Alternatively, introduce an SP1-style threaded CPU state that includes at least:

chunk
clk
pc

The fix should explicitly cover both:

• same-chunk execution ordering; and
• cross-chunk chunk binding.

---

Issue 2: BSS zero-fill can overwrite in-file .data bytes

Summary

The ELF loader stores the initial memory image in 8-byte BTreeMap entries.

In-file segment data is merged into an existing 8-byte entry, but BSS zero-fill unconditionally replaces the entire entry with zero.

When the end of a file-backed segment and the beginning of BSS share the same 8-byte block, the BSS path deletes valid .data bytes that were loaded previously.

The resulting committed Program.memory_image therefore does not match the ELF.

This issue is distinct from Issue 1: it is not an AIR under-constraint. It is an ELF-to-committed-program integrity bug in the trusted program-loading pipeline.

Affected component

vm/src/compiler/riscv/disassembler/elf.rs

Root cause

For in-file bytes, the loader updates only the relevant half of an 8-byte block:

if addr.is_multiple_of(8) {
    image
        .entry(addr)
        .and_modify(|value| {
            *value += word;
        })
        .or_insert_with(|| word);
} else {
    assert!(addr % 8 == 4);
    image
        .entry(addr - 4)
        .and_modify(|value| {
            *value += word << 32;
        })
        .or_insert_with(|| word << 32);
}

For BSS bytes, however, it uses:

image.insert(addr - addr % 8, 0);

BTreeMap::insert replaces the complete existing 8-byte value.

Therefore, if an earlier iteration loaded valid file-backed bytes into one half of the block, the later BSS iteration replaces both halves with zero.

Trigger condition

The bug is triggered by a PT_LOAD segment satisfying:

p_memsz > p_filesz
p_filesz mod 8 is in 1..=4
the final in-file bytes are nonzero

A representative layout is:

8-byte block:
+0 .. +3   file-backed .data
+4 .. +7   BSS

The loader first inserts the .data low word, then reaches the BSS portion and executes:

image.insert(block_address, 0);

The .data word is lost.

Reachability from ordinary source code

This does not require a manually crafted ELF.

For example:

#[no_mangle]
static mut PAYLOAD: u32 = 0xDEADBEEF;

Using Pico’s normal guest build and default linker can produce a writable load segment whose file-backed portion ends with this four-byte .data object and whose remaining memory size includes BSS.

We observed:

readelf -x .data:
ef be ad de

but after:

Compiler::compile()

the corresponding entry in Program.memory_image is:

0

instead of:

0x00000000DEADBEEF

Security impact

Program.memory_image is used to construct the program’s initial memory commitment.

Therefore, the proof system commits to and proves execution from the corrupted loader output, rather than from the ELF bytes the developer compiled and audited.

For example:

static mut SECURITY_FLAG: u32 = 1;

may be present as 1 in the ELF but committed and executed as 0 by Pico if it lies at the affected .data/BSS boundary.

Possible consequences include incorrect initialization of:

• feature or authorization flags;
• protocol constants;
• state-machine configuration;
• counters or nonces;
• mutable cryptographic state;
• sentinel values used to distinguish initialized and uninitialized state.

Again, the verifier is internally consistent with the malformed Program.memory_image; the security issue is that Pico’s trusted ELF-to-program conversion silently commits a program different from the supplied ELF.

Suggested fix

Make BSS zero-fill non-destructive:

image
    .entry(addr - addr % 8)
    .or_insert(0);

A more robust implementation would construct each segment byte-for-byte and merge explicit byte ranges, rather than mixing 4-byte reads with 8-byte storage blocks.

Suggested regression tests

At minimum, add loader tests for every boundary:

p_filesz mod 8 = 0
p_filesz mod 8 = 1
p_filesz mod 8 = 2
p_filesz mod 8 = 3
p_filesz mod 8 = 4
p_filesz mod 8 = 5
p_filesz mod 8 = 6
p_filesz mod 8 = 7

For each case:

1. use nonzero final file-backed bytes;
2. set p_memsz > p_filesz;
3. compare Program.memory_image byte-for-byte against the ELF segment semantics;
4. verify that only bytes in [p_filesz, p_memsz) are zeroed.

---

Relation to PR #101

During the same review, we independently reproduced the following sites addressed by PR #101:

• SLT/SLTU destination bit;
• DIV/REM remainder bound;
• SRLW/SRAW low-32-bit result limbs;
• SRL/SRA shift amount binding;
• SLL shift-limb selection;
• load addr_aligned;
• DIVUW quot_msb.

We confirmed six of these as end-to-end verifier-accepted forgeries and one as a completeness issue.

We are not re-reporting those findings because PR #101 already addresses them.

However, PR #101 is still open and unmerged, so the affected constraints remain present in main @ 22b0aae / v2.0.0.

Merging PR #101 would not fix either issue reported here:

• Issue 1 concerns the memory-access timestamp, which remains witness-controlled on the PR branch.
• Issue 2 is in the ELF loader and is outside the files modified by PR fix(bug): soundness and constraints for formal verification #101.