verification-protocol

name	verification-protocol
description	Trigger Pattern Always (used by all verifier agents) - Inject Into security-verifier agents (Phase 5)

VERIFICATION_PROTOCOL Skill (DAML)

Trigger Pattern: Always (used by all verifier agents) Inject Into: security-verifier agents (Phase 5) Purpose: Prove hypotheses TRUE or FALSE using daml test over Script () functions on the in-memory ledger, with submit/submitMustFail/query@T as the harm oracles.

---

Evidence Source Tracking (MANDATORY)

CRITICAL: For EVERY piece of evidence, tag its source. Evidence from mocks, documentation, or unverified external packages CANNOT support a REFUTED verdict. There is no public Canton read RPC, so production-onchain tags do not exist for DAML — [CODE] (in-scope source) plus an executed daml test is the strongest evidence available.

Tag	Meaning	Valid for REFUTED?
[CODE]	Audited codebase (in-scope .daml source) + executed daml test	YES
[POC-PASS]	A Script () compiled, daml test ran, harm assertion PASSED	YES (CONFIRM)
[POC-FAIL]	A Script () compiled, daml test ran, harm assertion FAILED	YES (REFUTE)
[CODE-TRACE]	Manual trace with concrete party/contract values, no execution	NO (caps at CONTESTED)
[MOCK]	Helper template / test-only state that does not exist in the audited templates	NO
[DOC]	Documentation / spec only	NO

Evidence Audit Table (REQUIRED in every verification output)

### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
|-------|-----------------|-----|-------------------|

Mock Rejection Rule

If ANY evidence supporting REFUTED has tag [MOCK] or [DOC]: CANNOT return REFUTED, MUST return CONTESTED, triggers a re-PoC against the actual in-scope templates.

---

Pre-Verification Understanding

Before writing ANY Script code, answer these three questions:

1. What is the EXACT bug? — Not "Authorization is missing" but "Choice Iou.Transfer lists only owner as controller and never re-asserts the issuer/co-signatory, so any single owner can move the asset without the joint authorization the template otherwise requires (Iou.daml:line N, template Iou, choice Transfer)".
2. What OBSERVABLE difference proves it? — Concrete before/after ACS state: which party holds which contract, what query@T party returns, what amount each child carries.
3. What is the EXACT assertion? — e.g., submit attacker (exerciseCmd cid Transfer with newOwner = attacker) SUCCEEDS and then query @Iou victim returns [] while query @Iou attacker is non-empty; or submitMustFail attacker (...) proves the guard holds (REFUTES).

If you cannot answer all three → ASK FOR CLARIFICATION.

---

Pre-PoC Feasibility Gates (MANDATORY)

Gate F1: Reachability

• Entry point identified (a choice exercisable by the attacker party, or a create the attacker can submit)
• Required authorizers traced: the choice's controller parties (AND-joined) and, for create, the new contract's signatory parties
• All required authorizers are parties the attacker profile actually controls or can obtain

If the choice's controllers / the contract's signatories include a party the attacker cannot supply → UNREACHABLE → FALSE_POSITIVE. If reachable only by a fully-trusted operator party acting maliciously → document trust assumption, adjust likelihood.

Gate F2: Value / Boundary Bounds

• Parameter domains identified (amount type Int/Decimal, list lengths, deadline range, cap)
• Expression evaluated at worst-case feasible inputs (0, 1, negative, max, empty list)
• Result crosses the bug threshold (invalid contract creatable, conservation violated, reachable abort, outsider query non-empty)

If values outside feasible domains → INFEASIBLE → FALSE_POSITIVE.

Both gates PASS → proceed to PoC. Either gate FAILS → document and stop.

---

DAML Anti-Hallucination Rules (MANDATORY)

Verify EVERY API call against these known-correct patterns. Do NOT assume EVM/Solana/Rust shapes apply.

-- Party allocation
attacker <- allocateParty "Attacker"          -- NOT: newParty, Address::generate
[a, b]   <- mapA allocateParty ["A", "B"]

-- Create / Exercise / ExerciseByKey
cid  <- submit issuer  (createCmd Iou with issuer; owner; amount)
cid' <- submit owner   (exerciseCmd cid Transfer with newOwner = bob)
res  <- submit p        (exerciseByKeyCmd @Account (issuer, label) Some_Choice with ...)

-- Negative test (the cmd is EXPECTED to FAIL)
submitMustFail attacker (exerciseCmd cid Transfer with newOwner = attacker)
-- ^ a PASSING submitMustFail means the action was BLOCKED → proves SAFETY → REFUTES the bug.

