{-# LANGUAGE OverloadedStrings #-}

{- | Threat model for detecting Missing Output Datum vulnerabilities.

A Missing Output Datum Attack targets state-machine validators that require a
continuation output to carry a valid datum. If the validator does not enforce
that requirement, an attacker can remove the datum from the continuation
output and still have the transaction validate.

== Consequences ==

1. __State corruption__: The next contract state cannot be reconstructed from
   the continuation output.

2. __Permanent fund locking__: Future spends may fail because the validator
   cannot decode the expected state from a missing datum.

== Mitigation ==

A secure validator should explicitly reject continuation outputs without datum
(e.g. @NoOutputDatum@) and ensure stateful outputs always include valid datum.

This threat model mutates a continuation output by replacing its datum with
@TxOutDatumNone@. If the transaction still validates, the script may be
vulnerable.
-}
module Convex.ThreatModel.MissingOutputDatum (
  missingOutputDatumAttack,
) where

import Convex.ThreatModel

{- | Check for Missing Output Datum vulnerabilities.

For a transaction that spends a script input and creates a continuation output
back to the same script address with a datum:

* Remove the continuation output datum (@TxOutDatumNone@)
* If the transaction still validates, the script does not enforce that
  continuation outputs carry state datum.
-}
missingOutputDatumAttack :: ThreatModel ()
missingOutputDatumAttack :: ThreatModel ()
missingOutputDatumAttack = String -> ThreatModel () -> ThreatModel ()
forall a. String -> ThreatModel a -> ThreatModel a
Named String
"Missing Output Datum Attack" (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ do
  -- Precondition: a script input is spent, so a validator runs.
  Input
scriptInput <- (Input -> Bool) -> ThreatModel Input
anyInputSuchThat (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)
  let scriptAddr :: AddressAny
scriptAddr = Input -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf Input
scriptInput

  -- Candidate targets: continuation outputs back to the same script address
  -- that currently have some datum.
  [Output]
outputs <- ThreatModel [Output]
getTxOutputs
  let continuationOutputsWithDatum :: [Output]
continuationOutputsWithDatum =
        (Output -> Bool) -> [Output] -> [Output]
forall a. (a -> Bool) -> [a] -> [a]
filter
          (\Output
o -> Output -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf Output
o AddressAny -> AddressAny -> Bool
forall a. Eq a => a -> a -> Bool
== AddressAny
scriptAddr Bool -> Bool -> Bool
&& Output -> Bool
hasOutputDatum Output
o)
          [Output]
outputs

  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]
continuationOutputsWithDatum)

  Output
target <- [Output] -> ThreatModel Output
forall a. Show a => [a] -> ThreatModel a
pickAny [Output]
continuationOutputsWithDatum

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"The transaction spends a script input at"
      , Doc -> String
forall a. Show a => a -> String
show (AddressAny -> Doc
prettyAddress AddressAny
scriptAddr)
      , String
"and creates a continuation output with datum."
      ]

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"Testing if the continuation output at index"
      , TxIx -> String
forall a. Show a => a -> String
show (Output -> TxIx
outputIx Output
target)
      , String
"can have its datum removed (TxOutDatumNone) while still validating."
      ]

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"If this validates, the script does not enforce datum presence on"
      , String
"continuation outputs. This can break state tracking and potentially"
      , String
"lock funds in an unspendable state."
      ]

  -- This SHOULD fail. If it validates, the script is vulnerable.
  TxModifier -> ThreatModel ()
shouldNotValidate (TxModifier -> ThreatModel ()) -> TxModifier -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ Output -> Datum -> TxModifier
forall t. IsInputOrOutput t => t -> Datum -> TxModifier
changeDatumOf Output
target Datum
forall ctx era. TxOutDatum ctx era
TxOutDatumNone

-- | True when an output carries any datum variant except TxOutDatumNone.
hasOutputDatum :: Output -> Bool
hasOutputDatum :: Output -> Bool
hasOutputDatum Output
output =
  case TxOut CtxTx Era -> Datum
forall ctx. TxOut ctx Era -> TxOutDatum ctx Era
datumOfTxOut (Output -> TxOut CtxTx Era
outputTxOut Output
output) of
    Datum
TxOutDatumNone -> Bool
False
    Datum
_ -> Bool
True