{-# LANGUAGE OverloadedStrings #-}

{- | Threat model for detecting Large Value Attack vulnerabilities.

A Large Value Attack exploits validators that don't properly validate the
structure of @Value@ in their outputs. If a validator allows spending from
a script output without checking what tokens are present in the output's value,
an attacker can "bloat" the value with additional junk tokens.

== Consequences ==

1. __Increased min-UTxO requirements__: Each unique token in a UTxO increases
   the minimum Ada required. Adding many junk tokens forces the victim to
   lock more Ada than intended.

2. __Serialization costs__: Large values increase transaction size, consuming
   more of the victim's fee budget when spending the UTxO.

3. __Permanent fund locking__: If the value is bloated sufficiently:

   - The transaction required to spend the UTxO may exceed protocol size limits
   - The serialized output may exceed the max-value-size protocol parameter

   In these cases, the UTxO becomes __permanently unspendable__ and funds
   are locked forever with no possibility of recovery.

== Root Cause ==

Validators that don't check the @Value@ structure of outputs being created.
For example, a validator that only checks:

@
traceIfFalse "insufficient payment" (valuePaidTo pkh >= expectedAmount)
@

This allows an attacker to include @expectedAmount + junkTokens@, satisfying
the check while bloating the output.

== Mitigation ==

A secure validator should either:

- Whitelist expected tokens (only allow known policy IDs)
- Check the token count (e.g., @length (flattenValue v) <= maxTokens@)
- Require exact value match (not just @>=@ comparison)
- Validate that outputs contain only expected assets

This threat model tests if a script output can have arbitrary tokens added
to its value via minting. If the transaction still validates, the validator
has a Large Value Attack vulnerability.
-}
module Convex.ThreatModel.LargeValue (
  largeValueAttack,
  largeValueAttackWith,
  largeValueAttackWithGen,
) where

import Cardano.Api qualified as C
import Convex.ThreatModel
import Convex.ThreatModel.TxModifier (addPlutusScriptMint, alwaysSucceedsMintingPolicy)
import Data.ByteString.Char8 qualified as BS
import GHC.Exts (fromList)
import Test.QuickCheck (Gen, choose)

{- | Default large-value attack. The number of junk tokens is drawn per
transaction from a curated range, so QuickCheck explores the parameter space
and shrinks counterexamples toward the smallest triggering value.
-}
largeValueAttack :: ThreatModel ()
largeValueAttack :: ThreatModel ()
largeValueAttack = Gen Int -> ThreatModel ()
largeValueAttackWithGen ((Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100))

{- | Large-value attack with a fixed junk-token count. Keep using this for
deterministic regression tests and golden seeds.
-}
largeValueAttackWith :: Int -> ThreatModel ()
largeValueAttackWith :: Int -> ThreatModel ()
largeValueAttackWith = Gen Int -> ThreatModel ()
largeValueAttackWithGen (Gen Int -> ThreatModel ())
-> (Int -> Gen Int) -> Int -> ThreatModel ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Gen Int
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

{- | Large-value attack parameterised by a generator for the number of junk
tokens minted and added to a script output. This is the primitive the other
two forms delegate to.
-}
largeValueAttackWithGen :: Gen Int -> ThreatModel ()
largeValueAttackWithGen :: Gen Int -> ThreatModel ()
largeValueAttackWithGen Gen Int
numTokensGen =
  String -> ThreatModel () -> ThreatModel ()
forall a. String -> ThreatModel a -> ThreatModel a
Named String
"Large Value Attack" (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ do
    Int
numTokens <- Gen Int -> (Int -> [Int]) -> ThreatModel Int
forall a. Show a => Gen a -> (a -> [a]) -> ThreatModel a
forAllTM Gen Int
numTokensGen Int -> [Int]
shrinkPositive

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

    Output
target <- ThreatModel Output
anyGuardedOutput

    -- Create junk tokens by minting with the always-succeeds policy
    let policyId :: PolicyId
policyId = ScriptHash -> PolicyId
C.PolicyId (ScriptHash -> PolicyId) -> ScriptHash -> PolicyId
forall a b. (a -> b) -> a -> b
$ Script PlutusScriptV2 -> ScriptHash
forall lang. Script lang -> ScriptHash
hashScript (PlutusScriptVersion PlutusScriptV2
-> PlutusScript PlutusScriptV2 -> Script PlutusScriptV2
forall lang.
IsPlutusScriptLanguage lang =>
PlutusScriptVersion lang -> PlutusScript lang -> Script lang
C.PlutusScript PlutusScriptVersion PlutusScriptV2
C.PlutusScriptV2 PlutusScript PlutusScriptV2
alwaysSucceedsMintingPolicy)
        junkTokens :: [(AssetName, Quantity)]
junkTokens =
          [ (ByteString -> AssetName
C.UnsafeAssetName (ByteString -> AssetName) -> ByteString -> AssetName
forall a b. (a -> b) -> a -> b
$ String -> ByteString
BS.pack (String -> ByteString) -> String -> ByteString
forall a b. (a -> b) -> a -> b
$ String
"junk" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i, Integer -> Quantity
C.Quantity Integer
1)
          | Int
i <- [Int
1 .. Int
numTokens]
          ]
        junkValue :: Value
junkValue =
          [Item Value] -> Value
forall l. IsList l => [Item l] -> l
fromList
            [ (PolicyId -> AssetName -> AssetId
C.AssetId PolicyId
policyId AssetName
name, Quantity
qty)
            | (AssetName
name, Quantity
qty) <- [(AssetName, Quantity)]
junkTokens
            ]
        bloatedValue :: Value
bloatedValue = Output -> Value
forall t. IsInputOrOutput t => t -> Value
valueOf Output
target Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> Value
junkValue

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

    String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
      [String] -> String
paragraph
        [ String
"Testing if"
        , Int -> String
forall a. Show a => a -> String
show Int
numTokens
        , String
"junk tokens can be minted and added to the output's value"
        , String
"while still passing validation."
        ]

    String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
      [String] -> String
paragraph
        [ String
"If this validates, the script's value validation is permissive."
        , String
"An attacker could exploit this to:"
        , String
"1) Increase min-UTxO requirements, locking victim's Ada"
        , String
"2) Inflate transaction sizes, increasing spending costs"
        , String
"3) Potentially lock funds permanently if size limits are exceeded"
        ]

    String -> [String] -> ThreatModel ()
tabulateTM String
"junk tokens" [Int -> String
bucket Int
numTokens]

    -- Create mint modifiers for all junk tokens
    let mintModifiers :: TxModifier
mintModifiers =
          [TxModifier] -> TxModifier
forall a. Monoid a => [a] -> a
mconcat
            [ PlutusScript PlutusScriptV2
-> AssetName -> Quantity -> ScriptData -> TxModifier
forall lang.
IsPlutusScriptInEra lang =>
PlutusScript lang
-> AssetName -> Quantity -> ScriptData -> TxModifier
addPlutusScriptMint PlutusScript PlutusScriptV2
alwaysSucceedsMintingPolicy AssetName
name Quantity
qty (() -> ScriptData
forall a. ToData a => a -> ScriptData
toScriptData ())
            | (AssetName
name, Quantity
qty) <- [(AssetName, Quantity)]
junkTokens
            ]

    -- This SHOULD fail - if it validates, the contract is vulnerable
    -- The attack: mint junk tokens AND add them to the target output
    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
bloatedValue
        TxModifier -> TxModifier -> TxModifier
forall a. Semigroup a => a -> a -> a
<> TxModifier
mintModifiers

{- | Shrink a positive integer toward 1 (the smallest meaningful value),
never reaching 0.
-}

-- | Coarse bucket for the parameter distribution report.
bucket :: Int -> String
bucket :: Int -> String
bucket Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
10 = String
"001-010"
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
50 = String
"011-050"
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
100 = String
"051-100"
  | Bool
otherwise = String
"101+"