{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}

{- | 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.
-}
module Convex.ThreatModel.MutualExclusion (
  mutualExclusionAttack,
) where

import Convex.ThreatModel

{- | 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.
-}
mutualExclusionAttack :: ThreatModel ()
mutualExclusionAttack :: ThreatModel ()
mutualExclusionAttack = String -> ThreatModel () -> ThreatModel ()
forall a. String -> ThreatModel a -> ThreatModel a
Named String
"Mutual Exclusion Attack" (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ do
  -- Get all outputs from the transaction
  [Output]
outputs <- ThreatModel [Output]
getTxOutputs

  -- Filter to script outputs (NOT key addresses) - these are continuations
  let scriptOutputs :: [Output]
scriptOutputs = (Output -> Bool) -> [Output] -> [Output]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Output -> Bool) -> Output -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AddressAny -> Bool
isKeyAddressAny (AddressAny -> Bool) -> (Output -> AddressAny) -> Output -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Output -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf) [Output]
outputs

  -- Precondition: there must be at least one script output to duplicate
  ThreatModel () -> ThreatModel ()
forall a. ThreatModel a -> ThreatModel a
threatPrecondition (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ Bool -> ThreatModel ()
ensure (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Output] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Output]
scriptOutputs)

  -- Pick a target script output to duplicate
  Output
target <- [Output] -> ThreatModel Output
forall a. Show a => [a] -> ThreatModel a
pickAny [Output]
scriptOutputs

  -- Get the details of the target output
  let targetAddr :: AddressAny
targetAddr = Output -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf Output
target
      targetValue :: Value
targetValue = Output -> Value
forall t. IsInputOrOutput t => t -> Value
valueOf Output
target
      targetRefScript :: ReferenceScript Era
targetRefScript = Output -> ReferenceScript Era
forall t. IsInputOrOutput t => t -> ReferenceScript Era
refScriptOf Output
target

  -- Get the datum from the output (need to handle the Output wrapper)
  let targetDatum :: TxOutDatum CtxTx Era
targetDatum = case TxOut CtxTx Era -> TxOutDatum CtxTx Era
forall ctx. TxOut ctx Era -> TxOutDatum ctx Era
datumOfTxOut (Output -> TxOut CtxTx Era
outputTxOut Output
target) of
        TxOutDatum CtxTx Era
TxOutDatumNone -> TxOutDatum CtxTx Era
forall ctx era. TxOutDatum ctx era
TxOutDatumNone
        TxOutDatumHash AlonzoEraOnwards Era
s Hash ScriptData
h -> AlonzoEraOnwards Era -> Hash ScriptData -> TxOutDatum CtxTx Era
forall era ctx.
AlonzoEraOnwards era -> Hash ScriptData -> TxOutDatum ctx era
TxOutDatumHash AlonzoEraOnwards Era
s Hash ScriptData
h
        TxOutDatumInline BabbageEraOnwards Era
s HashableScriptData
d -> BabbageEraOnwards Era -> HashableScriptData -> TxOutDatum CtxTx Era
forall era ctx.
BabbageEraOnwards era -> HashableScriptData -> TxOutDatum ctx era
TxOutDatumInline BabbageEraOnwards Era
s HashableScriptData
d
        TxOutSupplementalDatum AlonzoEraOnwards Era
s HashableScriptData
d -> AlonzoEraOnwards Era -> HashableScriptData -> TxOutDatum CtxTx Era
forall era.
AlonzoEraOnwards era -> HashableScriptData -> TxOutDatum CtxTx era
TxOutSupplementalDatum AlonzoEraOnwards Era
s HashableScriptData
d

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"The transaction contains a script output at index"
      , TxIx -> String
forall a. Show a => a -> String
show (Output -> TxIx
outputIx Output
target)
      , String
"going to"
      , Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ AddressAny -> Doc
prettyAddress AddressAny
targetAddr
      , String
"."
      ]

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"Testing if this output can be duplicated - adding another output with"
      , String
"IDENTICAL address, value, and datum."
      ]

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"If this validates, the script has a Mutual Exclusion vulnerability."
      , String
"Multiple script inputs could cross-match outputs when using list.find"
      , String
"to locate 'their' continuation, since duplicate outputs would match"
      , String
"the same criteria."
      ]

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"An attacker could exploit this to:"
      , String
"1) Have multiple inputs claim the same output as 'theirs'"
      , String
"2) Break the 1:1 correspondence between inputs and outputs"
      , String
"3) Redirect funds by manipulating input-output matching"
      ]

  -- The attack: add a duplicate output with the same address, value, datum
  -- If the tx validates with duplicate continuation outputs, the validator
  -- can't properly match inputs to outputs
  TxModifier -> ThreatModel ()
shouldNotValidate (TxModifier -> ThreatModel ()) -> TxModifier -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ AddressAny
-> Value
-> TxOutDatum CtxTx Era
-> ReferenceScript Era
-> TxModifier
addOutput AddressAny
targetAddr Value
targetValue TxOutDatum CtxTx Era
targetDatum ReferenceScript Era
targetRefScript