-- Party-scoped visibility oracle (the privacy harm oracle)
cids <- query @Iou outsider          -- what `outsider` can actually SEE; NEVER a god-view
mb   <- queryContractId owner cid     -- Some payload if `owner` is a stakeholder, None if not visible

-- Time control (deadline PoCs) — requires Daml.Script with time control
setTime (time (date 2024 Jan 1) 0 0 0)
passTime (days 8)
now <- getTime

-- Multi-command submit
submit p $ do
  c1 <- createCmd T1 with ...
  exerciseCmd c1 SomeChoice with ...

Authorization model facts (the spine of every DAML auth/asset PoC):

1. Controller vs signatory: the required authorizers of an Exercise/Fetch are the choice's listed controller parties (AND-joined); the required authorizers of a Create/Archive are the new/old contract's signatory parties. submit p cmd supplies authority for party p only.
2. Consuming kind: a consuming (default) choice ARCHIVES the contract on first exercise — a 2nd exerciseCmd on the same ContractId MUST fail with CONTRACT_NOT_FOUND. That failure REFUTES a double-spend claim; a SUCCEEDING second exercise on a wrongly-nonconsuming value-mover CONFIRMS double-spend.
3. ensure violation throws PreconditionFailed: a create whose ensure is False never enters the ACS.
4. Keys: maintainers MUST be signatories. lookupByKey returning None means "the submitter cannot SEE a contract with that key" (visibility), NOT "no such contract exists" — a false-None PoC must allocate a party that genuinely cannot see the keyed contract, then show the None branch mints/duplicates state.
5. submitMustFail semantics: submitMustFail p cmd PASSES when cmd FAILS. So the CONFIRM direction for an auth bug is submit attacker (...) SUCCEEDING plus a harm assertion; a passing submitMustFail proves SAFETY (REFUTES). State this explicitly whenever a submitMustFail is the deciding test.
6. query@T party is the privacy harm oracle — it returns only what party is a stakeholder of. Never assert against a god-view; an outsider seeing a contract = not (null (query @T outsider)).
7. Divulgence vs observer: fetch inside a shared transaction divulges a contract incidentally (transient, only to that transaction's witnesses), whereas observer is persistent visibility. A privacy finding must distinguish which mechanism is the leak.

---

DAML PoC Script Templates

Every PoC is a top-level Script (). daml test runs every in-scope Script (); isolation is file-scoped (one PoC file per finding: daml-test/PoC_{id}.daml).

Template 1: Missing / Single-Where-Joint Authorization

-- AUTHORIZATION: buggy direction — attacker succeeds + harm assertion
test_single_where_joint_auth : Script ()
test_single_where_joint_auth = do
  issuer   <- allocateParty "Issuer"
  owner    <- allocateParty "Owner"
  attacker <- allocateParty "Attacker"
  cid <- submit issuer do createCmd Asset with issuer; owner; amount = 100.0
  -- EXPLOIT: the choice lists only `owner` as controller; no co-auth from issuer
  submit owner do exerciseCmd cid Transfer with newOwner = attacker
  -- HARM: ownership moved without the joint authorization the template implies
  victimCids   <- query @Asset owner
  attackerCids <- query @Asset attacker
  assert (null victimCids)
  assert (not (null attackerCids))

-- REFUTATION direction: if co-auth IS required, this proves SAFETY
test_auth_is_enforced : Script ()
test_auth_is_enforced = do
  issuer <- allocateParty "Issuer"; owner <- allocateParty "Owner"; attacker <- allocateParty "Attacker"
  cid <- submit issuer do createCmd Asset with issuer; owner; amount = 100.0
  submitMustFail owner do exerciseCmd cid Transfer with newOwner = attacker
  -- PASSING submitMustFail ⇒ guard holds ⇒ REFUTES the bug.

Template 2: Double-Exercise via Wrong Consume-Mode

test_double_spend_nonconsuming : Script ()
test_double_spend_nonconsuming = do
  issuer <- allocateParty "Issuer"; owner <- allocateParty "Owner"
  cid <- submit issuer do createCmd Iou with issuer; owner; amount = 100.0
  -- If Spend is wrongly `nonconsuming`, the SAME cid can be exercised twice
  submit owner do exerciseCmd cid Spend with to = issuer
  submit owner do exerciseCmd cid Spend with to = issuer   -- succeeds ⇒ double-spend CONFIRMED
  -- (If Spend is correctly `consuming`, the 2nd exercise fails CONTRACT_NOT_FOUND ⇒ REFUTED)

Template 3: Value Conservation Across Split / Merge

test_value_conservation_split : Script ()
test_value_conservation_split = do
  issuer <- allocateParty "Issuer"; owner <- allocateParty "Owner"
  cid <- submit issuer do createCmd Iou with issuer; owner; amount = 100.0
  (c1, c2) <- submit owner do exerciseCmd cid Split with splitAmount = 30.0
  Some a1 <- queryContractId owner c1
  Some a2 <- queryContractId owner c2
  -- HARM: children must sum to the parent — a mint/burn breaks conservation
  assert (a1.amount + a2.amount == 100.0)

Template 4: lookupByKey False-None (visibility ≠ absence)

test_lookup_false_none_duplicate : Script ()
test_lookup_false_none_duplicate = do
  issuer <- allocateParty "Issuer"; outsider <- allocateParty "Outsider"
  -- A keyed contract exists but `outsider` is NOT a stakeholder, so cannot see it
  _ <- submit issuer do createCmd Registered with issuer; label = "x"
  -- A choice controlled by `outsider` that does `lookupByKey` will get None (not visible)
  -- and (buggily) treats None as "absent" → mints a duplicate keyed contract
  submit outsider do createAndExerciseCmd (Registrar with p = outsider) (Register with label = "x")
  -- HARM: two contracts now share the same key (uniqueness invariant broken)

Template 5: CID-Capability — Lookalike / Fail-Open / Stale-Brick

test_caller_cid_not_bound : Script ()
test_caller_cid_not_bound = do
  issuer <- allocateParty "Issuer"; attacker <- allocateParty "Attacker"
  good <- submit issuer do createCmd Config with issuer; allowed = True
  evil <- submit attacker do createCmd Config with issuer = attacker; allowed = True
  -- EXPLOIT: choice accepts a caller-supplied `cfg : ContractId Config` and does not
  -- bind it to the trusted issuer → attacker passes their own lookalike config
  op <- submit issuer do createCmd Op with issuer
  submit attacker do exerciseCmd op Run with cfg = evil   -- succeeds with forged capability ⇒ CONFIRMED

Template 6: Privacy / Disclosure (party-scoped query oracle)

test_observer_over_broad : Script ()
test_observer_over_broad = do
  issuer <- allocateParty "Issuer"; owner <- allocateParty "Owner"
  outsider <- allocateParty "Outsider"
  _ <- submit issuer do createCmd Position with issuer; owner; secret = 42
  -- HARM: an outsider who should NOT be a stakeholder can nonetheless see the contract
  cids <- query @Position outsider
  assert (not (null cids))   -- non-empty ⇒ over-broad observer / disclosure CONFIRMED

Template 7: Boundary-Value Scripts (no fuzzer / SAST fallback, Aptos-style)

-- ensure-gap, arithmetic abort, or deadline boundary via a shared helper
runBoundary : Decimal -> Script ()
runBoundary amt = do
  issuer <- allocateParty "Issuer"
  _ <- submit issuer do createCmd Asset with issuer; owner = issuer; amount = amt
  pure ()

boundaryMin : Script ()
boundaryMin = runBoundary 0.0       -- ensure-gap: does a zero-amount contract create?

boundaryNeg : Script ()
boundaryNeg = runBoundary (-1.0)    -- ensure-gap: does a negative-amount contract create?

boundaryMax : Script ()
boundaryMax = runBoundary 9999999999999999.0  -- arithmetic abort downstream ⇒ liveness brick

---

HARM vs MECHANISM (HARD GATE)

Asserting only that a choice CAN be exercised, a contract CAN be created, or a path is reachable is a mechanism test → [CODE-TRACE] at best, NOT [POC-PASS]. A [POC-PASS] requires a HARM assertion:

Class	Required harm assertion
Authorization	ownership/contract moved to attacker without the implied co-auth (query shows transfer)
Choice/Asset	same cid exercised twice (double-spend), or child1.amount + child2.amount /= parent.amount (conservation), or locked contract still moved
CID-capability	forged/lookalike ContractId accepted and harmful state produced; or whitelist-absent fail-open succeeds; or stale CID ⇒ CONTRACT_NOT_FOUND brick
State/key	duplicate keyed contract created via false-None; or exerciseByKey succeeds where maintainer authority should block
Privacy	not (null (query @T outsider)) for a party that should NOT be a stakeholder
Boundary	invalid contract creates (ensure-gap), OR the choice aborts (ArithmeticError, liveness brick), OR a past-deadline action SUCCEEDS

If the harm assertion fails (correct amounts, action blocked, outsider sees nothing) → [POC-FAIL].

---

Dual-Perspective Verification (MANDATORY)

Phase 1 — ATTACKER: Complete submit sequence? Which party does each submit use? What contract/value moves? Compose multiple exerciseCmd in one submit? Which controller/signatory/ensure is missing or bypassable?

Phase 2 — DEFENDER: What controller/signatory authorization blocks this? What ensure precondition rejects the input? What key+maintainer uniqueness prevents the duplicate? Does consuming archival prevent the replay? Does observer scoping prevent the disclosure? Why safe by design?

Phase 3 — VERDICT: Which argument won? If DEFENDER relies on a defense present in one template but ABSENT in a sibling for the same action → defense parity gap → do NOT REFUTE; minimum Medium.

---

Realistic Parameter Validation

Substitute ACTUAL template constants. Apply Rule 10: worst realistic operational state, not current snapshot.

State: 'With real fields [amount type=Decimal, cap=X, deadline=Y] at worst-state
[max holders, min amount, empty observer list], bug triggers when [condition]'
OR: 'With real fields, bug does NOT trigger because [reason: ensure rejects it / controller blocks it / key is unique]'

DAML-specific facts: Int/Decimal THROW on overflow (no silent wrap → liveness/brick, never silent-value) | ensure False ⇒ PreconditionFailed | a consuming choice archives once | maintainers ⊆ signatories | query@T party is party-scoped.

---

Anti-Downgrade Guard (MANDATORY for VS/BLIND findings)

Apply Rule 13's 5-question test BEFORE downgrading severity or marking FALSE_POSITIVE:

1. Who is harmed by this design gap?
2. Can affected parties avoid the harm?
3. Is the gap documented in protocol docs?
4. Could the protocol achieve the same goal without this gap?
5. Does the choice fulfill its stated purpose completely?

HARD RULE: Template A has co-authorization (or an ensure, or an observer scoping) for a choice but sibling Template B lacks it for the same action → defense parity gap, NOT "by design". Minimum severity: Medium.

Severity-modifier caveat (DAML): the "on-chain-only exploit → −1 tier" modifier is EVM-framed. Do NOT auto-downgrade a liveness-brick (Int/Decimal abort) or a privacy-disclosure finding with it — an outsider query@T leak crosses the disclosure boundary and a reachable abort is a liveness consequence.

---

New Observations (MANDATORY)

If during verification you discover a NEW bug not covered by any hypothesis:

• [VER-NEW-1]: {title} — {Module.daml: template/choice} — {brief description}

---

Error Trace Output (MANDATORY for CONTESTED/FALSE_POSITIVE)

• Failure Type: PRECONDITION_FAILED / AUTHORIZATION_ERROR / CONTRACT_NOT_FOUND / NO_SUCH_KEY / ASSERTION_FAILED / INSUFFICIENT_EVIDENCE / COMPILE_ERROR
• Location: {Module}.daml: {template / choice} : {approximate line}
• Error Message: {DAML Script error, e.g., PreconditionFailed, failed to find contract, requires authorizers ... but only ... were given}
• State at Failure: {which parties hold which contracts in the ACS}
• Investigation Question: {What would resolve this}

---

RAG Queries Before PoC (MANDATORY for HIGH/CRITICAL)

1. get_attack_vectors(bug_class="{category}")
2. get_similar_findings(pattern="{vulnerability description}")
3. validate_hypothesis(hypothesis="{finding summary}")
4. search_solodit_live(keywords="{daml canton vulnerability pattern}", impact=["HIGH","CRITICAL"], tags=["DAML","Canton","Daml"], quality_score=3, max_results=15)

Document in output: Attack Vectors Consulted, Similar Exploits Found, Historical Precedent.

RAG Confidence Override

RAG Confidence	Local Verdict	Final Verdict
>= 7/8 matches	FALSE_POSITIVE	CONTESTED (override)
>= 6/8 matches	FALSE_POSITIVE	CONTESTED (override)
< 6/8 matches	FALSE_POSITIVE	FALSE_POSITIVE (allowed)

---

Chain Hypothesis PoC Requirements

Chain hypotheses receive PRIORITY verification. Test the COMPLETE sequence in one Script: (1) execute the enabler submit, (2) assert the postcondition is created via query@T/queryContractId (e.g. the false-None state, the forged config in the ACS), (3) execute the previously-blocked exploit submit, (4) assert the combined impact exceeds either finding alone. Use standard allocateParty + submit setup.

---

Interpreting Results

Test PASSES (harm assertion holds) → Bug CONFIRMED

Test FAILS → Check Why

Failure	Meaning	Action
requires authorizers ... but only ... given	Controller/signatory auth IS present	Re-examine hypothesis (likely REFUTED)
PreconditionFailed	ensure rejected the input	Check if the ensure IS the defense (REFUTE) or if a weaker path bypasses it
failed to find contract (CONTRACT_NOT_FOUND)	Consuming choice already archived it	A double-spend claim is REFUTED; for stale-CID a brick is CONFIRMED
couldn't find key (NO_SUCH_KEY)	Key absent or not visible	Distinguish true-absent vs false-None (visibility)
submitMustFail PASSED	The action was BLOCKED	This proves SAFETY → REFUTES the auth/bypass bug
Wrong amount	Conservation held / setup wrong	Verify Decimal scale and party setup

---

Iteration Protocol

Attempt 1: Direct implementation from hypothesis. Attempt 2: Adjust setup (which party submits, contract field values, command ordering) — keep the SAME exerciseCmd/choice + SAME harm assertion + SAME location. Attempt 3: Re-examine assumptions (controller vs signatory, consuming vs nonconsuming, key visibility). Attempt 4: Verify choice/template signatures in source — do NOT assume EVM/Rust shapes. Attempt 5: Re-read anti-hallucination rules — confirm correct DAML-Script API. After 5 attempts: FALSE_POSITIVE with documented reasoning.

Retry guard: changing WHICH choice is exercised or WHICH query@T is asserted between attempts caps the result at [CODE-TRACE] (it is a different test, not a setup fix).

---

Insufficient Evidence (HALT CONDITIONS)

Before marking REFUTED, check ALL boxes:

• Required-authorizer set verified by reading the actual controller/signatory clauses (not assumed)
• Consume-mode of the choice verified (consuming/nonconsuming/pre/postconsuming) by reading source
• For key findings: maintainer set verified ⊆ signatory set; false-None tested with a genuinely non-stakeholder party
• Missing precondition documented (STATE / ACCESS / TIMING / EXTERNAL / BALANCE)
• Searched other findings for matching postconditions (chain integration)
• For privacy: harm tested with a party-scoped query@T outsider, not a god-view
• ensure clause read directly from source (not assumed present)
• External package (data-dependencies) behavior marked UNVERIFIED, not relied on for REFUTE

Evidence That Does NOT Count

• "Helper template shows X" — helper templates are [MOCK], not the audited templates
• "Choice is nonconsuming" — does not by itself bypass controller authorization
• "Attacker loses by transferring" — may profit via a position held in another template
• "Requires the operator party" — operator may be a compromised key or malicious signatory
• "Key cannot collide" — verify the actual key/maintainer and visibility scope
• "submitMustFail passed" — that proves SAFETY (REFUTES), it is NOT evidence the bug exists

---

Output Format

CONFIRMED

## Verdict: CONFIRMED
### Bug Mechanism Verified
{2-3 sentences on what daml test proves}
### Test Code
{Full Script () using allocateParty/createCmd/exerciseCmd + harm assertion}
### Test Output
{Assertions and ACS values from `daml test --files daml-test/PoC_{id}.daml`}
### Key Evidence
| Metric | Value |
|--------|-------|
| Before / After / Expected / Difference | {which party holds which contract, amounts} |
### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
### Severity: {LEVEL}
{1-2 sentence justification; note liveness/privacy are NOT auto-downgraded}
### Suggested Fix
{diff block + Fix scope + Verified: YES/NO}

FALSE_POSITIVE

## Verdict: FALSE_POSITIVE
### Attempts Made
**Attempt 1-N:** Approach, Result (Failure Type / error message), Learning
### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
### Why It Is Not a Bug
{2-3 sentences — e.g., a passing submitMustFail proved the controller co-auth holds}
### Error Trace
{Failure Type, Location, Error Message, State at Failure, Investigation Question}

CONTESTED

## Verdict: CONTESTED
### Evidence Status
| Checkpoint | Status | Details |
|------------|--------|---------|
| Controller/signatory set verified from source | YES/NO | |
| Consume-mode verified from source | YES/NO | |
| Key maintainer ⊆ signatory verified | YES/NO | |
| Privacy harm tested via party-scoped query@T | YES/NO | |
### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
### Why This Cannot Be REFUTED
{What evidence is missing — e.g., external data-dependency behavior unverified}
### Escalation Required
- [ ] Read actual controller/signatory clauses for {template.choice}
- [ ] Confirm key+maintainer against source
- [ ] Test additional choice paths: {list}
### Error Trace
{as above}