{-# LANGUAGE OverloadedStrings #-}

module Convex.ThreatModel.DoubleSatisfaction (
  doubleSatisfaction,
) where

import Data.ByteString (ByteString)
import PlutusTx.Builtins (toBuiltin)

import Convex.ThreatModel

safeScript :: SimpleScript
safeScript :: SimpleScript
safeScript = [SimpleScript] -> SimpleScript
RequireAllOf [] -- TODO: this is not the right script!

{- | Check for double satisfaction vulnerabilities.

  For a transaction with a public key output to an address (the victim) other than the signer
  (the attacker),

  * if you cannot redirect the output to the attacker, i.e. there is a script that
    cares about the output to the victim,
  * but it validates when you bundle the redirected transaction with a "safe script" that spends
    the same amount to the victim, tagging the output with a unique datum,

  then we have found a double satisfaction vulnerability in the script that stopped the first
  modified transaction.

  NOTE: This threat model removes the victim's output entirely and redirects the value to the
  attacker. This works for both Ada-only outputs and outputs with tokens.
-}
doubleSatisfaction :: ThreatModel ()
doubleSatisfaction :: ThreatModel ()
doubleSatisfaction = [Char] -> ThreatModel () -> ThreatModel ()
forall a. [Char] -> ThreatModel a -> ThreatModel a
Named [Char]
"Double Satisfaction" (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ do
  AddressAny
signer <- Hash PaymentKey -> AddressAny
keyAddressAny (Hash PaymentKey -> AddressAny)
-> ThreatModel (Hash PaymentKey) -> ThreatModel AddressAny
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThreatModel (Hash PaymentKey)
anySigner

  [Output]
outputs <- ThreatModel [Output]
getTxOutputs
  let validTarget :: AddressAny -> Bool
validTarget AddressAny
t = AddressAny
signer AddressAny -> AddressAny -> Bool
forall a. Eq a => a -> a -> Bool
/= AddressAny
t Bool -> Bool -> Bool
&& AddressAny -> Bool
isKeyAddressAny AddressAny
t
  Output
output <- [Output] -> ThreatModel Output
forall a. Show a => [a] -> ThreatModel a
pickAny ([Output] -> ThreatModel Output) -> [Output] -> ThreatModel Output
forall a b. (a -> b) -> a -> b
$ (Output -> Bool) -> [Output] -> [Output]
forall a. (a -> Bool) -> [a] -> [a]
filter (AddressAny -> Bool
validTarget (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

  let value :: Value
value = Output -> Value
forall t. IsInputOrOutput t => t -> Value
valueOf Output
output
      victimTarget :: AddressAny
victimTarget = Output -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf Output
output

  [Char] -> ThreatModel ()
counterexampleTM ([Char] -> ThreatModel ()) -> [Char] -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [[Char]] -> [Char]
paragraph ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
      [ [Char]
"The transaction above is signed by"
      , Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ AddressAny -> Doc
prettyAddress AddressAny
signer
      , [Char]
"and contains an output to"
      , Doc -> [Char]
forall a. Show a => a -> [Char]
show (AddressAny -> Doc
prettyAddress AddressAny
victimTarget) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"."
      , [Char]
"The objective is to show that there is a double satisfaction vulnerability"
      , [Char]
"that allows the signer to steal this output."
      ]

  [Char] -> ThreatModel ()
counterexampleTM ([Char] -> ThreatModel ()) -> [Char] -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [[Char]] -> [Char]
paragraph
      [ [Char]
"First we check that we cannot simply redirect the output to the signer,"
      , [Char]
"i.e. the script actually cares about this output."
      ]

  -- Precondition: removing the victim's output and paying to the signer should FAIL
  -- because the script enforces the payment to the victim
  ThreatModel () -> ThreatModel ()
forall a. ThreatModel a -> ThreatModel a
threatPrecondition (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    TxModifier -> ThreatModel ()
shouldNotValidate (TxModifier -> ThreatModel ()) -> TxModifier -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
      Output -> TxModifier
removeOutput Output
output
        TxModifier -> TxModifier -> TxModifier
forall a. Semigroup a => a -> a -> a
<> AddressAny -> Value -> Datum -> ReferenceScript Era -> TxModifier
addOutput AddressAny
signer Value
value Datum
forall ctx era. TxOutDatum ctx era
TxOutDatumNone ReferenceScript Era
forall era. ReferenceScript era
ReferenceScriptNone

  [Char] -> ThreatModel ()
counterexampleTM ([Char] -> ThreatModel ()) -> [Char] -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    [[Char]] -> [Char]
paragraph
      [ [Char]
"Now we try the same thing again, but this time there is another script"
      , [Char]
"that pays out to the victim and uses a unique datum to identify the payment."
      ]

  -- Attack: add safe script input with protected output, redirect original output to signer
  let uniqueDatum :: Datum
uniqueDatum = ScriptData -> Datum
txOutDatum (ScriptData -> Datum) -> ScriptData -> Datum
forall a b. (a -> b) -> a -> b
$ BuiltinByteString -> ScriptData
forall a. ToData a => a -> ScriptData
toScriptData (ByteString -> ToBuiltin ByteString
forall a. HasToBuiltin a => a -> ToBuiltin a
toBuiltin (ByteString
"SuchSecure" :: ByteString))

  TxModifier -> ThreatModel ()
shouldNotValidate (TxModifier -> ThreatModel ()) -> TxModifier -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    SimpleScript -> Value -> ReferenceScript Era -> TxModifier
addSimpleScriptInput SimpleScript
safeScript Value
value ReferenceScript Era
forall era. ReferenceScript era
ReferenceScriptNone
      TxModifier -> TxModifier -> TxModifier
forall a. Semigroup a => a -> a -> a
<> AddressAny -> Value -> Datum -> ReferenceScript Era -> TxModifier
addOutput AddressAny
victimTarget Value
value Datum
uniqueDatum ReferenceScript Era
forall era. ReferenceScript era
ReferenceScriptNone
      TxModifier -> TxModifier -> TxModifier
forall a. Semigroup a => a -> a -> a
<> Output -> TxModifier
removeOutput Output
output
      TxModifier -> TxModifier -> TxModifier
forall a. Semigroup a => a -> a -> a
<> AddressAny -> Value -> Datum -> ReferenceScript Era -> TxModifier
addOutput AddressAny
signer Value
value Datum
forall ctx era. TxOutDatum ctx era
TxOutDatumNone ReferenceScript Era
forall era. ReferenceScript era
ReferenceScriptNone