Verification Protocol

Verification Protocol (Sui Move)

Trigger Pattern: Always (used by all verifier agents) Inject Into: security-verifier agents (Phase 5) Purpose: Prove hypotheses TRUE or FALSE using Sui Move test framework with test_scenario PoC code.

Evidence Source Tracking (MANDATORY)

CRITICAL: For EVERY piece of evidence used in verification, you MUST tag its source. Evidence from mocks or unverified external packages CANNOT support a REFUTED verdict.

Evidence Source Tags

Evidence Audit Table (REQUIRED in every verification output)

Before ANY verdict, fill this table:

### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
|-------|-----------------|-----|-------------------|
| "External package returns X" | Mock module | [MOCK] | NO |
| "Object ownership is Y" | sources/module.move:123 | [CODE] | YES |
| "Shared object state is Z" | Sui Explorer object view | [PROD-ONCHAIN] | YES |

Mock Rejection Rule

AUTOMATIC OVERRIDE: If ANY evidence supporting REFUTED has tag [MOCK] or [EXT-UNV]:

• CANNOT return REFUTED
• MUST return CONTESTED
• Triggers production verification

Example:

## Verdict: REFUTED -> CONTESTED (mock evidence override)

### Evidence Audit
| Claim | Source | Tag | Valid? |
|-------|--------|-----|--------|
| "External module validates input" | test_helper.move:45 | [MOCK] | NO |

**Override reason**: REFUTED verdict relies on mock behavior at test_helper.move:45.
Production package behavior is UNVERIFIED. Must fetch published package source.

Pre-Verification Understanding

Before writing ANY test code, you MUST answer:

Question 1: What is the EXACT bug?

NOT: "Object ownership is wrong"
NOT: "Access control is missing"
NOT: "State is inconsistent"

YES: "Function [X] in module [Y] accepts shared object [Z] as `&mut` without
      verifying caller holds [CapabilityType], allowing any address to mutate
      field [W] at line [N]"

Question 2: What OBSERVABLE difference proves it?

NOT: "State changed"
NOT: "Object was modified"

YES: "Before exploit: pool.total_supply = 1000, attacker_balance = 0
      After exploit: pool.total_supply = 1000, attacker_balance = 500
      Expected: transaction should have aborted with ENotAuthorized"

Question 3: What is the EXACT assertion?

NOT: assert!(exploit_worked, 0)

YES: assert!(coin::value(&stolen_coin) > 0, ERR_EXPLOIT_FAILED)
 OR: // Transaction should abort -- if it succeeds, the bug exists
 OR: assert!(state_after.field != state_before.field, ERR_STATE_UNCHANGED)

If you cannot answer all three -> ASK FOR CLARIFICATION

Pre-PoC Feasibility Gates (MANDATORY)

Before writing test code, verify these two gates. If either FAILS, adjust the hypothesis.

Gate F1: Reachability

Trace a call path from a permissionless entry point to the vulnerable code.

• Entry point identified (public/external/entry function)
• Call path traced through intermediary functions
• All access checks on the path are passable by the attacker profile

If NO entry point reaches the vulnerable code → UNREACHABLE → FALSE_POSITIVE. If reachable only through a restricted path → document the restriction, adjust likelihood.

Gate F2: Math Bounds

Substitute real-world value domains into the expression that triggers the bug.

• Parameter domains identified (token decimals, max supply, TVL range, fee range, time bounds)
• Expression evaluated at worst-case feasible inputs
• Result crosses the bug threshold

If the bug requires values outside feasible domains → INFEASIBLE → FALSE_POSITIVE. If feasible only at extreme but realistic parameters → document the threshold, proceed with adjusted severity.

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

Test File Templates

See templates.md in this directory for all Sui Move test templates (Templates 1-6: shared object mutation, capability theft, dynamic fields, object wrapping, PTB exploit, concurrent access).

Interpreting Results

Test PASSES -> Bug CONFIRMED

The assertion that "proves the bug" succeeded.

Test FAILS -> Check Why

Iteration Protocol

Attempt 1: Direct implementation of test strategy from hypothesis.

Attempt 2: Adjust parameters:

• Different coin amounts (larger/smaller, edge values like 0, 1, u64::MAX)
• Different transaction ordering (swap next_tx blocks)
• Different actor addresses
• Different object states (empty pool, full pool, single-user, multi-user)

Attempt 3: Re-examine assumptions:

• Are shared objects properly published in setup?
• Are capability objects at the right addresses?
• Is the module's initialization complete (all shared objects created)?
• Are type parameters correct (generic type instantiation)?
• Does the function require a Clock or TxContext argument not provided?

After 5 attempts: If still fails -> FALSE_POSITIVE with documented reasoning.

Severity Determination

CRITICAL

• Direct fund theft (Coin drain from shared pools)
• Unauthorized admin capability acquisition
• Arbitrary package upgrade (if upgrade cap compromised and no timelock)
• No special prerequisites needed
• Attacker profits significantly

HIGH

• Fund loss with specific setup (object pre-creation, ordering dependency)
• Broken core functionality (deposits, withdrawals, swaps, liquidations)
• Shared object state corruption affecting all users
• Significant TVL at risk

MEDIUM

• Limited fund loss under specific conditions
• Object state corruption (non-fund data)
• Edge cases with real impact at design limits
• Dynamic field pollution affecting protocol behavior
• Moderate value at risk

LOW

• Negligible direct impact
• Extreme edge cases only
• Admin-controlled risk (with multisig governance)
• View function / event emission issues
• Stranded non-value objects

Exchange Rate Finding Severity (MANDATORY)

CRITICAL: Before assigning severity to ANY finding affecting share/asset ratios or exchange rates, you MUST complete this quantitative analysis.