{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedStrings #-}

{- | Threat model for detecting Value Underpayment vulnerabilities.

A Value Underpayment Attack exploits validators that don't properly verify
that the actual ADA value in an output matches the expected value based on
the datum. If a validator tracks a "balance" in the datum but doesn't verify
the actual ADA matches, an attacker can modify transactions to underpay.

== Example Vulnerability ==

Consider a bank contract where the account datum tracks a balance:

@
data AccountDatum = AccountDatum { balance :: Integer, owner :: PubKeyHash }
@

If the deposit action (IncreaseBalance) only checks that:
- The output datum has an increased balance
- But doesn't verify that the actual ADA value increased by the same amount

Then an attacker can "deposit" by increasing the datum balance without
adding any actual ADA to the output.

== Consequences ==

1. __Free balance increases__: Attacker gains balance without depositing funds
2. __Theft of pooled funds__: If the bank pays out based on datum balance,
   the attacker can withdraw more than they deposited
3. __Insolvency__: Multiple attackers can drain the bank's pooled funds

== Root Cause ==

Validators that:
- Track value in datum without verifying actual UTxO value matches
- Only check datum changes without checking corresponding value changes
- Allow balance increases without requiring matching fund increases

== Mitigation ==

A secure validator should:
- Verify output value matches expected value based on datum
- Check that fund_difference == balance_change for deposits/withdrawals
- Never rely solely on datum for balance tracking

This threat model tests if a script output can have its ADA value reduced
while keeping the datum unchanged. If the transaction still validates,
the validator has a Value Underpayment vulnerability.
-}
module Convex.ThreatModel.ValueUnderpayment (
  valueUnderpaymentAttack,
  valueUnderpaymentAttackWith,
) where

import Cardano.Api qualified as C
import Convex.ThreatModel

-- | Minimum ADA to leave in the output (to avoid min-UTxO violations)
minOutputAda :: C.Lovelace
minOutputAda :: Lovelace
minOutputAda = Lovelace
2_000_000

{- | Check for Value Underpayment vulnerabilities by halving the ADA value.

This is the default configuration that reduces the ADA in a script output
by 50%. If the transaction still validates, the script doesn't properly
verify that output values match expected amounts.
-}
valueUnderpaymentAttack :: ThreatModel ()
valueUnderpaymentAttack :: ThreatModel ()
valueUnderpaymentAttack = Double -> ThreatModel ()
valueUnderpaymentAttackWith Double
0.5

{- | Check for Value Underpayment vulnerabilities with a configurable
reduction factor.

For a transaction with script outputs:

* Find a script output with ADA value
* Reduce its ADA value by the given factor (e.g., 0.5 = halve it)
* Keep the datum unchanged
* If the transaction still validates, the script doesn't verify
  that output value matches the expected amount based on datum.

@reductionFactor@ should be between 0 and 1:
- 0.5 means reduce to 50% of original value
- 0.25 means reduce to 25% of original value
- 0.9 means reduce to 10% of original value (keep only 10%)

The attack ensures at least 'minOutputAda' remains to avoid min-UTxO failures.
-}
valueUnderpaymentAttackWith :: Double -> ThreatModel ()
valueUnderpaymentAttackWith :: Double -> ThreatModel ()
valueUnderpaymentAttackWith Double
reductionFactor = [Char] -> ThreatModel () -> ThreatModel ()
forall a. [Char] -> ThreatModel a -> ThreatModel a
Named ([Char]
"Value Underpayment Attack (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Double
reductionFactor Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
100) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"% reduction)") (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 (NOT key addresses)
  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
  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)

  -- Further filter to outputs that have enough ADA to be reduced
  let hasEnoughAda :: p -> Bool
hasEnoughAda p
out =
        let adaValue :: Lovelace
adaValue = Value -> Lovelace
C.selectLovelace (p -> Value
forall t. IsInputOrOutput t => t -> Value
valueOf p
out)
         in Lovelace
