{-# 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,
  valueUnderpaymentAttackWithGen,
) where

import Cardano.Api qualified as C
import Convex.ThreatModel
import Test.QuickCheck (Gen, choose, shrinkRealFrac)

{- | Default value-underpayment attack. The reduction factor is drawn per
transaction from a curated range, so QuickCheck explores the parameter space
and shrinks counterexamples toward the smallest triggering value.
-}
valueUnderpaymentAttack :: ThreatModel ()
valueUnderpaymentAttack :: ThreatModel ()
valueUnderpaymentAttack = Gen Double -> ThreatModel ()
valueUnderpaymentAttackWithGen ((Double, Double) -> Gen Double
forall a. Random a => (a, a) -> Gen a
choose (Double
0.01, Double
0.99))

{- | Value-underpayment attack with a fixed reduction factor. Keep using
this for deterministic regression tests and golden seeds.
-}
valueUnderpaymentAttackWith :: Double -> ThreatModel ()
valueUnderpaymentAttackWith :: Double -> ThreatModel ()
valueUnderpaymentAttackWith = Gen Double -> ThreatModel ()
valueUnderpaymentAttackWithGen (Gen Double -> ThreatModel ())
-> (Double -> Gen Double) -> Double -> ThreatModel ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Gen Double
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

{- | Value-underpayment attack parameterised by a generator for the ADA
reduction factor (fraction of the original ADA removed from a script output).
This is the primitive the other two forms delegate to.
-}
valueUnderpaymentAttackWithGen :: Gen Double -> ThreatModel ()
valueUnderpaymentAttackWithGen :: Gen Double -> ThreatModel ()
valueUnderpaymentAttackWithGen Gen Double
reductionFactorGen =
  [Char] -> ThreatModel () -> ThreatModel ()
forall a. [Char] -> ThreatModel a -> ThreatModel a
Named [Char]
"Value Underpayment Attack" (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ do
    Double
reductionFactor <- Gen Double -> (Double -> [Double]) -> ThreatModel Double
forall a. Show a => Gen a -> (a -> [a]) -> ThreatModel a
forAllTM Gen Double
reductionFactorGen Double -> [Double]
shrinkPositiveDouble

    -- Skip iterations where the draw is too small to be a meaningful attack.
    Bool -> ThreatModel ()
ensure (Double
reductionFactor Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
0)

    {- The floor for the reduced ADA amount has to be each output's own
    protocol-mandated minimum, not a hardcoded guess: 'rebalanceAndSign' runs
    'Convex.ThreatModel.Cardano.Api.topUpUnderfundedOutputs' on every output
    before validation, which would silently restore ADA a reduction below
    that real minimum, masking a genuine underpayment vulnerability behind a
    false "still passes". Flooring at the real minimum here means the
    reduced output is never below it, so that top-up is a no-op and the
    deliberate reduction reaches the validator intact.
    -}
    LedgerProtocolParameters Era
envPParams <- ThreatModelEnv -> LedgerProtocolParameters Era
pparams (ThreatModelEnv -> LedgerProtocolParameters Era)
-> ThreatModel ThreatModelEnv
-> ThreatModel (LedgerProtocolParameters Era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThreatModel ThreatModelEnv
getThreatModelEnv
    let minRequiredAda :: Output -> Lovelace
minRequiredAda Output
out = ShelleyBasedEra Era
-> PParams (ShelleyLedgerEra Era) -> TxOut CtxTx Era -> Lovelace
forall era.
HasCallStack =>
ShelleyBasedEra era
-> PParams (ShelleyLedgerEra era) -> TxOut CtxTx era -> Lovelace
C.calculateMinimumUTxO ShelleyBasedEra Era
forall era. IsShelleyBasedEra era => ShelleyBasedEra era
C.shelleyBasedEra (LedgerProtocolParameters Era -> PParams (ShelleyLedgerEra Era)
forall era.
LedgerProtocolParameters era -> PParams (ShelleyLedgerEra era)
C.unLedgerProtocolParameters LedgerProtocolParameters Era
envPParams) (Output -> TxOut CtxTx Era
outputTxOut Output
out)

    -- Only outputs with enough ADA above their own minimum are reducible.
    let hasEnoughAda :: Output -> Bool
hasEnoughAda Output
out = Value -> Lovelace
C.selectLovelace (Output -> Value
forall t. IsInputOrOutput t => t -> Value
valueOf Output
out) Lovelace -> Lovelace -> Bool
forall a. Ord a => a -> a -> Bool
> Output -> Lovelace
minRequiredAda Output
out
    Output
target <- (Output -> Bool) -> ThreatModel Output
anyGuardedOutputSuchThat Output -> Bool
hasEnoughAda

    -- 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
        requiredAda :: Lovelace
requiredAda = Output -> Lovelace
minRequiredAda Output
target
        -- Calculate reduced ADA, ensuring we don't go below the output's own
        -- 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
requiredAda (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"
        ]

    [Char] -> [[Char]] -> ThreatModel ()
tabulateTM [Char]
"reduction %" [Double -> [Char]
bucketPct Double
reductionFactor]

    -- 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

-- | Shrink a positive 'Double' toward 0, discarding non-positive results.
shrinkPositiveDouble :: Double -> [Double]
shrinkPositiveDouble :: Double -> [Double]
shrinkPositiveDouble = (Double -> Bool) -> [Double] -> [Double]
forall a. (a -> Bool) -> [a] -> [a]
filter (Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
0) ([Double] -> [Double])
-> (Double -> [Double]) -> Double -> [Double]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> [Double]
forall a. RealFrac a => a -> [a]
shrinkRealFrac

-- | Coarse bucket for the reduction-factor distribution report.
bucketPct :: Double -> String
bucketPct :: Double -> [Char]
bucketPct Double
r
  | Double
r Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0.25 = [Char]
"01-25%"
  | Double
r Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0.50 = [Char]
"26-50%"
  | Double
r Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0.75 = [Char]
"51-75%"
  | Bool
otherwise = [Char]
"76-99%"