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.