security: beta pre-audit, the remaining items (12f, 12k, 13, 16, 11) by cryptskii · Pull Request #1099 · deterministicstatemachine/dsm

cryptskii · 2026-10-02T08:30:56Z

Summary

This PR holds the security pre-audit work that came after #1096 merged. Each item is recorded in specs/requirements/CONFORMANCE_GAPS.md, with its tests and mutation controls in VERIFICATION_MATRIX.md.

12f (§6.66): a parent on a trader lineage already known Invalid at or before p is now terminal. The position resolves Invalid, and the vault key it held is skipped instead of waiting forever. The Lean model is updated (parent_on_an_invalid_lineage_is_invalid).
Body check test: a root cell that names the fulfillment with a different body is Invalid for the lineage. The peer-side check now has a dedicated node test and a mutation control.
12k (§6.66, fixed per the owner's ruling): when a trader's own claim names its fulfillment with the wrong body, the trader's device now resolves the pair Invalid, as its peers do. Before, it reported "retries exhausted". The fix is in the Rust resolution and the Lean model.
S20: the spec text now carries the owner's ruling on relaying a withheld pair, and names §17.5 and §33.
Item 13 (§6.69): the WebView runs only the app's own scripts. There is no 'unsafe-eval', inline scripts are admitted by hash, and navigation is limited to the app's page, the QR link and the beta issue form.
Item 16 (§6.69): a release build exports only the launcher. The Pico self-test activity is now in the debug manifest only.
Item 11 (§6.64), what a sync that hits its limit means (owner ruling, 2026-10-01):
- Each inbox route gets its own budget, and every route is read on every sync.
- A route holding more than the sync took is reported in StorageSyncResponse.more_pending (field 6). That's a status, not an error.
- A copy classified as junk is passed over by its content (envelope_merge_key), never consumed by message id. The id is visible on the spool, and the node keeps a second copy under the same id, so consuming junk by id would let one junk copy hide an honest transfer for good.
- storage.sync resumes each member's read from a persisted cursor. A copy that is never consumed therefore no longer hides what lies more than a page cap (1,024 entries) behind it. inbox.pull is unchanged and moves no cursor.
- The poller stays in its fast (eager) mode on more_pending only while the sync is actually taking entries.

Related Issues

Follows #1096 (security pre-audit). Built on #1097 and #1098, both merged into this branch.

Testing

make lint passes (clippy + fmt): cargo clippy -p dsm_sdk --all-targets -D warnings and rustfmt are clean for item 11's changes. The earlier items' sessions ran their own lint.
make build passes: cargo check -p dsm_sdk --lib --tests passes on the merged tree.
make typecheck passes: the frontend tsc passes with the regenerated dsm_app_pb.ts.
Relevant targeted tests pass:
- Item 11's three node tests on Postgres pass, plus the b0x_consumed and inbox_poller unit tests.
- Eight mutations were each observed red on their named tests.
- The full dsm_sdk lib suite: 1,072 passed. One BLE test failed only in a parallel local run; it shares process-global state, and CI runs this suite single-threaded.
- The conformance evidence check passes.
make android produces a working APK: not run here. Items 13 and 16 were validated by their own Gradle and policy checks.

Checklist

I read CONTRIBUTING.md
I used conventional commits
I updated docs or comments when behavior changed (§6.64, §6.66, §6.69, the matrix, S20)
I did not include secrets, local paths, or machine-specific config
I kept unrelated changes out of this PR
The real-code guard passes; it bans those markers

Notes

Code map pins will be stale. The pins bind each row to the code its evidence reaches, and this PR changes the resolution path (12f, 12k) and the spool read (item 11). A repin needs this PR's own Code map artifact, done the same way fix(ci): main green: https instrumented config, #1095's guard lines made real, repin after #1096 #1098's was.
Still open from item 11: junk sent as a countersign, finality certificate or cert-resync message is refused by its own path and stays on the spool rather than being passed over. It hides nothing behind it, but each time the read returns to the start it re-reads up to one page cap per member.
Not code: the GCP storage fleet still enforces the old 256 KiB cell limit. It needs a redeploy from main before a two-leg trade will work on the phone rig.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Y4wDTToHmJfkYYJvMKXt3u

Generated by Claude Code

…y is skipped (12f) The walk of a trader's lineage (DSM Amendment A8) reports a lineage Invalid at or before p, or quarantined for a divergent write-once register cell, as a failure. parent_for read every failure as "not established", so the facts saw no parent and the key the exercise held waited forever: an impossible operation stranded a DLV key (§23.3, §23.5 arm iv). SoFi Amendment S13 already decides the same verdict for setups: "No trade whose trader's lineage is known invalid can occupy a vault key indefinitely." - trader_at_parent classifies the walk's result as validation::setup_lineage does for setups: Invalid and Quarantined are TraderAtParent::LineageInvalid; Incomplete and Unresolved establish nothing. - ParentPosition::LineageInvalid is terminal, whatever P names: never compatible, always impossible. The two predicates now derive from the root the parent leaves P standing on (root_left_by); impossible is not compatible, since a ParentPosition is always terminal. - Lean: ParentState.lineageInvalid, theorem parent_on_an_invalid_lineage_is_invalid, and its non-vacuity witness. Dropping it from parentImpossible fails three proofs. Tests: dsm::sofi::resolve::tests::the_walks_verdict_on_a_traders_lineage_reaches_the_facts; dsm::sofi::facts::tests::a_parent_on_a_lineage_known_invalid_is_terminal. Mutations, each red: the walk's verdict read as no parent; the facts reading a lineage known invalid as no fact.

…nvalid for the lineage The body check in peer_position (SoFi Amendment S20, 12j) had no test of its own. B trades with its pair's leader refusing the pair, then writes its pair itself with a claim it signs naming its F under another R_realize. The pair registers (matched by F's id); a peer walking B's lineage to q gets Invalid with the body check's reason, and the vault's walk passes over the key B's exercise holds. Mutation: the check compares only the fulfillment id -> red (the walk reads the position as unresolved, not Invalid). Found by this test, recorded separately (12k): B's own device does not resolve q Invalid; its ladder reads the misbodied pair as not registered and waits.