adaValue Lovelace -> Lovelace -> Bool
forall a. Ord a => a -> a -> Bool
> Lovelace
minOutputAda
      reducibleOutputs :: [Output]
reducibleOutputs = (Output -> Bool) -> [Output] -> [Output]
forall a. (a -> Bool) -> [a] -> [a]
filter Output -> Bool
forall {p}. IsInputOrOutput p => p -> Bool
hasEnoughAda [Output]
scriptOutputs

  -- Precondition: there must be at least one script output with enough ADA
  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]
reducibleOutputs)

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

  -- Calculate reduced value
  let currentValue :: Value
currentValue = Output -> Value
forall t. IsInputOrOutput t => t -> Value
valueOf Output
target
      currentAda :: Lovelace
currentAda = Value -> Lovelace
C.selectLovelace Value
currentValue
      -- Calculate reduced ADA, ensuring we don't go below minimum
      -- Lovelace has a Num instance, so we can use numeric operations
      reducedAda :: Lovelace
reducedAda = Lovelace -> Lovelace -> Lovelace
forall a. Ord a => a -> a -> a
max Lovelace
minOutputAda (Integer -> Lovelace
forall a. Num a => Integer -> a
fromInteger (Integer -> Lovelace) -> Integer -> Lovelace
forall a b. (a -> b) -> a -> b
$ Double -> Integer
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
round (Lovelace -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Lovelace
currentAda Double -> Double -> Double
forall a. Num a => a -> a -> a
* (Double
1 Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
reductionFactor)))
      adaDifference :: Value
adaDifference = Value -> Value
C.negateValue (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$ Lovelace -> Value
C.lovelaceToValue (Lovelace
currentAda Lovelace -> Lovelace -> Lovelace
forall a. Num a => a -> a -> a
- Lovelace
reducedAda)
      reducedValue :: Value
reducedValue = Value
currentValue Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> Value
adaDifference

  [Char] -> ThreatModel ()
counterexampleTM ([Char] -> ThreatModel ()) -> [Char] -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [[Char]] -> [Char]
paragraph
      [ [Char]
"The transaction contains a script output at index"
      , TxIx -> [Char]
forall a. Show a => a -> [Char]
show (Output -> TxIx
outputIx Output
target)
      , [Char]
"."
      ]

  [Char] -> ThreatModel ()
counterexampleTM ([Char] -> ThreatModel ()) -> [Char] -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [[Char]] -> [Char]
paragraph
      [ [Char]
"Testing if the ADA value can be reduced from"
      , Lovelace -> [Char]
forall a. Show a => a -> [Char]
show Lovelace
currentAda
      , [Char]
"to"
      , Lovelace -> [Char]
forall a. Show a => a -> [Char]
show Lovelace
reducedAda
      , [Char]
"(reduction factor:"
      , Double -> [Char]
forall a. Show a => a -> [Char]
show (Double
reductionFactor Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
100) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"%)"
      , [Char]
"while keeping the datum unchanged."
      ]

  [Char] -> ThreatModel ()
counterexampleTM ([Char] -> ThreatModel ()) -> [Char] -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [[Char]] -> [Char]
paragraph
      [ [Char]
"If this validates, the script's value validation is insufficient."
      , [Char]
"An attacker could exploit this to:"
      , [Char]
"1) Increase their balance without depositing matching funds"
      , [Char]
"2) Steal funds from pooled reserves"
      , [Char]
"3) Create inconsistency between datum balance and actual UTxO value"
      ]

  -- This SHOULD fail - if it validates, the contract is vulnerable
  -- The attack: reduce the ADA value but keep datum the same
  TxModifier -> ThreatModel ()
shouldNotValidate (TxModifier -> ThreatModel ()) -> TxModifier -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ Output -> Value -> TxModifier
forall t. IsInputOrOutput t => t -> Value -> TxModifier
changeValueOf Output
target Value
reducedValue