{-# LANGUAGE OverloadedStrings #-}

{- | Threat model for detecting missing integer boundary checks.

A Negative Integer Attack exploits validators that don't check integer bounds
(e.g., @balance >= 0@). The attack negates integer fields in output datums,
which may reveal that the validator allows negative values where only positive
values make semantic sense.

== Consequences ==

1. __Logical state corruption__: If a validator allows negative balances,
   users can withdraw more than they deposited, draining funds from a pool.

2. __Protocol invariant violation__: Counters, timestamps, or other fields
   that should be monotonic or non-negative can be corrupted.

== Vulnerable Patterns ==

=== Pattern: Missing balance check ===

@
// Vulnerable: no check that balance >= 0
let new_balance = input_balance - withdrawal_amount
expect output_datum.balance == new_balance
@

An attacker with @balance = 0@ can withdraw funds, creating @balance = -100@.
The validator doesn't reject this because it never checks @balance >= 0@.

== Mitigation ==

A secure validator should:

- Explicitly check @balance >= 0@ or appropriate bounds for all integer fields
- Validate that counters only increase (or decrease within bounds)
- Use unsigned integers where semantically appropriate (though Plutus uses Integer)

This threat model tests if a script output with an inline datum still validates
when integer fields are negated.
-}
module Convex.ThreatModel.NegativeInteger (
  -- * Negative integer attack
  negativeIntegerAttack,
  negateIntegers,
) where

import Convex.ThreatModel

{- | Check for missing integer boundary checks.

For a transaction with script outputs containing inline datums:

* Recursively negate all @ScriptDataNumber@ fields in the datum
* If the transaction still validates, the script doesn't enforce
  proper bounds checking on integer fields.

This catches vulnerabilities where validators allow negative values
for fields like balances, counters, or timestamps that should be non-negative.

@
negativeIntegerAttack  -- Negate all integers in the datum
@
-}
negativeIntegerAttack :: ThreatModel ()
negativeIntegerAttack :: ThreatModel ()
negativeIntegerAttack = String -> ThreatModel () -> ThreatModel ()
forall a. String -> ThreatModel a -> ThreatModel a
Named String
"Negative Integer 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 with inline datums
  let scriptOutputsWithDatum :: [Output]
scriptOutputsWithDatum = (Output -> Bool) -> [Output] -> [Output]
forall a. (a -> Bool) -> [a] -> [a]
filter Output -> Bool
isScriptOutputWithInlineDatum [Output]
outputs

  -- Precondition: there must be at least one script output with inline datum
  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]
scriptOutputsWithDatum)

  -- Pick a target output
  Output
target <- [Output] -> ThreatModel Output
forall a. Show a => [a] -> ThreatModel a
pickAny [Output]
scriptOutputsWithDatum

  -- Extract the inline datum (we know it exists due to the filter)
  ScriptData
originalDatum <- case Output -> Maybe ScriptData
getInlineDatum Output
target of
    Maybe ScriptData
Nothing -> String -> ThreatModel ScriptData
forall a. String -> ThreatModel a
failPrecondition String
"Script output missing inline datum"
    Just ScriptData
originalDatum' -> ScriptData -> ThreatModel ScriptData
forall a. a -> ThreatModel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ScriptData
originalDatum'

  let negatedDatum :: ScriptData
negatedDatum = ScriptData -> ScriptData
negateIntegers ScriptData
originalDatum

  -- Only proceed if something actually changed (datum has integers to negate)
  ThreatModel () -> ThreatModel ()
forall a. ThreatModel a -> ThreatModel a
threatPrecondition (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ Bool -> ThreatModel ()
ensure (ScriptData
negatedDatum ScriptData -> ScriptData -> Bool
forall a. Eq a => a -> a -> Bool
/= ScriptData
originalDatum)

  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
"with an inline datum containing integer fields."
      ]

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"Testing if negating the integers in the datum"
      , String