- §6.66 12f: the record (a parent on a lineage known invalid left the key waiting; now terminal), its mutation controls and the Lean theorem. MR-SOFI-0234 Partial -> Met. - §6.66 12j: the body check in peer_position now has its own test and a mutation control (VERIFICATION_MATRIX updated). - §6.66 12k (found by that test, not fixed): the trader's own device reads a pair whose root cell names its F under another body as not registered and waits, where every peer reads the position Invalid. Only the trader's key can make it, and nothing advances either way; the owner decides. - §7 regenerated.

…r, and names §17.5 and §33 Owner ruling, 2026-10-01 (pre-audit 12e), quoted verbatim in S20 as the producer's MUST: the next operation at a vault registers a withheld pair from the signed C_q its exercise carries before advancing past the key, and retries. S20's amends list now names §17.5 (the exercise's new field) and §33. Written on #1096 at CORE's request. MASTER: §1 re-pinned (SoFi 7792794…, 2694 lines); MR-SOFI-0362 carries the MUST.

…he app's own page only (item 13) Pre-audit item 13. The WebView's policy admitted 'unsafe-eval' and 'unsafe-inline' for scripts, so any injected script ran; any http(s) link the page followed was handed to another app, and any other scheme loaded in the WebView itself (a failure while deciding loaded it too). - index.html's Content-Security-Policy: script-src 'self' plus the SHA-256 of each inline script the page carries, which InlineScriptHashes computes from the emitted page (after minification) and writes into the policy. A page without the token, or an inline script with attributes, fails the build. base-uri, form-action and frame-src are 'none'. The bundle needs no eval: production has no devtool, mobile development uses source-map, and web development now uses cheap-module-source-map. - validate-android-assets.js (CI runs it in `npm run build`) reads the page the APK ships and fails on 'unsafe-eval', 'unsafe-inline' for scripts, an inline script its hash does not admit, a hash no script has, the build's token left in place, or base-uri/form-action/frame-src/object-src not 'none'. - WebNavigationPolicy: the app's own assets load; dsm://native/qr/start opens the scanner; the beta issue form (github.com/deterministicstatemachine/dsm /issues/new) opens in the system browser; everything else is refused. Both shouldOverrideUrlLoading and onCreateWindow go through it. The bridge port is posted to WebNavigationPolicy.APP_ORIGIN. - tools/sanitize-android-index.js, which nothing ran and which would have rewritten the policy back to 'unsafe-inline' 'unsafe-eval', is deleted. - style-src keeps 'unsafe-inline' (six style blocks, a style attribute and a JSX style element); recorded as the residual. Verified: the shipped page served locally runs its three inline scripts and mounts React with no violation; an injected inline script is blocked (securitypolicyviolation script-src-elem). Mutations, each red: the policy re-admitting 'unsafe-inline' 'unsafe-eval' (the validator fails); the plugin removed (the validator names the token and the three unadmitted hashes); the policy opening any http(s) (WebNavigationPolicyTest red). Android unit tests 262/0.

…f-test is debug-only (item 16) Pre-audit item 16. PicoSelfTestActivity, a bench tool whose own comment says "Debug bring-up only", was exported by the main manifest with no permission. Any installed app could launch it; with its confirmation extras it calls Unified.counterInitMax() and Unified.birthCageSlot0() ("IRREVERSIBLE"). - The activity and its USB device filter are declared in src/debug/AndroidManifest.xml and src/debug/res only, so a release build does not declare it and nothing can start it. The class stays where it is (the real-code baseline is keyed by path); LocalPicoUsb asks for USB permission itself, so release does not depend on the attach intent. - ci/android_exported_components.sh (run by production_safety_checks.sh): the release manifest states android:exported on every component, exports only MainActivity, and the launcher answers MAIN alone with no data filter. Verified: processDebugResources and processReleaseResources pass; the release merged manifest declares no PicoSelfTestActivity, the debug one does. Mutation: the gate run on the previous manifest fails ("activity com.dsm.wallet.debug.PicoSelfTestActivity is exported").

The WebView runs only the app's own scripts and goes nowhere else; a release build exports the launcher only. Records with exploit, closure, residual (style-src keeps 'unsafe-inline'; allowContentAccess stays default) and the mutation controls; §6.29's Pico entry points at the closure; VERIFICATION_MATRIX rows; §7 regenerated.

…s its peers do (12k) Owner ruling, 2026-10-01 (12k, "Fix now"): "same bytes => same terminal verdict for local and peer resolution; no retry/incomplete result once all required evidence is present; no advancing past the Invalid position". A pair final on F whose root claim names F under another body than derive(P, F) was Invalid at every peer (peer_position's body check, S20) but read as merely lost by the trader's own ladder: rung 0 answered NotRegistered, so sofi.resolve answered RetriesExhausted for good. - PairStanding::Misbodied: the pair final on F, matched by its id, under a claim that is not derive(P, F). is_lost() covers it for the S14 skip. - The facts and the ladder carry the pair standing itself (`pair`) where they carried `registered` and `position_lost`; rung 0 resolves Misbodied Invalid, and resolve_refuted_in_hand does the same. - Lean: Facts.misbodied, read at rung 0; Evolves keeps a misbodied pair misbodied and unregistered; a_misbodied_pair_is_invalid and its non-vacuity witness; resolution_is_permanent covers the new rung; the pending theorems state "not misbodied". Tests: dsm::sofi::facts::tests::a_pair_final_on_its_fulfillment_under_another_body_resolves_invalid; the registration standing test (Misbodied, and Lost while settling); the node test a_root_cell_naming_the_fulfillment_with_another_body_is_invalid_for_the_lineage now asserts B's own resolve is (q, Invalid) — on the old code (q, RetriesExhausted). Mutations, each red: rung 0 reading Misbodied as not registered (the facts test and the node test); the Misbodied fact removed from standing_of (two unit tests); the Lean rung dropped (proofs fail). dsm lib 1396/0.

The trader's own device now resolves a misbodied pair Invalid, as its peers do. Record with the ruling quoted, the tests, and the three mutation controls; §7 regenerated.

The Negative test column takes canonical cargo test names only; the WebView policy check, the Kotlin unit test and the manifest gate are described in prose. Conformance evidence passes.

… read that resumes (item 11) Pre-audit item 11, with the owner's ruling (2026-10-01): each inbox route has its own budget; a route left holding more is resumable status, not an error; junk classified terminally is not charged again; no route starves another; repeated syncs make bounded progress through a route. SOFI's part (wip/item-11-inbox-budget): - StorageSyncRequest.limit is each route's budget, and every route is read on every sync. Previously one budget was spent route by route, so junk on the first route left the rest unread and unreported. - StorageSyncResponse.more_pending (field 6) names each route holding more than the sync took. The sync still succeeds. The poller and the WebView event carry it; the frontend binding is regenerated. - The test harness resumes a held funding admission. Found in review and fixed here: - The work in progress consumed junk by message id. The id is cleartext on the spool, and the node keeps a second copy under an id, so one junk copy under an honest message's id would have hidden the honest copy for good. Junk is now passed over by content: b0x_passed_over(address, copy_key), keyed by envelope_merge_key and checked once a copy opens. b0x_consumed keeps consumption by id for copies of decided objects only. - A copy that opens to none of the spooled payloads is passed over too (RetrievalOutcome::unknown). Before, it held the read position forever. - Every read of a member started at the read position and read at most 16 pages of 64. A copy that is never consumed (which a third party can make) hid everything more than 1,024 entries behind it. storage.sync now reads with retrieve_resuming: each member's read resumes at a persisted cursor (b0x_scan_cursor) and goes back to the position at the spool's end. A read stopped at its page cap reports the route more_pending. inbox.pull reads from the position and moves no cursor. - The read keeps copies in spool order, so a partial take takes the oldest. - The poller entered eager mode on any more_pending, which a pinned route would hold at 8 s instead of 60 s. It now does so only when the sync took entries (enters_eager_mode). Tests: a_route_full_of_junk_keeps_no_other_route_unread_and_is_worked_through, a_copy_passed_over_hides_no_other_copy_under_its_id, a_copy_that_waits_hides_nothing_more_than_a_page_cap_behind_it (node, on Postgres); b0x_consumed and inbox_poller unit tests. Eight mutations, each red on its named tests: the global break restored, unrecognized requests not passed over, more_pending never reported, junk consumed by id, the read never resuming, unknown copies not passed over, the page cap not reported, any pending route hurrying the poller. Clippy -D warnings and rustfmt clean. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y4wDTToHmJfkYYJvMKXt3u

The open "SOFI's sync design" paragraph becomes the closure: each gate, its test and its mutation, the two defects found in review of the hand-off (junk consumed by id, the poller held eager), and what stays open: a countersign, finality certificate or cert-resync message whose body is junk is refused by its own path and left, not passed over. It hides nothing behind it, but a route holding one re-reads up to a page cap per member each time the read returns to the position. VERIFICATION_MATRIX: three MR-STOR-0034 rows. Conformance evidence passes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y4wDTToHmJfkYYJvMKXt3u

No conflicts. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y4wDTToHmJfkYYJvMKXt3u

…ing tag (item 13, CodeQL) CodeQL (js/bad-tag-filter, two high alerts on #1099): the inline-script regex in the build's hasher (InlineScriptHashes) and the shipped-page policy check (webview-policy.js) matched only lower-case <script> and a bare </script>. HTML tag names are case-insensitive and a closing tag may carry whitespace, so an inline <SCRIPT>...</SCRIPT > went unhashed and uncounted. The CSP would then block it, failing closed, but the check whose job is to see every inline script passed. Reproduced with the old checker: a page with an unhashed upper-case script reported no problem. Both now match /<script\b([^>]*)>([\s\S]*?)<\/script\b[^>]*>/gi, and test src= case-insensitively. The fixed checker names the unhashed upper-case script and accepts it once it is hashed. The Android bundle builds, and validate-android-assets passes on the shipped page. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y4wDTToHmJfkYYJvMKXt3u

cryptskii · 2026-10-02T08:46:49Z

Code map is red on 622 stale pins, the expected repin, and nothing else. On db0bfa9, make requirement-map-intent reports PIN_STALE 622 and no unpinned or orphan pins. Every printed reason is a code change, from 12f, 12k and item 11 moving production and test closures. The map check itself is clean: 0 contradictions, 24 sentinels with 0 lost, 0 entry points new or lost, and 40 of 40 mutation cases passing. So are intent rows (0 failing).

The repin needs this PR's own code-map artifact and pin-evidence log, done the same way #1098's was. A session with artifact access is doing it now and will push it to this branch. f2b362a, the CodeQL regex fix, changes no Rust, so the pins are the same on either head.

Generated by Claude Code

…34's status accepted #1099's Code map read 622 PIN_STALE (run 36984943750 at f2b362a), with no unpinned or orphan pins: 12f and 12k moved the SoFi resolution path, and item 11 moved the spool read and the sync, along with their evidence tests' closures. Each key went through intent_pins' own rules (prepare, judge_repin, refuse_evidence, seal_new), with the map loaded once: - 622 repinned at f2b362a, every one a code move. - Two of them, MR-SOFI-0234's trader_parent_compatible and trader_parent_impossible, also moved status from Partial to Met. 12f closed that gap (88a6ca6, CONFORMANCE §6.66 12f: the walk's Invalid verdict reaches the facts; two tests and three mutation controls). The status move was checked against that record and accepted by name. The map was built here with `make requirement-map` and checked against CI's. Its stale-pin digests equal every one CI's Code map printed for this commit (175 of 175 in the log's window), and its totals match (622 stale, 13 pinned, 1148 rows). Evidence came from a board run of this commit's code: - the core crate and every crate before dsm_sdk (1731 passed); - the storage node, in full; - dsm_sdk's 46 evidence tests and supply_cap_enforcement. All passed. make requirement-map-intent MAP=... INTENT_BUILT=android,node: 0 failing rows, 0 failing pins, 635 PINNED. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y4wDTToHmJfkYYJvMKXt3u

Two conflicts, the conformance record and the verification matrix: each side appended at the same place (main's §6.69 and item 11 rows, this branch's §6.70 and SPHINCS+ rows). Both kept, §6.69 before §6.70. Conformance evidence passes; the real-code guard passes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y4wDTToHmJfkYYJvMKXt3u

cryptskii and others added 13 commits October 1, 2026 23:02

docs(conformance): 12k closed with the owner's ruling (§6.66)

9e9e386

The trader's own device now resolves a misbodied pair Invalid, as its peers do. Record with the ruling quoted, the tests, and the three mutation controls; §7 regenerated.

docs(matrix): items 13 and 16 name their non-cargo checks in prose

43bf9ad

The Negative test column takes canonical cargo test names only; the WebView policy check, the Kotlin unit test and the manifest gate are described in prose. Conformance evidence passes.

Merge main (#1097, #1098) into security/beta-pre-audit-remaining

db0bfa9

No conflicts. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y4wDTToHmJfkYYJvMKXt3u

github-advanced-security Bot found potential problems Oct 2, 2026

View reviewed changes

Comment thread dsm_client/frontend/scripts/webview-policy.js Fixed

Comment thread dsm_client/frontend/webpack.config.js Fixed

cryptskii merged commit 52d7257 into main Oct 2, 2026
27 checks passed

This was referenced Oct 2, 2026

security: SPHINCS+ construction version 2, the FIPS 205 structure with BLAKE3 (pre-audit item 17) #1100

Merged

security: a transfer's memo, ticker and nonce are in no public object (pre-audit item 4) #1102

Merged

Navigation Menu

security: beta pre-audit, the remaining items (12f, 12k, 13, 16, 11) - #1099

security: beta pre-audit, the remaining items (12f, 12k, 13, 16, 11)#1099
cryptskii merged 15 commits into
mainfrom
security/beta-pre-audit-remaining

cryptskii commented Oct 2, 2026

Uh oh!

Uh oh!

Uh oh!

cryptskii commented Oct 2, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

cryptskii commented Oct 2, 2026

Summary

Related Issues

Testing

Checklist

Notes

Uh oh!

Uh oh!

Uh oh!

cryptskii commented Oct 2, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants