Unsound SBF `memmove` Rewriting

[0xalpharush]

AI Disclosure: Codex GPT-5.4 xhigh assisted

Summary

The SBF front-end silently rewrites sol_memmove_ into sol_memcpy_ during CFG
optimization when the configuration option solanaDefactoSemantics=true (which is the default).
For overlapping copies, memmove and memcpy have different semantics, so the prover
can prove postconditions that are false for real Solana execution.

Root Cause

The rewrite happens here:

• src/main/kotlin/sbf/cfg/RemoveMemmove.kt#L25

That pass performs an unconditional in-place replacement:

call sol_memmove_

becomes:

call sol_memcpy_

The pass is invoked from pointer analysis optimizations:

• src/main/kotlin/sbf/cfg/PointerOptimizations.kt#L31
• src/main/kotlin/sbf/cfg/SbfCFG.kt#L995

The gate for this rewrite is effectively on by default:

• lib/Shared/src/main/kotlin/ebpf/SolanaConfig.kt#L90
• lib/Shared/src/main/kotlin/ebpf/SolanaConfig.kt#L181
• lib/Shared/src/main/kotlin/ebpf/SolanaConfig.kt#L571

optimisticNoMemmove() returns DefactoSemantics.get() || OptimisticNoMemmove.get(),
and DefactoSemantics defaults to true.

There is also no supported pointer-domain handling for sol_memmove_ itself:

• src/main/kotlin/sbf/domains/memory/PointerDomain.kt#L4773

That path explicitly throws:

throw PointerDomainError("TODO(4): support memmove")

So, as currently implemented, it is not possible to run the normal SBF prover pipeline
on true memmove semantics without relying on an assumption like this rewrite. That may
explain why the rewrite exists, but it does not make the rewrite sound.

Why This Is Unsound

In Agave, the runtime registers the two syscalls separately:

• agave/syscalls/src/lib.rs:453

result.register_function("sol_memcpy_", SyscallMemcpy::vm)?;
result.register_function("sol_memmove_", SyscallMemmove::vm)?;

The actual semantic distinction is implemented in:

• agave/syscalls/src/mem_ops.rs:13

SyscallMemcpy rejects overlap:

if !is_nonoverlapping(src_addr, n, dst_addr, n) {
    return Err(SyscallError::CopyOverlapping.into());
}

memmove(invoke_context, dst_addr, src_addr, n, memory_mapping)

SyscallMemmove does not perform that check:

mem_op_consume(invoke_context, n)?;

memmove(invoke_context, dst_addr, src_addr, n, memory_mapping)

And the shared helper uses overlap-safe copying:

unsafe { std::ptr::copy(src_ptr, dst_ptr, n as usize) };

So memmove is not just a cosmetic alias for memcpy. Rewriting one into the other
changes program semantics on valid overlapping inputs.

Concrete False-Proof Shape

This pattern should be rejected by the prover:

base[0] = 1
base[1] = 2
base[2] = 3
base[3] = 4
memmove(base + 1, base, 3)
assert(base[3] == 1)

Real memmove(base + 1, base, 3) yields:

[1, 1, 2, 3]

so base[3] == 3, not 1.

After the prover rewrites memmove into memcpy, the TAC model performs a forward copy
through the overlap and yields:

[1, 1, 1, 1]

which incorrectly proves the false assertion.

POC

My fork now contains a minimal reproducer in:

• src/test/kotlin/sbf/TACMemmoveSoundnessTest.kt#L27

The checked-in test overlapping memmove should not be rewritten into forward memcpy
constructs exactly the shape above and runs the normal cfg.simplify(globals) pipeline
before TAC translation.

During reproduction, the simplified CFG clearly shows the semantic change:

call sol_memcpy_  /*sol_memmove_*/

and the resulting TAC performs:

Stack_B_3697 := Stack_B_3696
Stack_B_3698 := Stack_B_3697
Stack_B_3699 := Stack_B_3698

which is the forward-copy behavior of memcpy, not overlap-safe memmove.

The test expects verify(tacProg) to return false. Instead, the prover returns true.

The repository also contains a Solana Rust end-to-end witness in:

• src/test/kotlin/solver/SolanaMemmoveSoundnessE2ETest.kt#L25

That test runs the full project_for_tests Solana flow on a Rust rule that performs an
overlapping core::ptr::copy, which is memmove-style and should therefore be valid and
overlap-safe.

How To Run

Checkout 0xalpharush@7f14b30

Prerequisites:

• JDK 21 or another supported JDK
• z3
• cvc5
• For the Solana Rust end-to-end witness, a Python environment with the prover CLI
  dependencies installed, for example:

python -m venv .venv
source .venv/bin/activate
pip install -r scripts/certora_cli_requirements.txt

Run just this POC:

./gradlew test --tests 'sbf.TACMemmoveSoundnessTest.overlapping memmove should not be rewritten into forward memcpy'

Run the Solana Rust end-to-end witness:

./gradlew test --tests 'solver.SolanaMemmoveSoundnessE2ETest.overlapping memmove in a Solana Rust program is unsoundly verified'

Expected Reproduction Result

For the TAC-level unit test, the expected result is a failing test run:

[sbf.TACMemmoveSoundnessTest] > test > overlapping memmove should not be rewritten into forward memcpy(): FAILURE

TACMemmoveSoundnessTest > overlapping memmove should not be rewritten into forward memcpy() FAILED
expected: <false> but was: <true>

That is the soundness failure: the verifier proved a property that is false under the
real Solana runtime semantics for memmove.

For the Solana Rust end-to-end witness, the expected result is a successful test run:

[solver.SolanaMemmoveSoundnessE2ETest] > test > overlapping memmove in a Solana Rust program is unsoundly verified(): SUCCESS

That e2e test is intentionally written to assert the current buggy behavior. A SUCCESS
there means the prover unsoundly treated the bad rule as proved, i.e. it returned
UNSAT for a rule that should fail under real memmove semantics.

Impact

A user program can use overlapping memmove on valid
runtime inputs, and the prover can silently reason about that call as memcpy instead.
That can produce false proofs for memory postconditions after overlapping copies.