{-# 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
  (Output
target, ScriptData
originalDatum) <- ThreatModel (Output, ScriptData)
anyGuardedOutputWithInlineDatum

  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