Skip to content

feat: core types + arithmetic security hardening #20

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
almogdepaz wants to merge 2 commits into
base: main
Choose a base branch
from
Open

feat: core types + arithmetic security hardening #20

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a939127
feat: core types + arithmetic security hardening (PR 1/7)
almogdepaz Mar 22, 2026
0d2e8e8
feat: TAIL enforcement for CAT spends (F-01 fix)
almogdepaz Mar 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 95 additions & 0 deletions .audit/findings/feynman-pass1.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
# Enemy Pass 1 - Feynman (Full Baseline)

## Pass Ledger
- Pass: `1`
- Auditor: `Feynman`
- Scope: `/Users/home/Dev/veil`
- Mode: `Full baseline (Phase 0->5)`
- Input: Raw `veil` workspace
- Output artifact: `.audit/findings/feynman-pass1.md`

## Phase 0 - Attacker Recon

### Language
- Rust workspace (`src`, `clvm_zk_core`, settlement guests for RISC0/SP1)

### Attack Goals
1. Lock or desynchronize settled assets so users cannot spend outputs after an apparently successful trade.
2. Break nullifier/accounting integrity so spends are accepted while wallet/simulator state diverges.
3. Misroute settlement payment outputs to the wrong recipient key material.
4. Create irreversible state skew between proof outputs and host wallet records.

### Novel / High Bug-Density Areas
- `src/cli.rs`: local validator/orchestrator flow for `offer-create` and `offer-take`.
- `src/protocol/settlement.rs`: host-side extraction of maker terms + settlement proof creation.
- `src/simulator.rs`: nullifier and commitment state mutation (`process_settlement`).
- `backends/*/guest_settlement/src/main.rs`: settlement output commitments and public fields.

### Value Stores and Outflow/Mutation Paths
- **Nullifier anti-double-spend state:** `CLVMZkSimulator.nullifier_set`
- Mutated by: `spend_coins_*`, `process_settlement`.
- **Spendable commitment tree/index:** `coin_tree`, `commitment_to_index`, `merkle_leaves`
- Mutated by: `add_coin*`, `spend_coins_*`, `process_settlement`.
- **Wallet-side spend descriptors:** `WalletCoinWrapper { coin, program, spent }`
- Mutated by: faucet/transfer paths and `offer_take_command` wallet insertion.
- **Offer metadata:** `StoredOffer.{maker_pubkey,maker_bundle,offered_tail_hash,requested_tail_hash}`
- Mutated by: `offer_create_command`, consumed by `offer_take_command`.

### Complex Interaction Path
1. `offer_create_command` -> persists `StoredOffer`.
2. `offer_take_command` -> `prove_settlement(...)` -> dual proof verification -> `simulator.process_settlement(...)`.
3. `offer_take_command` then reconstructs output coins into wallets for future spending.

This path crosses proof construction, proof verification, state commitment insertion, and wallet local state mutation.

## Phase 1 - Function-State Matrix (Condensed)

| Function | Reads | Writes | Guards / Assumptions | External Calls |
|---|---|---|---|---|
| `offer_create_command` | maker wallet coin/program, requested tail arg | pending offer list, maker coin `spent=true` | assumes delegated puzzle hash match and exactly one maker coin | `Spender::create_conditional_spend` |
| `offer_take_command` | offer metadata + taker coin + simulator root/path | simulator settlement state, maker/taker wallet coins, pending offers | assumes settlement output is link-consistent with stored offer metadata | `prove_settlement`, proof verifiers, `process_settlement` |
| `prove_settlement` | maker proof bytes/journal, taker coin data | settlement proof/output | assumes validator enforces maker/taker linkage and maker pubkey binding | zkVM prover (`risc0`/`sp1`) |
| `CLVMZkSimulator.process_settlement` | settlement output | nullifier set, commitment index/tree | assumes upstream output commitments map to wallet-manageable coin descriptors | none |
| `Spender::create_spend_with_serial` | wallet coin + program + secrets | proof bundle | assumes `program` compiles to `coin.puzzle_hash` and commitment fields align | `ClvmZkProver::prove_with_serial_commitment` |
| `SettlementProof::to_spend_bundle` | settlement output | single-nullifier spend bundle | assumes one nullifier is sufficient for downstream validators | none |