"still passes validation."
      ]

  String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
paragraph
      [ String
"If this validates, the script doesn't enforce integer bounds."
      , String
"An attacker could exploit this to:"
      , String
"1) Create negative balances (withdraw more than deposited)"
      , String
"2) Corrupt counters or timestamps"
      , String
"3) Violate protocol invariants"
      ]

  -- Try to validate with the negated datum
  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 (ScriptData -> Datum
toInlineDatum ScriptData
negatedDatum)

{- | Recursively negate all integer fields in a @ScriptData@ value.

For @ScriptDataNumber n@, returns @ScriptDataNumber (negate n)@.

Recursively processes @ScriptDataConstructor@ fields, lists, and maps.

For other @ScriptData@ variants (Bytes), returns the value unchanged.
-}
negateIntegers :: ScriptData -> ScriptData
negateIntegers :: ScriptData -> ScriptData
negateIntegers (ScriptDataConstructor Integer
idx [ScriptData]
fields) =
  Integer -> [ScriptData] -> ScriptData
ScriptDataConstructor Integer
idx ((ScriptData -> ScriptData) -> [ScriptData] -> [ScriptData]
forall a b. (a -> b) -> [a] -> [b]
map ScriptData -> ScriptData
negateIntegers [ScriptData]
fields)
negateIntegers (ScriptDataList [ScriptData]
items) =
  [ScriptData] -> ScriptData
ScriptDataList ((ScriptData -> ScriptData) -> [ScriptData] -> [ScriptData]
forall a b. (a -> b) -> [a] -> [b]
map ScriptData -> ScriptData
negateIntegers [ScriptData]
items)
negateIntegers (ScriptDataMap [(ScriptData, ScriptData)]
entries) =
  [(ScriptData, ScriptData)] -> ScriptData
ScriptDataMap [(ScriptData -> ScriptData
negateIntegers ScriptData
k, ScriptData -> ScriptData
negateIntegers ScriptData
v) | (ScriptData
k, ScriptData
v) <- [(ScriptData, ScriptData)]
entries]
negateIntegers (ScriptDataNumber Integer
n) =
  Integer -> ScriptData
ScriptDataNumber (Integer -> Integer
forall a. Num a => a -> a
negate Integer
n)
negateIntegers ScriptData
x = ScriptData
x -- bytes, etc. unchanged

-- | Check if an output is a script output with an inline datum.
isScriptOutputWithInlineDatum :: Output -> Bool
isScriptOutputWithInlineDatum :: Output -> Bool
isScriptOutputWithInlineDatum Output
output =
  Bool -> Bool
not (AddressAny -> Bool
isKeyAddressAny (Output -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf Output
output)) Bool -> Bool -> Bool
&& Output -> Bool
hasInlineDatum Output
output

-- | Check if an output has an 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

-- | Extract the inline datum from an output if present.
getInlineDatum :: Output -> Maybe ScriptData
getInlineDatum :: Output -> Maybe ScriptData
getInlineDatum 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 BabbageEraOnwards Era
_ HashableScriptData
hashableData -> ScriptData -> Maybe ScriptData
forall a. a -> Maybe a
Just (HashableScriptData -> ScriptData
getScriptData HashableScriptData
hashableData)
    Datum
_ -> Maybe ScriptData
forall a. Maybe a
Nothing

-- | Convert a @ScriptData@ to an inline @Datum@ (TxOutDatum CtxTx Era).
toInlineDatum :: ScriptData -> Datum
toInlineDatum :: ScriptData -> Datum
toInlineDatum ScriptData
sd =
  BabbageEraOnwards Era -> HashableScriptData -> Datum
forall era ctx.
BabbageEraOnwards era -> HashableScriptData -> TxOutDatum ctx era
TxOutDatumInline BabbageEraOnwards Era
BabbageEraOnwardsConway (ScriptData -> HashableScriptData
unsafeHashableScriptData ScriptData
sd)