{-# 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

Note: the duplicate carries the SAME value as the original output, not just
the same address and datum. This also catches validators that locate "their"
continuation by @list.find@-ing on the output's value (e.g. matching an
expected payout amount) rather than on the datum. The duplicate's ADA is
handled by the test harness's rebalancing (it tops up or draws down the
wallet's change output to absorb whatever a 'TxModifier' adds or removes),
so this attack doesn't need to hand-balance the duplicate itself.

The rebalancing cannot conjure *native tokens*, though: a duplicate of an
output that carries tokens (e.g. a state thread token) needs those tokens
to come from somewhere, and the signing wallet has none, so such
transactions are skipped rather than tested. For a unique thread token that
skip mirrors reality - a real attacker cannot obtain a second copy of the
token either, so the duplicated-output transaction isn't constructible
on-chain in the first place, and a validator that locates its continuation
by that token is not vulnerable to this attack.

== 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
  (the test harness's rebalancing absorbs the duplicate's ADA by adjusting
  the wallet's change output, so this doesn't trip @ValueNotConservedUtxo@;
  a duplicate carrying native tokens the wallet cannot supply is skipped,
  see the module header)
* 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
  -- Require at least two script inputs, mirroring the "Account A and Account
  -- B" attack scenario above. With fewer than two script inputs there is
  -- nothing for a duplicated output to be cross-matched against, so any
  -- validator that simply aggregates value at its own address (rather than
  -- picking "its" output via list.find) would trivially "still validate"
  -- without that indicating a Mutual Exclusion vulnerability.
  --
  -- This is a hard applicability bound, not a harness limitation: the
  -- tempting alternative of *fabricating* a second script input (a sibling
  -- account the attacker created) doesn't produce a sound test. The sibling
  -- has to be funded by the attacker, so for an aggregate-value validator
  -- the two-identical-inputs transaction validates legitimately - the
  -- attacker merely gets their own funding back, and flagging that would be
  -- a false positive. Cross-matching is only meaningfully testable on
  -- transactions that *organically* spend two or more script inputs (the
  -- account-style contracts this attack was written for); contracts whose
  -- transactions never do should not list this model.
  [Input]
inputs <- ThreatModel [Input]
getTxInputs
  let scriptInputs :: [Input]
scriptInputs = (Input -> Bool) -> [Input] -> [Input]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Input -> Bool) -> Input -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AddressAny -> Bool
isKeyAddressAny (AddressAny -> Bool) -> (Input -> AddressAny) -> Input -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Input -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf) [Input]
inputs
  ThreatModel () -> ThreatModel ()
forall a. ThreatModel a -> ThreatModel a
threatPrecondition (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ Bool -> ThreatModel ()
ensure ([Input] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Input]
scriptInputs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2)

  -- 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