module Test.QuickCheck.ContractModel.ThreatModel.DoubleSatisfaction
  ( doubleSatisfaction
  ) where

import Cardano.Api

import PlutusTx.Prelude (BuiltinByteString)

import Test.QuickCheck.ContractModel.ThreatModel

safeScript :: SimpleScript SimpleScriptV2
safeScript :: SimpleScript SimpleScriptV2
safeScript = [SimpleScript SimpleScriptV2] -> SimpleScript SimpleScriptV2
forall lang. [SimpleScript lang] -> SimpleScript lang
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 Ada from) the victim to the attacker, i.e. there is a script that
--     care 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.
doubleSatisfaction :: ThreatModel ()
doubleSatisfaction :: ThreatModel ()
doubleSatisfaction = 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 ada :: Value
ada = Value -> Value
projectAda (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$ Output -> Value
forall t. IsInputOrOutput t => t -> Value
valueOf Output
output

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

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

  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 -> Value -> TxModifier
forall t. IsInputOrOutput t => t -> Value -> TxModifier
changeValueOf Output
output (Output -> Value
forall t. IsInputOrOutput t => t -> Value
valueOf Output
output Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> Value -> Value
negateValue Value
ada)
                                        TxModifier -> TxModifier -> TxModifier
forall a. Semigroup a => a -> a -> a
<> AddressAny -> Value -> Datum -> TxModifier
addOutput AddressAny
signer Value
ada Datum
forall ctx era. TxOutDatum ctx era
TxOutDatumNone

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

  -- 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 (BuiltinByteString
"SuchSecure" :: BuiltinByteString)

      victimTarget :: AddressAny
victimTarget = Output -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf Output
output

  TxModifier -> ThreatModel ()
shouldNotValidate (TxModifier -> ThreatModel ()) -> TxModifier -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ SimpleScript SimpleScriptV2 -> Value -> TxModifier
addSimpleScriptInput SimpleScript SimpleScriptV2
safeScript Value
ada
                   TxModifier -> TxModifier -> TxModifier
forall a. Semigroup a => a -> a -> a
<> AddressAny -> Value -> Datum -> TxModifier
addOutput      AddressAny
victimTarget Value
ada Datum
uniqueDatum
                   TxModifier -> TxModifier -> TxModifier
forall a. Semigroup a => a -> a -> a
<> Output -> Value -> TxModifier
forall t. IsInputOrOutput t => t -> Value -> TxModifier
changeValueOf  Output
output (Output -> Value
forall t. IsInputOrOutput t => t -> Value
valueOf Output
output Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> Value -> Value
negateValue Value
ada)
                   TxModifier -> TxModifier -> TxModifier
forall a. Semigroup a => a -> a -> a
<> AddressAny -> Value -> Datum -> TxModifier
addOutput      AddressAny
signer Value
ada Datum
forall ctx era. TxOutDatum ctx era
TxOutDatumNone