{-# LANGUAGE OverloadedStrings #-}

{- | Threat model for detecting missing OutputDatumHash witness vulnerabilities.

This attack mutates a continuation output from inline datum to @TxOutDatumHash@
with a hash that is not present in @txInfoData@. A secure validator that reads
state from output datum hashes must reject this transaction because it cannot
resolve the hash to actual datum bytes.

== Consequences ==

1. __State resolution failure__: The validator cannot decode continuation state.

2. __Potential fund locking__: If invalid continuation outputs are accepted,
   future spends can fail when state cannot be reconstructed.

== Mitigation ==

A secure validator should reject @OutputDatumHash@ values that cannot be found
in the transaction datum map.
-}
module Convex.ThreatModel.OutputDatumHashMissing (
  outputDatumHashMissingAttack,
  outputDatumHashMissingAttackWith,
) where

import Cardano.Api qualified as C
import Convex.ThreatModel
import Convex.Utils.String (unsafeDatumHash)

-- | Default attack using a deterministic orphaned datum hash.
outputDatumHashMissingAttack :: ThreatModel ()
outputDatumHashMissingAttack :: ThreatModel ()
outputDatumHashMissingAttack =
  Hash ScriptData -> ThreatModel ()
outputDatumHashMissingAttackWith
    (Text -> Hash ScriptData
unsafeDatumHash Text
"deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef")

{- | Attack with configurable orphaned datum hash.

For transactions that spend a script input and create a continuation output with
inline datum at the same script address:

* Replace that output's datum with @TxOutDatumHash@ using @orphanHash@
* Keep the hash absent from @txInfoData@
* If the transaction still validates, the contract does not enforce datum-hash
  resolution safety.
-}
outputDatumHashMissingAttackWith :: C.Hash C.ScriptData -> ThreatModel ()
outputDatumHashMissingAttackWith :: Hash ScriptData -> ThreatModel ()
outputDatumHashMissingAttackWith Hash ScriptData
orphanHash = String -> ThreatModel () -> ThreatModel ()
forall a. String -> ThreatModel a -> ThreatModel a
Named String
"Output Datum Hash Missing Attack" (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ do
  -- Precondition: a script input is spent, so a validator executes.
  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 to same script address with inline datum.
  [Output]
outputs <- ThreatModel [Output]
getTxOutputs
  let continuationInlineOutputs :: [Output]
continuationInlineOutputs =
        (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
hasInlineDatum 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]
continuationInlineOutputs)

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

  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 inline datum."
      ]

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"Testing if the output datum at index"
      , TxIx -> String
forall a. Show a => a -> String
show (Output -> TxIx
outputIx Output
target)
      , String
"can be converted to TxOutDatumHash with an orphaned hash"
      , String
"that is not present in txInfoData."
      ]

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"If this validates, the script may accept output datum hashes without"
      , String
"ensuring the hash resolves in the datum map, which can break state"
      , String
"reconstruction and lead to locked funds."
      ]

  -- 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 (AlonzoEraOnwards Era -> Hash ScriptData -> Datum
forall era ctx.
AlonzoEraOnwards era -> Hash ScriptData -> TxOutDatum ctx era
TxOutDatumHash AlonzoEraOnwards Era
forall era. IsAlonzoBasedEra era => AlonzoEraOnwards era
C.alonzoBasedEra Hash ScriptData
orphanHash)

-- | True when an output uses inline datum.
hasInlineDatum :: Output -> Bool
hasInlineDatum :: Output -> Bool
hasInlineDatum Output
output =
  case TxOut CtxTx Era -> Datum
forall ctx. TxOut ctx Era -> TxOutDatum ctx Era
datumOfTxOut (Output -> TxOut CtxTx Era
outputTxOut Output
output) of
    TxOutDatumInline{} -> Bool
True
    Datum
_ -> Bool
False