oh-my-opencode/packages/omo-codex/plugin/skills/programming/references/rust-ub

Rust Undefined Behavior Exorcist

You are a UB hunter. Your job is to find, classify, prove, and eliminate every instance of undefined behavior in Rust code. Miri is your primary weapon — everything else supplements where Miri cannot reach.

Core Philosophy

1. Miri first, always. Before reading a single line of unsafe, run Miri. Before proposing a fix, run Miri. After applying a fix, run Miri. Miri is the oracle.
2. Classify before fixing. Every UB finding gets classified against the 14-category taxonomy (see ub-taxonomy.md). This prevents misdiagnosis and ensures the fix targets the root cause, not a symptom.
3. Prove the fix. A fix is not done until Miri passes with full paranoia flags. If Miri cannot run the test (FFI, I/O), the fix is not done until the appropriate sanitizer passes.
4. Bead handoff. Each resolved UB instance is a "bead" — a discrete, documented, proven fix. Hand it off with: the UB category, the root cause, the fix, and the Miri proof.

The UB Taxonomy

14 categories. The full reference is in ub-taxonomy.md. Memorize the categories; classify every finding:

#	Category	Miri?
1	Aliasing violations (Stacked/Tree Borrows)	YES
2	Data races	YES
3	Use-after-free / dangling pointers	YES
4	Uninitialized memory	YES
5	Invalid values (type invariant violations)	YES
6	Misaligned pointer access	YES
7	Pin invariant violations	PARTIAL
8	FFI boundary UB	LIMITED
9	Incorrect Send/Sync implementations	YES (via race)
10	Out-of-bounds memory access	YES
11	Provenance violations	YES (strict mode)
12	Double free / invalid free	YES
13	Library / unsafe contract violations	PARTIAL
14	Unwinding across extern "C"	PARTIAL

The Hunt Workflow

Phase 1: Reconnaissance

1. Find all unsafe blocks and unsafe impls:

   rg 'unsafe\s*(fn|impl|{|\{)' --type rust -n
   

2. Find all unsafe trait implementations:

   rg 'unsafe\s+impl\s+(Send|Sync)' --type rust -n
   

3. Find transmute / pointer casts / raw pointer derefs:

   rg '(transmute|transmute_copy|from_raw|into_raw|as_ptr|as_mut_ptr|offset|add|sub|read|write|copy|ptr::null)' --type rust -n
   

4. Find FFI boundaries:

   rg 'extern\s+"C"' --type rust -n
   

5. Count and catalog. Create a hit list: file, line, unsafe category, initial risk assessment (high/medium/low based on the UB taxonomy).

Phase 2: Miri Sweep (THE CRITICAL PHASE)

Run Miri with escalating strictness. Do not skip any level.

Level 1 — Default (Stacked Borrows):

cargo +nightly miri test 2>&1

Level 2 — Strict Provenance + Symbolic Alignment:

MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-backtrace=full" \
  cargo +nightly miri test 2>&1

Level 3 — Full Paranoia (the audit standard):

MIRIFLAGS="\
  -Zmiri-strict-provenance \
  -Zmiri-symbolic-alignment-check \
  -Zmiri-preemption-rate=0.1 \
  -Zmiri-backtrace=full \
  -Zmiri-disable-isolation" \
  cargo +nightly miri test 2>&1

Level 4 — Tree Borrows (second model confirmation):

MIRIFLAGS="\
  -Zmiri-tree-borrows \
  -Zmiri-strict-provenance \
  -Zmiri-symbolic-alignment-check \
  -Zmiri-preemption-rate=0.1 \
  -Zmiri-backtrace=full \
  -Zmiri-disable-isolation" \
  cargo +nightly miri test 2>&1

Interpret results:

• Fails at Level 1 → Definite UB. Fix immediately.
• Passes Level 1, fails Level 2 → Provenance or alignment UB. Fix.
• Passes Levels 1-3, fails Level 4 → Tree Borrows found something Stacked Borrows missed (unusual). Investigate — may be a Tree Borrows false positive, but usually indicates fragile aliasing.
• Passes all 4 → Miri-clean. Proceed to supplementary tools.

Phase 3: Supplementary Scans

For code Miri cannot fully cover:

Concurrent code with custom atomics:

RUSTFLAGS="--cfg loom" cargo test --lib --release -- loom_tests 2>&1

FFI-heavy code:

RUSTFLAGS="-Zsanitizer=address" cargo +nightly test -Zbuild-std --target $(rustc -vV | rg host | awk '{print $2}') 2>&1

Untrusted input parsing:

cargo +nightly fuzz run <target> -- -max_total_time=300 2>&1

Phase 4: Fix-and-Prove Loop

For each UB finding:

1. Classify against the 14-category taxonomy.
2. Write the SAFETY comment explaining what is wrong and what the fix must achieve.
3. Apply the minimal fix. Do not refactor — fix the UB and nothing else.
4. Run Miri (Level 3 minimum) on the specific test that triggered the UB.
5. Run Miri (Level 3) on the full test suite to check for regressions.
6. Document the bead:

   BEAD: [Category #] [Short description]
   FILE: [path:line]
   ROOT CAUSE: [one sentence]
   FIX: [one sentence]
   PROOF: Miri Level [N] pass — [command used]
   

Phase 5: Hardening (Post-Fix)

After all beads are resolved:

1. Add Miri to CI if not already present (see miri-sanitizers-loom.md for the GitHub Actions config).
2. Add #[cfg(miri)] regression tests for each bead — these are the tests that originally caught the UB, locked in so it never returns.
3. Review SAFETY comments on every remaining unsafe block. Each must name the specific invariant from the taxonomy.
4. Run the full paranoia sweep one final time to confirm clean.

Miri-First Decision Protocol

When the agent encounters unsafe code during ANY Rust task (not just audits):

Is there unsafe code in the changeset?
  YES → Run Miri Level 1 before proceeding.
  │     Miri fails?
  │       YES → Stop. Classify. Fix. Prove. Then continue.
  │       NO  → Run Miri Level 2 (strict provenance).
  │             Miri fails?
  │               YES → Stop. Classify. Fix. Prove. Then continue.
  │               NO  → Proceed with the original task.
  NO → Proceed normally.

This is not optional. Every unsafe block gets Miri'd before it ships.

SAFETY Comment Standard

Every unsafe block requires a SAFETY comment within 5 lines above it. The comment must:

1. Name the UB category it could trigger (from the taxonomy).
2. State the invariant that makes this safe.
3. Name who/what guarantees the invariant (caller contract, type system, runtime check).

// SAFETY: [Category 4 — Uninitialized Memory]
// All N elements have been written to via `ptr::write` in the loop above.
// The loop runs exactly `len` times, and `len` was validated against the
// allocation size at line 42. MaybeUninit::assume_init is therefore sound.
unsafe { buf.assume_init() }

Bad SAFETY comments that must be rejected:

• // SAFETY: we know this is safe — Says nothing.
• // SAFETY: this is fine because we tested it — Testing does not prove absence of UB.
• // SAFETY: the caller ensures correctness — Which invariant? What is the contract?
• No SAFETY comment at all — Immediate failure.

Audit Report Format

When completing a UB audit, produce a summary:

## UB Audit Report

**Scope:** [crate/module/file]
**Miri version:** [output of `cargo +nightly miri --version`]
**Date:** [date]

### Findings

| # | Category | File:Line | Severity | Status |
|---|----------|-----------|----------|--------|
| 1 | Aliasing | src/buf.rs:42 | High | Fixed (Bead #1) |
| 2 | Uninit | src/ffi.rs:98 | High | Fixed (Bead #2) |

### Beads

#### Bead #1: Aliasing violation in buffer resize
- **Root cause:** `&mut` created while `&` to same slice existed
- **Fix:** Restructured to drop shared ref before taking mutable
- **Proof:** `cargo +nightly miri test -- test_buffer_resize` passes Level 3

### Miri CI Status
- [ ] Miri added to CI (Level 2 minimum)
- [ ] All SAFETY comments reviewed
- [ ] Regression tests added for each bead

Common Fix Patterns

Aliasing → Use UnsafeCell or restructure borrows

// BEFORE (UB: &mut while & exists)
let ptr = slice.as_ptr();
let mut_ref = &mut slice[0];  // UB: ptr still usable

// AFTER
let mut_ref = &mut slice[0];
// ptr is never created / used across the mutable borrow

Uninitialized → Use MaybeUninit::write + assume_init

// BEFORE (UB: mem::uninitialized)
let x: T = unsafe { std::mem::uninitialized() };

// AFTER
let x: T = unsafe {
    let mut uninit = MaybeUninit::<T>::uninit();
    uninit.write(initial_value);
    uninit.assume_init()
};

Provenance → Use expose_provenance / with_exposed_provenance

// BEFORE (UB: provenance lost)
let addr = ptr as usize;
let recovered = addr as *const T;

// AFTER
let addr = ptr.expose_provenance();
let recovered = std::ptr::with_exposed_provenance::<T>(addr);

Send/Sync → Remove manual impl, use PhantomData

// BEFORE (unsound)
unsafe impl Send for MyType {}

// AFTER — if MyType truly needs Send, prove it:
// SAFETY: [Category 9 — Send/Sync]
// MyType's only non-Send field is `*mut Buffer`. Access to the buffer
// is guarded by `self.lock: Mutex<()>`, which provides the
// happens-before guarantee required by Send.
unsafe impl Send for MyType {}

FFI → Validate at boundary

// BEFORE (UB: null pointer from C becomes &T)
let result = unsafe { ffi_call() };

// AFTER
let raw = unsafe { ffi_call() };
let result = NonNull::new(raw).ok_or(Error::NullFromFfi)?;

Activation

This skill activates when:

• The user requests a "UB audit", "miri sweep", "unsafe audit", "soundness check", "rustonomicon audit", "race hunt"
• The agent encounters unsafe code during a Rust task and needs to verify it
• Miri reports a failure and the agent needs to classify and fix it
• The user asks "is this sound?" about Rust code

Miri is not optional. Miri is the proof. Ship nothing unsafe without Miri's blessing.