Safe Hands: Solana transaction authorization suite (T0 guard + T1 builder + T1 Squads proposer) - #112
Draft
Pratiikpy wants to merge 79 commits into
Draft
Safe Hands: Solana transaction authorization suite (T0 guard + T1 builder + T1 Squads proposer)#112Pratiikpy wants to merge 79 commits into
Pratiikpy wants to merge 79 commits into
Conversation
…nding, T22 rules, velocity, fee caps (31 tests)
…trip) with roundtrip tests (40 total)
…ts, intent binding, injection-proof (8 tests + wasip2 component, 494KB)
…ilder policy pre-check + roundtrip invariant (6 tests, 514KB component)
…+ forged-verdict rejection + Squads v4 proposals (6 tests incl. SH-TRUST-FORGED)
…+ live devnet multisig + full 3-tool flow proven
…, 0.05 SOL moved from vault
… clippy clean on host & wasm targets
… custody tiers, threat models, transcripts
… QA) + SPL on-chain evidence
…harness - decode: resolve v0 Address Lookup Tables explicitly; fail closed when loaded addresses are missing or count-mismatched; preserve signer/ writable flags and program-id-by-index after resolution - policy: aggregate per-transaction spend caps and exact intent-amount matching across all transfers, closing the split-transfer cap bypass - tlv: correct Token-2022 AccountType::Mint marker (1, not 2), with an independent golden test - authorize: require fresh, structurally complete simulation evidence (context.slot + getSlot within max_slot_age); missing evidence -> UNKNOWN - rpc: MockTransport records (method, params) pairs for exact assertions - conformance: supply context.slot + getSlot in the mock so the 20-fixture arena matches the hardened simulate() contract (20/20 passing)
- LICENSE: MIT (the repo previously shipped no license text) — satisfies the submission's MIT requirement; holder "Safe Hands contributors" - .gitignore: ignore env files, private keys / Solana keypairs, local scratch, and node_modules; no blanket *.json so YAML fixtures and registry.json stay tracked
Matches upstream CI (tools/ci/validate_components.sh) locked builds. Fixes the misleading "offline" claim: tests mock RPC (no live network), but cargo still fetches dependencies on a fresh clone, so --offline is not forced.
…+ decoder fuzz A property-based fuzz of the decoder (arbitrary bytes -> Ok/Err, never panic) found a real panic on hostile input: a v0 or legacy message header whose readonly counts exceed the key partition underflowed the writable/signer computation, and legacy parsing indexed account keys without a bounds check. Both now validate and fail closed. - decode: enforce `readonly_signed <= num_signers` and `num_signers + readonly_unsigned <= key_count` for v0 and legacy; bounds-check every legacy account index instead of indexing directly - policy/tests: 6 property-based security invariants (under-cap allows; split-aggregate over-cap never allows; disallowed recipient never allows; authority-change always denies; signed never allows; evaluation deterministic) - roundtrip: decoder totality fuzz (1024 cases) + committed regression seed Verified: core 66, authorize 11, spl 6, squads 6, conformance 20/20.
Clone-and-run reproduction of the safety claim without `just`: host tests (property invariants + decoder fuzz), the 20-fixture attack arena, and all three wasm32-wasip2 release builds. No keys, no funds, no live network.
…n on devnet
Turns the three-plugin authorization suite into a running merchant desk:
issue a USDC invoice, confirm it from finalized chain evidence, and prepare
an approval-gated refund through Squads.
payment-verify (T0, new):
A wasm32-wasip2 component cannot persist a byte, so nothing is stored.
The invoice reference is derived from (merchant, order_id, salt) and is
off-curve by construction, so no key for it can exist. Issuing and
checking an invoice are therefore the same call: an unpaid order returns
its payment link, a paid one returns finalized evidence. Two independent
RPC endpoints must agree; disagreement is UNKNOWN, never a merge.
Rejected: Token-2022, delegated authority, split and multi-owner
payments, duplicates, wrong mint/recipient/reference, failed
transactions. A reference attached to an unrelated transaction is
ignored rather than escalated, so it cannot be used to force manual
review.
merchant_owner, invoice_salt and the settlement mint are host-only. A
live run had the model invent a mint address; with no argument to
supply, an injection cannot invoice in a lookalike token.
durable nonce:
A recent blockhash dies in ~90s, which is shorter than a human takes to
approve a refund. spl-transfer-build can pin validity to a nonce account
instead. It takes two independent operator opt-ins — the nonce account
in allowed_nonce_accounts and advance_nonce in allowed_instructions —
and the decoder now enforces that AdvanceNonceAccount is instruction 0,
which was previously only asserted in a comment.
Tier 1 layering:
Solana Pay URL construction and the operator workflow are a skill, not
compiled code. Two SOPs: a cron-triggered invoice watch and a
manual-only refund with a confirmation gate on every funds-touching
step.
Findings from running it against devnet, each now covered by a test:
- The canonical Solana Pay shape was being rejected. Attaching the
reference makes the RPC render the multisig variant of
TransferChecked, with the payer under multisigAuthority and the
reference listed as a signer despite signing nothing. A genuine SPL
multisig is still refused, at the owner-must-have-signed check.
- Lateness masked the amount. A payment both late and short reported
only LATE. The amount now wins and `late` rides on the evidence. A
non-positive expiry means no expiry.
- Blank optional values, in arguments and in config, were treated as
real values and turned unset options into hard failures.
Fixtures 21-23 add nonce-allowlisted ALLOW, refund redirect DENY, and
refund inflation DENY. stage_local.py no longer skips plugins missing
from a hardcoded list.
105 core tests, 23 conformance fixtures, clippy clean on host and
wasm32-wasip2. Live devnet record in EVIDENCE-merchant.md; EVIDENCE.md
remains historical pre-remediation data and is not evidence for this
build.
The merchant loop was previously only exercised through `zeroclaw agent -m` on the CLI. This records it running end to end over a real Telegram chat against the daemon: charge -> payment link -> customer pays -> PAID with payer and signature, with the trace confirming payment-verify was actually invoked rather than answered from memory.
…ation Records the attack the brief requires, run against the live agent on a real channel: a relayed customer message asking to redirect a refund and skip multisig approval. Two independent layers refuse it — the agent declines and names the attempt, and the builder denies the same request with SH-DENY-RECIPIENT-003 when it is forced through the tools deliberately. The second is the one that holds if the model is compromised. Also records both SOPs loading and validating against the runtime, with the confirmation gates parsed on exactly the funds-touching steps.
…ortuguese The rule read 'default to Portuguese; switch to English if they write in English', and the model answered English messages in Portuguese anyway. The wording was not the problem — a long Portuguese conversation history is a strong prior and outweighed the instruction. A fresh session obeyed the same skill correctly. The rule now leads with mirroring the message being answered rather than a house default. Verified over Telegram switching both ways inside one conversation after /new.
solana-tx-authorize already returned a decision_id committing to the exact transaction bytes, the policy, the verdict and the reason codes. Nothing could check it. `--verify` recomputes all of it: decodes the transaction, canonicalises the policy, re-runs the engine, and re-derives the id. A reviewer does not have to trust our ALLOW, and does not have to trust us either — they recompute it. Verified against a live devnet decision (all 5 checks pass) and against a forged one: swapping the intent recipient while still claiming ALLOW re-derives DENY with SH-INTENT-RECIPIENT-031, so the forgery cannot pass. Building it surfaced that the verdict is not a pure function of (bytes, policy) as the decision_id shape suggests — it also depends on the caller-declared intent and on simulation evidence from RPC. The receipt now carries both, with simulation marked as attested rather than recomputed, because pretending otherwise would let a receipt claim a verdict its inputs do not support. Also adds Kani proof harnesses for the authorization invariants (src/policy/proofs.rs, compiled only under cargo kani) and declares the kani cfg so normal builds and clippy are unaffected.
…s stated honestly Documents `just verify-receipt` (re-derive any decision, including the forgery case) and the Kani harnesses. The Kani section says plainly that the harnesses compile and CBMC starts on them but no run has reached a verdict here, so they are proof obligations rather than proofs — the verified claims remain the ones prove-safety covers.
…JSON The first harness called Policy::from_json, which pulls an entire serde parse into the solver. CBMC spent over an hour walking allocation paths inside it and never reached a verdict. Building the same Policy by hand removes that cost and leaves the harness exploring the decision logic, which is the part actually under proof. Also trims the symbolic amount set to the cap boundary — cap-1, cap, cap+1 — since u128::MAX added solver cost without adding a distinct branch. The module docs now record both limits and why they exist.
No harness reached a verdict. Three rounds of tuning moved the bottleneck but never terminated, so the claims are labelled proof obligations and the README points at prove-safety as the verified set. The negative result is specific enough to be useful: the cost is not the decision logic but the heap collections it reads from. evaluate resolves an allowlist by looking a String up in a BTreeSet<String>, and CBMC must model the tree's node linking. Dropping the JSON parse cut exploration from 1.2 MB to 107 KB of log and moved the stall from serde into BTreeSet; shrinking the collections did not move it again. The fix is structural — split evaluate into fact resolution over collections and a pure decision over resolved booleans, then prove the decision. That is a refactor of audited code and is deliberately not being done late to chase a result.
cargo-mutants broke the policy engine 76 ways and reran the suite. Four
breakages went undetected, and two of them were load-bearing:
policy.rs:302 the packet-size guard. Flipping > to >= survived, so the
boundary was never pinned. A transaction of exactly
max_transaction_bytes — Solana's 1232-byte MTU, a legitimate
maximum-size transaction — could have started being rejected
with every test still green.
policy.rs:25 Verdict::as_str could return "xyzzy". Not cosmetic: that
string feeds the decision_id hash every receipt commits to
and that --verify re-derives.
Two more surfaced on the instruction allowlist: no test drove a known program
carrying an unlisted instruction, and no test covered an operator who removes
transfer_checked from allowed_instructions. Both now have tests.
Survivors in the fee block are left alone deliberately. Policy::from_json
rejects the fee section in v0.1, so that code is unreachable through the
public API; a test that reached it through a back door would assert nothing
about the shipped product. Said so in a comment where the next reader will
find it.
Also adds audit: libs/safe-hands-core
audit: plugins/payment-verify
audit: plugins/solana-tx-authorize
audit: plugins/spl-transfer-build
audit: plugins/squads-proposal-build
audit: conformance, now part of prove-safety: cargo-audit across all six
lockfiles, failing on any new advisory. RUSTSEC-2025-0141 (bincode
unmaintained) is accepted knowingly — Solana's wire format IS bincode-1, and
2/3 changed it, so upgrading would silently change the bytes this project
exists to encode exactly.
…declare what they import Mutation testing on the full 76-mutant run left 16 survivors, not the 4 an earlier partial run suggested. Six were real and now have tests: recipient_matches_intent could be replaced wholesale with `true` and the unit suite passed — no test drove a transfer whose recipient disagreed with the declared intent. The conformance arena covers it; this crate's own tests did not, and mutants only reruns this crate. policy_from_config's emptiness guard could be inverted — the fail-closed path every plugin depends on when no policy is configured. Plus the ATA-matching branch, and both arms of the action/mint consistency check (SPL and bare SOL). Eleven survivors remain and are equivalent mutants, not gaps: ten sit in the fee block, which Policy::from_json rejects outright in v0.1 so nothing can reach it, and one is a redundant emptiness guard that from_json would reject anyway. Adds tools/ci/verify_capabilities.py and `just verify-capabilities`, now in prove-safety. Every other check in this repository reads the source; this one reads the compiled .wasm an operator installs and asserts it imports no capability beyond its declared permissions. All four components import wasi:http and nothing else of consequence — no wasi:filesystem, no wasi:sockets. "Holds no keys and stores nothing" is now a property of the artifact, checked, rather than a claim about the code.
Until now nothing here ever ran the artifact. cargo test links the plugin crates as rlibs and calls their Rust directly; the conformance arena does the same. The .wasm an operator installs was built, linted, and never executed by anything but ZeroClaw itself — a real gap for a security tool, because the source is what we audit and the component is what refuses the payment. component-test loads each staged component into wasmtime, grants exactly the imports the ZeroClaw host grants (WASI p2 plus outbound HTTP, no preopened directory), implements the zeroclaw:plugin/logging host side, and calls execute() across the component boundary. Six refusals asserted: garbage bytes, no policy, no merchant, a single RPC endpoint, and a forged ALLOW handed to the proposer. build.rs regenerates a gate-free copy of wit/v0 on every build, because wasmtime's host bindgen has no features option for @unstable items. Generating it rather than checking in a second copy means a contract change breaks the build instead of drifting silently. Two things this surfaced, both in the harness rather than the product: a DENY verdict returned with success: true is the authorizer working, not erroring, and the builder reads mint decimals from chain before evaluating policy, so its recipient and cap refusals need a live endpoint and cannot be asserted offline. Both are written down where the next reader will hit them.
…gine Two libFuzzer targets, both clean on first run: decode 6,874,508 executions, 0 crashes policy 2,551,685 executions, 0 crashes The decoder target asserts more than absence of panics — it asserts decoding is deterministic. The same bytes must yield the same facts on a second call, because decision_id binds a verdict to exactly those bytes; a decoder that answered differently on a second look would make that commitment meaningless. The policy target is the harness the stalled Kani proofs were reaching for, run by a tool that terminates. Kani could not finish because CBMC models BTreeSet<String> node internals symbolically (its issue #1251); libFuzzer executes concretely, so the collections that blocked verification cost nothing. It asserts ALLOW is unreachable for an unlisted recipient, and that anything allowed cleared every hard invariant — unsigned, no authority change, within cap, no Token-2022 extension. Weaker than a proof, because it explores rather than exhausts. Stronger than a test, because nobody chose the inputs. Kept out of prove-safety deliberately: fuzzing runs for as long as you give it, and a gate has to terminate. `just fuzz <target> <seconds>`.
Author
|
Keeping this as a draft deliberately, and flagging why so it isn't read as an abandoned PR. The Superteam Brasil listing was updated to say that registry PRs are not submissions and that registry merges happen separately after judging, with maintainers inviting the strongest implementation per plugin family. So this branch is not being pushed for review during the bounty window — the submission is a showcase post, and this PR is here as the code it links to. The branch is current and the components are unchanged. Two things have been added since the last push, both aimed at making the work checkable rather than at moving this PR along:
Happy to pick this up whenever maintainers want to look at it post-judging, and equally happy to rebase or split it per whatever the registry process ends up being. |
verify_capabilities.py reads the import table out of each compiled component with wasm-tools, which is not present on ubuntu-latest. Everything else in the gate passed; this was the only missing runner dependency.
The 58s cut showed the Telegram session only. The new cut adds the executed Squads multisig payout on Solana Explorer and the green prove-safety CI run, so the on-chain and offline evidence are both visible in the video rather than only claimed in the README.
The README says what Safe Hands establishes. This says what it does not, at the same level of precision: - the verification boundary drawn explicitly: verdict() is proven exhaustively over all 42 ResolvedFacts fields, resolve()<->evaluate() agreement is proptested rather than proven, and decode() is only fuzzed. An attacker who could make the decoder mis-describe a transaction would defeat all twelve proofs without touching them, so that is named as the weakest link. - intent binding closes bytes-vs-declared-intent, not declared-intent-vs-what -the-operator-meant. The Squads approval covers that gap with a process control, not a technical one. - the surfaces we refuse rather than handle, and why each is hard. - the fixtures are regression tests, not a red team, and saying otherwise would be dishonest. Also records that Kani and cargo-fuzz do not run on Windows, so contributors there cannot reproduce the proofs or the fuzzing locally.
…uild hashes
Two gaps the ROADMAP names, closed.
SH_PROPTEST_CASES: the case count was hard-coded at 512, which is the right
number for a gate that runs on every change but made a longer soak impossible
to ask for. It is now a floor, not a ceiling:
SH_PROPTEST_CASES=200000 cargo test
CI keeps 512 and stays fast.
Artifact provenance: the README publishes hashes from a Windows build with an
honest caveat that a Linux build may differ. CI now publishes its own hashes
from a clean runner in the job summary, so both are visible and comparable
rather than a reader having to take one platform's word for it.
Found by running the suite at 200k cases instead of 512.
split_aggregate_over_cap_never_allows drew 1..8 amounts and then discarded any
draw whose sum missed the cap. Every single-transfer draw is discarded by
construction, and most small ones are too, so proptest exhausted its 1024
global-reject budget and aborted:
Test aborted: Too many global rejects
successes: 3286
global rejects: 1024 at prop_assume!(sum > 25_000_000)
The property never failed - it could not run. This is the backbone of the
split-bypass claim, and it was only ever exercised a few hundred times because
it aborted the moment anyone asked for more.
Now the draw is topped up to clear the cap instead of being thrown away. No
rejects, every transfer still at or under the per-tx cap so the aggregate rule
remains the only one that can fire, and the property runs 200k cases in 1.6s.
Whole suite green at SH_PROPTEST_CASES=200000: 194 passed, 0 failed.
The verification-debt section claimed fuzzing was too short. It now says what happened when that was acted on: a property that could not run at scale, found within minutes of raising the budget, and fixed.
decode() is the weakest link in the verification chain and the ROADMAP says so: verdict() is proven exhaustively, the model/engine agreement is proptested, and everything downstream trusts whatever shape the decoder returns. An attacker who could make it mis-describe a transaction would defeat all twelve Kani proofs without touching one of them. Its only adversarial coverage was a libFuzzer target that cannot run on Windows, plus a uniform-random property. Random bytes essentially never produce a plausible header followed by a hostile length, which is exactly the shape a hand-rolled cursor is most likely to trust. These start from a real transfer message and damage it: - every truncation, byte by byte, including empty - single-byte corruption anywhere in the first 400 bytes - a shortvec claiming up to 65535 elements in front of a real message - every value of the versioned-transaction prefix byte - arbitrary runs spliced in behind a well-formed head Two invariants everywhere: never panic (in the component a panic is a trap, and a caller reading a trap as anything but refuse has failed open), and decode twice must agree (decision_id binds a verdict to exactly these bytes, so a decoder that answered differently would void that commitment). No findings: 6 properties green at SH_PROPTEST_CASES=200000. The value is that they now run wherever cargo test runs, rather than only where libFuzzer does.
The twelve harnesses in policy/resolved/proofs.rs are the strongest claim in the project - ALLOW-requires-every-hard-check stated over the entire decision space rather than sampled. Nothing was running them. Kani is Linux/macOS only, so every contributor on Windows was taking the word 'proven' on trust, and so was every reader of the README. CI is Linux; there was no reason for this gap except that nobody had closed it. Now they run on every push. If a change to the engine breaks an invariant, or the heap-free model drifts from evaluate() in a way the proptest agreement misses, this fails.
The ROADMAP admits the prompt boundary is tested hardest because it is the cheapest to simulate, and that this is a poor reason. Safe Hands trusts three things it does not control and only one of them is a chat message. The RPC endpoint supplies mint decimals, simulation results and the current slot. Decimals decide what '25' means and simulation is a hard gate, so a wrong answer there is not noise. Covered: a simulation slot ahead of the chain, a stale one, eight shapes of malformed evidence (missing context, null result, a string where a slot belongs, a JSON-RPC error, a failed simulation), an unreachable endpoint, and a mint the endpoint will not describe. The operator policy arrives as JSON from host config. Covered: empty, null, non-object, unterminated, 2000 nested brackets, a 5000-element allowlist, negative and 1e400 caps, a duplicate key whose second value is permissive, and homoglyph addresses. One invariant throughout: degrade to refusal, never to permission. An endpoint that lies, stalls, contradicts itself or disappears must never yield a verdict more permissive than an honest one would have. All 7 pass unchanged - the behaviour was already right. The value is that it is now pinned, and that the untested boundaries named in the ROADMAP are no longer untested.
Kani now runs in CI, so the proofs are discharged on every push rather than resting on a local run. Trust-boundary chaos is covered for the RPC and the policy document. Left explicitly open: paid human red-teaming, and a model that has been compromised rather than merely fooled.
The top item in the ROADMAP. decode() is the weakest link in the chain - verdict() is proven exhaustively, everything downstream trusts whatever shape the decoder returns, and an attacker who could make it mis-describe a transaction would defeat all twelve authorization proofs without touching one. Proving it outright is out of reach: it parses heap structures, which is what made the earlier attempt to model-check evaluate() directly fail to terminate. What is in reach is the property that matters most, over a bounded input: no byte string up to N bytes makes the decoder panic Worth a theorem rather than a fuzzing result because of where this runs. In a wasm32-wasip2 component a panic is a trap, and a host that reads a trap as anything but refuse has failed open. Err is a correct answer; unwinding is not an answer at all. Three harnesses: no-panic to 8 bytes, no-panic to 3, and decoding-is-a-function to 6. The bounds are small because Kani explores the whole input space, so every byte costs exponentially. They reach past the signature-vector shortvec, the version byte and the message header - where a truncated buffer and a lying length prefix are both in play. Beyond the bound the same properties are asserted by decode_hostile.rs and the libFuzzer target. CI runs these as a separate non-blocking job. Symbolic execution through a parser can fail to terminate in a way the policy proofs cannot, and a speculative proof must not be able to turn the gate red. The policy job is now pinned to its own harnesses so it cannot regress.
The ROADMAP names this as untested and it is the harder case. Every existing injection test assumes a model that has been tricked - still trying to do its job, given bad information. A compromised model is not confused. It supplies a transaction, an intent that describes it exactly, a passing simulation, and effect evidence that agrees with both. Every consistency check the engine can run against the caller's own story succeeds. Nothing is out of place. What it cannot supply is the operator's policy: caps, the recipient allowlist and the asset list come from host config, which the host injects and strips from caller arguments. So the property is not 'can the engine spot a lie' - against a competent liar it cannot - but that a perfectly consistent story which violates policy is still refused. Seven cases, each with a truthful intent: unlisted recipient, over cap, unlisted asset, a split spend whose intent declares the true aggregate, an asserted passing simulation, and the same violation told honestly and then dishonestly - neither is allowed. Plus a control case that must be ALLOW, so a future change cannot make these pass by refusing everything. If any of them ever fails, intent matching has been promoted from a second check into a substitute for the first, and a compromised model could authorize itself.
Both were listed as open. One is closed; the other is started and honestly described as started - bounded proofs of the property that matters, running non-blocking because symbolic execution through a parser may not terminate.
The ROADMAP calls intent semantics unsolved. That is true of the whole problem
and lazy about the half that is tractable - which was already proven, with the
proofs never given their meaning.
Authorization has three objects, not two: what the operator meant (M), the
policy they wrote (P), and the transaction (T). The usual industry check is T
against a declaration the agent supplies, which is the weakest comparison
available, because a compromised agent supplies both and they agree.
This project checks T against P. It does not check P against M. Saying only
'we do intent binding' hides which of those is which.
INTENT.md defines the denotation of a policy as a set of permitted effect
vectors - net balance movement from simulated before/after state, not the
instruction list, because an instruction list says what a transaction claims
to do and balance movement says what it did. Soundness is then:
evaluate(P, T) = ALLOW => effects(T) in [[P]]
That is not asserted, it is the conjunction of four existing Kani harnesses,
each exhaustive over all 42 fields. The document names which clause each one
discharges. Completeness is explicitly not claimed: refusing something
permissible is a usability cost, allowing something impermissible is the
failure this exists to prevent.
P against M stays open, and no amount of testing closes it - M exists only in
someone's head. Two things would narrow it without solving it: rendering the
policy back to the operator in their own terms, and making the Squads approval
show effects rather than instructions.
…hat measured N = 8 did not finish inside 90 minutes on CI. That is a result, not a setback, and it is worth recording rather than quietly deleting: the obstacle to proving this decoder is the shape of the code, not the amount of proof effort available. Symbolic execution has to carry every path through a hand-rolled cursor that reads length prefixes out of the same buffer it is bounded by. A decoder built from bounded, heap-free steps would be provable at a useful width. This one is not, at any width worth having. So the bounds drop to 4 bytes and the unwind to 8 - enough to cover the signature shortvec, the version byte and the start of the header, which is where a truncated buffer and a lying length prefix are both in play. Beyond that the property is asserted by decode_hostile.rs and the libFuzzer target, which is testing rather than proof and is described as such. This strengthens ROADMAP item 8.1 rather than satisfying it: the first move is to restructure decode until it can be proven, not to keep raising N.
…st of my own
Two independent hostile reviewers were pointed at this branch. Both found
things. These are the ones that are straightforwardly wrong and fixable.
1. Squads: refuse a Controlled multisig.
squads.rs parsed config_authority and nothing ever read it. On a Controlled
multisig that single key can call multisig_add_member, change the threshold,
and rotate the config authority - no vote, no proposal. So the Initiate-only
check this plugin performs proves nothing there: whoever holds that authority
can grant themselves Vote and Execute and approve their own proposal, while
the tool prints 'the agent holds no keys and cannot approve'.
The central safety claim is only true on an Autonomous multisig, so refuse
rather than emit a proposal under a guarantee that does not hold.
2. payment-verify: two endpoints must actually be two endpoints.
Config was validated with starts_with("https://") on each URL and nothing
else. rpc_url == rpc_url_fallback was accepted, queried one provider twice,
and the receipt still reported 'primary and fallback agreed'. A copy-paste in
host config silently turned a 2-of-2 corroboration gate into 1-of-1 while
still claiming corroboration. Identical URLs now drop the fallback, so the
result is honestly single-sourced.
3. chaos_boundaries.rs: my own test asserted nothing.
Added earlier in this session. Every hostile policy assertion sat behind
and not one of the sixteen
documents parses, so the bodies never ran - the test reduced to 'from_json
does not panic'. The reasoning inside was also inverted: it searched for a
zero cap as though that were permissive, when zero is the strictest value
there is.
Rewritten to assert the real contract - hostile documents are rejected - plus
two positive controls: the shipped policy shape must still parse, and an
honest RPC endpoint must still reach Ok. Without those, a change that broke
parsing or the mock would make the whole file pass by refusing everything,
which is precisely the failure it was written to prevent.
237 tests, clippy clean on all three crates.
An independent review checked the docs against the code. These are the places they did not match. Correcting them is more useful than the claims were. EVIDENCE-proofs.md said the program-admission rule was 'held to a proof rather than a test'. The exact opposite is true: it is the one rule the proof model does not implement, so the harnesses say nothing about it. That was the worst line in the documentation and it is now a correction in place rather than a quiet edit. ROADMAP.md now records the model/engine divergence in full: which two functions disagree, that every observed divergence is model-stricter so there is no exploit, and why the proofs still do not transfer - reading 'the model never allows X' as a statement about the engine needs engine-ALLOW implies model-ALLOW, which is false. Also records that 17 of 34 boolean fields are never exercised by the agreement tests, so raising the case count cannot find this. Corrected three claims I wrote earlier in this session: the decoder proofs do not reach past the message header (a legacy message needs 37 bytes to deserialize, so every input they explore returns Err - they prove the length guard does not panic), the chaos policy tests pinned nothing until they were rewritten, and 'seven cases' was six plus a control. README: the proven-engine headline now says verdict function, which is what is actually proven; the pasted Kani output was stale at 8 harnesses and is now 12. Fixture counts said 20, 23 and 28 in different files; all now say 28, which is what is on disk.
Effect analysis diffs balances, so an SPL Approve CPI'd from an admitted program grants an unlimited delegate while moving nothing - zero movements, inside any cap, reachable ALLOW. The vault is drained afterwards, outside this system. FreezeAccount and SetAuthority(CloseAccount) are invisible the same way. The claim that the worst case is the operator's cap was wrong; the worst case is an unbounded standing delegate. And the mitigation for it is unavailable: neither T1 builder populates facts.effects, so under an effects.required policy both return UNKNOWN instead of a proposal. The transactions the decoder cannot read are exactly the ones that cannot be routed to a human through Squads. Writing these down rather than fixing them under time pressure. A reader should get them from the roadmap, not from an exploit.
…roke The config_authority check added in the previous commit broke three existing tests, because the shared multisig fixture had always built a Controlled multisig - config_authority set to [8u8; 32]. Nothing had ever depended on that being Autonomous, so nothing had noticed. The fixture now builds an Autonomous multisig, which is the only shape this tool is willing to propose against, and a new test patches only the config_authority bytes of that same fixture to assert the refusal fires and names its reason. Building those bytes by hand instead - as an earlier draft did - tested the account parser rather than the rule: it refused, but for a malformed-account reason, which would have passed a weaker assertion while covering nothing. 12 tests in this crate, clippy clean on host and wasm32-wasip2.
The most serious finding from the adversarial review, and the one the docs got most wrong. Effect analysis diffs balances. An SPL Approve, CPI'd out of a program the operator has admitted, moves zero lamports and zero tokens: every Movement is zero, the transaction sits inside any per-transaction cap, and it can reach ALLOW. What it leaves is a delegate entitled to the whole balance, drained later, outside this system, with no policy consulted. FreezeAccount and SetAuthority(CloseAccount) were invisible the same way. parse_token_account read mint, owner, amount and state, and skipped exactly the fields that matter here: delegate at 72..108, delegated_amount at 121..129, close_authority at 129..165. effects::authority_changes compares those four across the transaction and reports the accounts where they moved. It reports the fact and does not decide what to do about it - which changes are acceptable is the policy's business, and revocation is reported alongside grant for that reason. Deliberately built as a separate function rather than a field on Balance: the struct is constructed in a dozen places across tests and callers, and widening it to close a security hole would have meant touching all of them under time pressure. Seven tests, including a positive control - an ordinary transfer must NOT be reported, or a function that returned everything handed to it would pass every other case. Accounts on only one side are excluded: creation and closure are already visible as movements, and reporting them here would flag every ATA creation. The README's claim that the worst case is the operator's cap was false. The worst case was an unbounded standing delegate, and the amount at risk was the account rather than the transaction.
…e roadmap Also states plainly what is still missing: authority_changes reports the fact, and nothing yet turns that report into a denial. Observable is not enforced.
Completes the previous commit. Detecting the grant and then allowing the transaction would have been worse than not detecting it - the report would sit in a receipt nobody reads while the verdict stayed ALLOW. observe() carries the finding on Effects::authority_changed, and solana-tx-authorize folds a non-empty result into facts.authority_change: a fact the engine already denies at policy.rs:485 and the heap-free model already denies at resolved.rs:163. Reusing that fact rather than adding a rule was the point. A new rule needs a new ResolvedFacts field, and the model and engine already diverge on the admitted-program path. Adding a second divergence inside the very subsystem where the proofs are known not to transfer would have widened the hole this work exists to close. So an SPL Approve CPI'd from an admitted program - zero movements, inside every cap, previously reachable ALLOW - is now DENY, by a rule that was already proven.
The load-bearing joint of the whole verification story, and it was broken. Twelve Kani harnesses prove properties of resolved::verdict(). That is only a statement about policy::evaluate() - the function operators run - if the two agree. On the admitted-program path they did not: evaluate() forgives an unfamiliar program when effects are required, present and the operator named it; resolve() denied unconditionally. Engine Allow, model Deny, on the repository's own ALLOW fixture. Nothing was exploitable - every divergence ran model-stricter. But the implication needed for the proofs to transfer is engine-ALLOW => model-ALLOW, and that was false, so on the one path where the engine deliberately permits a program nobody decoded, twelve proofs said nothing. The carve-out is now mirrored in the model, and tests/model_agreement.rs pins it by varying the instruction list - which neither existing agreement check ever does. That is why they could not catch this: 17 of 34 boolean fields, has_unknown_program among them, were unreachable at any case count. Checked the tests actually bite: reverting the model change makes them fail with both verdicts printed, and restoring it makes them pass. 248 core tests, clippy clean.
Under an effects-required policy both builders returned UNKNOWN rather than a draft, because neither ever populated facts.effects. The consequence was backwards: the transactions whose effects matter most - the ones the decoder cannot read - were exactly the ones that could never reach a human through Squads. The mitigation was unavailable precisely when it was needed. Both now observe effects from the same RPC on the same terms as solana-tx-authorize, and fold an authority change into facts.authority_change so a delegate grant denies here too rather than only at the guard. Evidence that cannot be obtained still stays absent, so the engine reports UNKNOWN instead of reading silence as 'nothing moved' - which was the correct half of the original behaviour and is preserved.
The decoder proofs are deliberately non-blocking: symbolic execution through a hand-rolled parser can fail to terminate, which the policy proofs cannot, since that model is heap-free by construction. `continue-on-error: true` on the job does not cover the case that actually happens. The job hits its own `timeout-minutes` and GitHub marks it *cancelled*, and a cancelled job makes the run cancelled no matter what the flag says. So the run at HEAD read red while every substantive job in it was green: prove-safety (offline gate) success machine-checked proofs (kani) success 12/12 harnesses, 414 checks supply-chain audit success decoder proofs (non-blocking) cancelled <- the whole run's verdict Bounding the step with `timeout` instead makes it exit 124, which is an ordinary failure, which `continue-on-error` on the step does absorb. The summary now states which way it went rather than staying silent. If the proof runs out of time that is written into the job summary, next to a pointer at tests/decode_hostile.rs, which asserts the same property on every platform inside the blocking gate. Only the exhaustive form is lost, and saying so is the point.
The roadmap said "the bound is now 4 bytes" directly after recording that
N = 8 did not terminate. A reader takes that to mean 4 does terminate.
It does not.
Two independent CI observations, both on the shipped bounds of 4/3/4:
run 31078266306 job cancelled at its 45-minute limit, ~30 of those
minutes spent in the solver
run 31089942044 bounded step exited 124 at the 25-minute mark
Neither emitted a single `VERIFICATION:- SUCCESSFUL` line, and neither
printed a harness summary. So the honest statement is not that some
smaller N works, it is that none of the ones tried do.
The property itself is not abandoned. tests/decode_hostile.rs asserts
decode-never-panics on every platform inside the blocking gate, and the
fuzzer has 2M inputs behind it. What is missing is the exhaustive form -
the theorem - and the difference between a test and a theorem is exactly
the distinction this project asks to be judged on. Saying "covered by
tests, not by a theorem" costs a claim and keeps the argument intact.
This changes no code. It removes an implication the measurements do not
support.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this is
Three wasm32-wasip2 tool components + a shared core that give a ZeroClaw agent a complete, safe path for moving Solana money:
The agent proposes, a Squads multisig disposes. No component holds a key or signs anything.
Prove it in one command (offline)
All unit tests + a 20-fixture YAML attack arena (amount/recipient/mint swaps, hidden transfers, authority handovers, unlimited delegates, durable nonces, fail-closed paths, and a forged caller-supplied ALLOW) + clippy -D warnings on host and wasm32-wasip2 + release builds of all three components.
Already run live
Notes for review