## Phase 2 - Feynman Interrogation Highlights

### Suspect FS-01 (Category 1/2/7): Settlement output reconstruction appears inconsistent with spend semantics
- **Question:** Why are post-settlement wallet coins created with placeholder program source instead of the program that matches each coin's `puzzle_hash`?
- **Code evidence:**
- `offer_take_command` inserts five post-settlement wallet coins with `program: "(mod () (q . ()))"` (`src/cli.rs`, around lines `2925-3035`).
- Spending path later uses stored wallet program when proving (`src/cli.rs`, around lines `2124-2127` and `1736-1739`).
- Guest spend logic asserts compiled `program_hash == coin.program_hash` (`backends/risc0/guest/src/main.rs`, around lines `374-375`).
- **Verdict:** `SUSPECT`.
- **State feed to Pass 2:** wallet coin descriptor (`coin fields + program`) <-> simulator commitment tree entries.

### Suspect FS-02 (Category 3/4): Asset-type metadata may be dropped on settlement wallet insertion
- **Question:** Why are settlement output coins instantiated with `PrivateCoin::new` (XCH default tail) even when settlement supports non-XCH asset tails?
- **Code evidence:**
- `offer_take_command` creates all five settlement wallet coins via `PrivateCoin::new(...)` (`src/cli.rs`, around lines `2912`, `2937`, `2961`, `2993`, `3019`).
- `PrivateCoin::new` hardwires `XCH_TAIL` (`src/protocol/structures.rs`, around lines `101-103`).
- Coin commitment includes `tail_hash` in preimage (`clvm_zk_core/src/coin_commitment.rs`, lines around `71-85` and `105-123`).
- **Verdict:** `SUSPECT`.
- **State feed to Pass 2:** settlement commitment tail-hash state <-> wallet `coin.tail_hash`.

### Suspect FS-03 (Category 3/4): Missing explicit maker key linkage check despite stated validator requirement
- **Question:** Why is there no check that `settlement_proof.output.maker_pubkey` matches `offer.maker_pubkey` before settlement state mutation?
- **Code evidence:**
- Guest output explicitly exposes `maker_pubkey` for validator checking (`backends/*/guest_settlement/src/main.rs`, comments around lines `22-33` and `143-153`).
- CLI comment acknowledges required check but does not enforce it (`src/cli.rs`, around line `2816`).
- **Verdict:** `SUSPECT`.
- **State feed to Pass 2:** offer metadata key <-> settlement proof public key <-> payment coin derivation.

### Suspect FS-04 (Category 6): Settlement bundle helper drops one nullifier
- **Question:** Why does `SettlementProof::to_spend_bundle()` include only `maker_nullifier` while settlement output carries two nullifiers?
- **Code evidence:**
- `to_spend_bundle` maps settlement to single-nullifier `PrivateSpendBundle` (`src/protocol/settlement.rs`, around lines `43-51`).
- **Verdict:** `SUSPECT` (possible API-level inconsistency; requires state cross-check for active usage).

## Verification Summary (Pass 1)
- Confirmed C/H/M findings this pass: `0`
- Suspects forwarded to State pass: `4` (`FS-01`..`FS-04`)

## Output for Pass 2
- Run full State pass on coupled pairs around settlement outputs, wallet descriptors, nullifier sets, and offer metadata linkage.
99 changes: 99 additions & 0 deletions .audit/findings/feynman-pass3.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
# Enemy Pass 3 - Feynman (Targeted Re-Interrogation)

## Pass Ledger
- Pass: `3`
- Auditor: `Feynman`
- Scope mode: `Targeted (delta-only)`
- Input delta from Pass 2:
- `SI-001` (settlement output reconstruction mismatch)
- `SI-002` (maker key linkage check omission)
- `SI-003` (single-nullifier projection helper)
- Scope IN:
- `src/cli.rs` offer-take and spend flows
- `src/protocol/structures.rs` + `clvm_zk_core/src/coin_commitment.rs`
- `backends/risc0/guest/src/main.rs`
- `src/protocol/settlement.rs`
- Scope OUT:
- previously-cleared non-settlement modules
- Output artifact: `.audit/findings/feynman-pass3.md`

## Targeted Interrogation

### Delta Item A - SI-001 (wallet reconstruction mismatch)

**Q1:** Why does settlement insert wallet outputs with a placeholder program?

**Trace:**
1. `offer_take_command` pushes settlement outputs to both wallets with `program: "(mod () (q . ()))"` (`src/cli.rs`, around `2925-3035`).
2. Future spends consume this stored program (`src/cli.rs`, around `1736-1739`, `2124-2127`).
3. Guest spending enforces `program_hash == commitment_data.program_hash` (`backends/risc0/guest/src/main.rs`, around `374-375`).

**Q2:** Why are settlement output coins instantiated as XCH regardless of proof tail hashes?

**Trace:**
1. Settlement params include explicit asset tails (`taker_tail_hash`, `goods_tail_hash`) (`src/cli.rs`, around `2752-2756`).
2. Settlement guest commitments are built with those tails (`backends/risc0/guest_settlement/src/main.rs`, around `119-145`).
3. Host inserts wallet coins with `PrivateCoin::new(...)` (XCH default) (`src/cli.rs`, around `2912`, `2937`, `2961`, `2993`, `3019`; `src/protocol/structures.rs`, around `101-103`).
4. Commitment preimage includes `tail_hash`; CAT/XCH mismatch changes leaf (`clvm_zk_core/src/coin_commitment.rs`, around `71-85`, `105-123`).

**Feynman verdict:** The implicit assumption is "proof output commitments and wallet coin records are equivalent by construction." They are not. This breaks both spend preconditions: (a) program hash equality and (b) leaf commitment reconstruction.

**Reachability / impact:**
- Reachable on every `offer_take_command`.
- For XCH-only offers: spend path fails at `program_hash mismatch`.
- For CAT-involving offers: failure can occur earlier at merkle path lookup due wrong `tail_hash`, then also at program mismatch.

**Result:** `TRUE POSITIVE`, severity kept `HIGH`.

---

### Delta Item B - SI-002 (maker pubkey linkage guard)

**Q:** Why is there no explicit runtime check that settlement proof key matches stored offer key?

**Trace:**
1. Settlement guests expose `maker_pubkey` publicly "so validator can check it matches offer" (`backends/*/guest_settlement/src/main.rs`, comments around output struct).
2. CLI contains only a comment about this requirement (`src/cli.rs`, around `2816`) and proceeds to state mutation without assertion.
3. Wallet payment puzzle derivation uses `offer.maker_pubkey` (`src/cli.rs`, around `2892-2895`), while proof commitment derivation uses key extracted from maker proof inside `prove_settlement`.

**Feynman verdict:** Missing guard is real. It is a consistency hardening gap: if metadata and proof diverge (tampered/off-path offer object), host local coin reconstruction can desync from proof-committed outputs.

**Reachability / impact:**
- Not triggered on normal in-process offer creation/take flow.
- Triggerable under tampered imported or edited offer metadata.

**Result:** `TRUE POSITIVE`, severity `LOW`.

---

### Delta Item C - SI-003 (`SettlementProof::to_spend_bundle`)

**Q:** Is single-nullifier projection exploitable in active flow?

**Trace:**
- Method exists and drops taker nullifier (`src/protocol/settlement.rs`, around `43-51`).
- No active settlement execution path in this scope uses `to_spend_bundle`; CLI uses `process_settlement(&settlement_proof.output)` directly (`src/cli.rs`, around `2872-2874`).

**Feynman verdict:** Risky API shape, but no in-scope exploitable path currently.

**Result:** `FALSE POSITIVE` for this audit scope.

## Delta vs Previous Passes

### Net-New Findings
1. `FF-001` (Cross-feed `P2 -> P3`): settlement output/wallet reconstruction desync causes deterministic post-settlement spend failure.
2. `FF-002` (Cross-feed `P2 -> P3`): missing maker key linkage assertion before settlement state mutation.

### Net-New Root Causes
- RC-01: Placeholder wallet program + XCH-default tail insertion after settlement.
- RC-02: Required key-link invariant documented but not enforced.

### False Positives Eliminated
- `SI-003`: single-nullifier projection helper not used in active settlement path.

### Severity Adjustments
- None (SI-001 remains HIGH; SI-002 remains LOW).

## Output for Pass 4 (Targeted State Re-Analysis)
- Re-check all settlement mutation paths for additional coupled pairs impacted by RC-01/RC-02.
- Verify no parallel path already performs reconciliation.
71 changes: 71 additions & 0 deletions .audit/findings/nemesis-raw.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
# Enemy Raw Findings (Pre-Final Consolidation)

## Scope
- Target: `/Users/home/Dev/veil`
- Language: Rust
- Priority modules scanned: 10
- Priority functions analyzed: 41

## Pass Timeline

| Pass | Auditor | Mode | Output | Net-New Delta |
|---|---|---|---|---|
| 1 | Feynman | Full | `feynman-pass1.md` | 4 suspects (`FS-01`..`FS-04`) |
| 2 | State | Full (enriched) | `state-pass2.md` | 2 confirmed gaps (`SI-001`, `SI-002`), 1 unresolved (`SI-003`) |
| 3 | Feynman | Targeted | `feynman-pass3.md` | 2 confirmed findings (`FF-001`, `FF-002`), 1 false positive eliminated |
| 4 | State | Targeted | `state-pass4.md` | no net-new items (converged) |

## Phase 1 Enemy Map (Condensed)

| Function | Writes A | Writes B | Coupled Pair | Status |
|---|---:|---:|---|---|
| `CLVMZkSimulator.process_settlement` | nullifier set + commitment tree | wallet descriptors | CP-01/02/03 | producer only |
| `offer_take_command` wallet insertion | wallet coin descriptors | simulator commitments | CP-01/02/03 | **gap** |
| `offer_take_command` key handling | offer key usage | proof key check | CP-04 | **gap** |
| `SettlementProof::to_spend_bundle` | maker nullifier | taker nullifier | CP-05 | asymmetry (later eliminated in-scope) |

## Raw Finding Set

### RF-001 -> NM-001 (survived)
- **Title:** Post-settlement wallet reconstruction diverges from proof-committed outputs
- **Discovery path:** Cross-feed `P2 -> P3`
- **Root cause:** `offer_take_command` inserts settlement outputs with placeholder program source and default XCH tail, while simulator commitments come from settlement proof output (which may include non-XCH tails and different puzzle hashes).
- **Why it matters:** outputs accepted into global state can become non-spendable from wallet flow due `program_hash mismatch` and/or commitment mismatch.
- **Current status:** TRUE POSITIVE (`HIGH`).

### RF-002 -> NM-002 (survived)
- **Title:** Missing maker pubkey linkage assertion before settlement state mutation
- **Discovery path:** Cross-feed `P2 -> P3`
- **Root cause:** runtime never enforces `settlement_proof.output.maker_pubkey == offer.maker_pubkey` despite guest and comments declaring this validator requirement.
- **Current status:** TRUE POSITIVE (`LOW`).

### RF-003 (eliminated)
- **Title:** Single-nullifier projection in `SettlementProof::to_spend_bundle`
- **Discovery path:** Feynman suspect -> State check -> targeted Feynman call-site review
- **Disposition:** FALSE POSITIVE in current scope (helper not used in active settlement state transition path).

## Multi-Step Trigger Traces (Raw)

### NM-001 operational sequence
1. Taker executes `offer_take_command`, producing a valid settlement proof and output commitments.
2. `process_settlement` inserts commitments into simulator merkle/index state.
3. Host inserts corresponding wallet coins using placeholder program and XCH-default tail.
4. Later spend path consumes wallet `program` and `coin` fields.
5. Guest assertion `program_hash == coin.program_hash` fails; CAT outputs can also fail merkle lookup due tail mismatch.

### NM-002 operational sequence
1. Settlement output carries `maker_pubkey` from maker proof/journal.
2. Host does not assert that it equals `offer.maker_pubkey`.
3. If offer metadata diverges (tampered/imported mismatch), local payment coin derivation can diverge from proof output commitments.

## Verification Log (Raw)

| Finding | Method | Result |
|---|---|---|
| RF-001 | Deep code trace across `cli` -> `simulator` -> guest spend invariants | confirmed |
| RF-002 | Deep code trace + invariant check against guest output contract | confirmed |
| RF-003 | Call-site trace | disproved (in-scope non-reachable) |

## Convergence
- No net-new findings in Pass 4.
- Loop converged before pass bound (`4/6` passes used).
Loading
Loading