convex-testing-interface
Safe HaskellSafe-Inferred
LanguageHaskell2010

Convex.ThreatModel.MutualExclusion

Description

Threat model for detecting Mutual Exclusion vulnerabilities.

A Mutual Exclusion Attack exploits validators that use list.find or similar functions to locate "their" continuation output without enforcing uniqueness. When multiple inputs try to match outputs by property (e.g., same owner, same script address), having duplicate outputs allows cross-matching between different inputs.

Example Vulnerability ==

Consider an account validator that locates its continuation by finding an output with the same owner:

  -- Aiken pseudocode
  let my_output = outputs |> list.find(fn(o) { o.datum.owner == my_owner })

If an attacker creates two identical outputs, two different account inputs can both "find" the same output (or each find a different one that doesn't actually correspond to their input).

Attack Scenario ==

  1. Transaction spends Account A (owner: Alice) and Account B (owner: Bob)
  2. Original outputs: Output A' (owner: Alice), Output B' (owner: Bob)
  3. Attack: Duplicate Output A' so we have two outputs with owner: Alice
  4. Now Account A and Account B can both claim Output A' as "theirs" since list.find returns the first match
  5. This breaks the 1:1 correspondence between inputs and outputs

Consequences ==

  1. Cross-matching: Input A claims Output B's value, Input B claims nothing
  2. State corruption: Multiple inputs modify the same output
  3. Fund theft: Attacker can redirect funds by manipulating which input matches which output

Root Cause ==

Validators that: - Use list.find to locate continuations without enforcing uniqueness - Match outputs by datum properties without checking index correspondence - Don't verify that each input has exactly one matching output

Mitigation ==

A secure validator should: - Use index-based matching (output[i] corresponds to input[i]) - Verify no duplicate outputs exist with the same matching criteria - Use list.filter and check exactly one result

This threat model tests if duplicating a script continuation output still allows the transaction to validate. If it does, the validator has a Mutual Exclusion vulnerability.

Synopsis

Documentation

mutualExclusionAttack :: ThreatModel () Source #

Check for Mutual Exclusion vulnerabilities by duplicating script outputs.

For a transaction with script continuation outputs:

  • Find a script output (continuation) that goes back to a script address
  • Duplicate it — add another output with the SAME address, value, and datum
  • If the transaction still validates, the script doesn't properly enforce mutual exclusion between inputs and outputs

This catches vulnerability patterns in bank_02 and bank_03 where multiple account inputs can cross-match outputs because the validator uses list.find without enforcing uniqueness.