From 8855feae473882b82643db792327423152e45b5c Mon Sep 17 00:00:00 2001 From: Brian W Bush Date: Thu, 2 Mar 2023 15:27:42 -0700 Subject: [PATCH] SCP-5141 SCP-5142 Enforced initial and final state validity in validator. --- marlowe-test/src/Spec/Marlowe/Marlowe.hs | 4 +- .../src/Spec/Marlowe/Plutus/Specification.hs | 2 +- marlowe/CHANGELOG.md | 5 ++ marlowe/debugging-cookbook.md | 12 +++- .../marlowe-cardano-specification.md | 23 ++++++- marlowe/src/Language/Marlowe/Scripts.hs | 65 +++++++++++++------ 6 files changed, 82 insertions(+), 29 deletions(-) diff --git a/marlowe-test/src/Spec/Marlowe/Marlowe.hs b/marlowe-test/src/Spec/Marlowe/Marlowe.hs index e2572a2ec7..6b6c0a7684 100644 --- a/marlowe-test/src/Spec/Marlowe/Marlowe.hs +++ b/marlowe-test/src/Spec/Marlowe/Marlowe.hs @@ -150,14 +150,14 @@ alternateMarloweValidatorSize :: IO () alternateMarloweValidatorSize = do let validator = Scripts.validatorScript alternateMarloweValidator let vsize = SBS.length . SBS.toShort . LB.toStrict $ Serialise.serialise validator - assertBool ("alternateMarloweValidator is too large " <> show vsize) (vsize <= 15349) + assertBool ("alternateMarloweValidator is too large " <> show vsize) (vsize <= 14869) -- | Test that the untyped validator is not too large. marloweValidatorSize :: IO () marloweValidatorSize = do let validator = Scripts.validatorScript marloweValidator let vsize = SBS.length . SBS.toShort . LB.toStrict $ Serialise.serialise validator - assertBool ("marloweValidator is too large " <> show vsize) (vsize <= 12242) + assertBool ("marloweValidator is too large " <> show vsize) (vsize <= 12347) -- | Test `extractNonMerkleizedContractRoles`. diff --git a/marlowe-test/src/Spec/Marlowe/Plutus/Specification.hs b/marlowe-test/src/Spec/Marlowe/Plutus/Specification.hs index 61f0336f3a..ca4b579cc8 100644 --- a/marlowe-test/src/Spec/Marlowe/Plutus/Specification.hs +++ b/marlowe-test/src/Spec/Marlowe/Plutus/Specification.hs @@ -195,7 +195,7 @@ tests referencePaths = -- DO NOT ALTER THE FOLLOWING VALUE UNLESS YOU ARE COMMITTING -- APPROVED CHANGES TO MARLOWE'S SEMANTICS VALIDATOR. THIS HASH -- HAS IMPLICATIONS FOR VERSIONING, AUDIT, AND CONTRACT DISCOVERY. - "8099cd4eafbe7187b6513adcdb01ea3719296f614b07945a5462b408" + "a7cc35084607dab02a50761ca15f6192d0c2ffe12f0d22263fa3f286" ] , testGroup "Payout Validator" [ diff --git a/marlowe/CHANGELOG.md b/marlowe/CHANGELOG.md index 2e382ea7c7..43249b0774 100644 --- a/marlowe/CHANGELOG.md +++ b/marlowe/CHANGELOG.md @@ -34,3 +34,8 @@ Based on audit findings, we added "Constraint 18. Final balance" to the Marlowe- ## SCP-5143: Removed tracing from validator In order to reduces the validator size, calls to Plutus tracing functions were removed. + + +## SCP-5141: Valid initial and final states + +Based on audit finds, we added "Constraint 19. No duplicates" to the Marlowe-Cardano specification and require that the validator ensure that both the intial and final states of the contract obey the invariants of correct total value, positive balances, and non-duplication of keys for accounts, choices, and bound values. diff --git a/marlowe/debugging-cookbook.md b/marlowe/debugging-cookbook.md index 93d33d4ebe..0fababe2ca 100644 --- a/marlowe/debugging-cookbook.md +++ b/marlowe/debugging-cookbook.md @@ -100,16 +100,24 @@ Transaction failures occur in either phase 1 validation (ledger rules) or phase * If a transaction fails phase two validation, a terse Marlowe error will be reported in the Plutus trace log: * `"a"`: The slot/time validity range for the transaction is infinite or semi-infinite. The range should be finite/bounded. - * `"b"`: All accounts must have positive balances. + * `"bi"`: All accounts must have positive balances in the initial state. + * `"bo"`: All accounts must have positive balances in the final state. * `"c"`: A transaction containing a contract that closes may not also include the creation of a new contract. * `"d"`: The datum or value at the script output does not match the contract's transition. + * `"eai"` : The initial state must not have duplicate accounts. + * `"ebi"` : The initial state must not have duplicate bound values. + * `"eci"` : The initial state must not have duplicate choices. + * `"eao"` : The final state must not have duplicate accounts. + * `"ebo"` : The final state must not have duplicate bound values. + * `"eco"` : The final state must not have duplicate choices. * `"f"`: The value in the script's output UTxO does not match the value in its internal state. * `"o"`: Outputting to two Marlowe scripts with the same address in the same transaction is forbidden. * `"p"`: Insufficient value is paid to a public-key address. * `"r"`: Insufficient value is paid in a role payout. This may occur because the role payout was adjusted to satisfy the minimum-ADA ledger rule, despite that adjustment violating the terms of the contract. * `"s"`: A required public-key signature was not present in the transaction. * `"t"`: The role token authorizing the application of input is not present in the transaction. - * `"v"`: The value input from the script does not match that specified in its datum. + * `"vi"`: The value input from the script does not match that specified in its datum. + * `"vo"`: The value output from the script does not match that specified in its datum. * `"w"`: Inputting from two Marlowe scripts with the same address in the same transaction is forbidden. * `"x"`: The input datum was not provided to the script. * If these errors occur during Plutus validation but not outside of it, then there likely is a clock inconsistency between local time and the node. diff --git a/marlowe/specification/marlowe-cardano-specification.md b/marlowe/specification/marlowe-cardano-specification.md index d2b441ab49..3167fc9e02 100644 --- a/marlowe/specification/marlowe-cardano-specification.md +++ b/marlowe/specification/marlowe-cardano-specification.md @@ -318,9 +318,11 @@ all demerkleizes transactionInput ≡ True #### *Constraint 13.* Positive balances -All accounts in the state have positive balances. +All accounts in the initial and final states have positive balances. ```haskell -all ((> 0) . snd) (accounts $ marloweState marloweData) ≡ True +positiveBalances $ marloweState marloweData ≡ True +positiveBalances $ txOutState transactionOutput ≡ True + where positiveBalances state = all ((> 0) . snd) (accounts state) ``` @@ -364,13 +366,28 @@ The payment to a role must be in a single output, but the payment to an address #### *Constraint 18.* Final balance The value output to the script's UTxO must equal the total value in the output state. - ```haskell outValue ≡ foldMap toValue (accounts $ txOutState transactionOutput) where toValue ((_, Token currency name), count)) = Value.singleton currency name count ``` +#### *Constraint 19.* No duplicates + +The initial and final state must not have duplicate keys in their account entries, choices, or bound values. +```haskell +hasDuplicateKey (accounts inState ) ≡ False +hasDuplicateKey (choices inState ) ≡ False +hasDuplicateKey (boundValues inState ) ≡ False +hasDuplicateKey (accounts outState) ≡ False +hasDuplicateKey (choices outState) ≡ False +hasDuplicateKey (boundValues outState) ≡ False + where + outState = txOutState transactionOutput + hasDuplicateKey am = let ks = fst <$> toList am in length ks /= length (nub ks) +``` + + ## Plutus Validator for Marlowe Payouts diff --git a/marlowe/src/Language/Marlowe/Scripts.hs b/marlowe/src/Language/Marlowe/Scripts.hs index 6441455264..d2ded63fc3 100644 --- a/marlowe/src/Language/Marlowe/Scripts.hs +++ b/marlowe/src/Language/Marlowe/Scripts.hs @@ -202,12 +202,10 @@ mkMarloweValidator case closeInterval $ txInfoValidRange scriptContextTxInfo of Just interval' -> interval' Nothing -> traceError "a" - -- The incoming balance of each account must be positive. - -- [Marlowe-Cardano Specification: "Constraint 13. Positive balances".] - let positiveBalances = traceIfFalse "b" $ validateBalances marloweState -- Find Contract continuation in TxInfo datums by hash or fail with error. let inputs = fmap marloweTxInputToInput marloweTxInputs + {- We do not check that a transaction contains exact input payments. We only require an evidence from a party, e.g. a signature for PubKey party, or a spend of a 'party role' token. This gives huge flexibility by allowing @@ -215,22 +213,19 @@ mkMarloweValidator Then, we check scriptOutput to be correct. -} let inputContents = fmap getInputContent inputs + -- Check that the required signatures and role tokens are present. -- [Marlowe-Cardano Specification: "Constraint 14. Inputs authorized".] let inputsOk = validateInputs inputContents - -- Since individual balances were validated to be positive, - -- the total balance is also positive. - let inputBalance = totalBalance (accounts marloweState) - -- [Marlowe-Cardano Specification: "Constraint 5. Input value from script".] - -- The total incoming balance must match the actual script value being spent. - let balancesOk = traceIfFalse "v" $ inputBalance == scriptInValue - - let preconditionsOk = positiveBalances && balancesOk + -- [Marlowe-Cardano Specification: "Constraint 13. Positive balances".] + -- [Marlowe-Cardano Specification: "Constraint 19. No duplicates".] + -- Check that the initial state obeys the Semantic's invariants. + let preconditionsOk = checkState "i" scriptInValue marloweState - -- Package the inputs to be applied in the semantics. -- [Marlowe-Cardano Specification: "Constraint 0. Input to semantics".] + -- Package the inputs to be applied in the semantics. let txInput = TransactionInput { txInterval = interval, txInputs = inputs } @@ -264,16 +259,17 @@ mkMarloweValidator _ -> let totalIncome = foldMap collectDeposits inputContents totalPayouts = foldMap snd payoutsByParty - finalBalance = inputBalance + totalIncome - totalPayouts - outputBalance = totalBalance (accounts txOutState) + finalBalance = scriptInValue + totalIncome - totalPayouts in - -- The total account balance must be paid to a single output to the script. - -- [Marlowe-Cardano Specification: "Constraint 3. Single Marlowe output".] - -- [Marlowe-Cardano Specification: "Constraint 6. Output value to script."] - checkOwnOutputConstraint marloweData finalBalance - -- The value in the script's output UTxO must match the value in the output state. - -- [Marlowe-Cardano Specification: "Constraint 18. Final balance."] - && traceIfFalse "f" (outputBalance == finalBalance) + -- [Marlowe-Cardano Specification: "Constraint 3. Single Marlowe output".] + -- [Marlowe-Cardano Specification: "Constraint 6. Output value to script."] + -- Check that the single Marlowe output has the correct datum and value. + checkOwnOutputConstraint marloweData finalBalance + -- [Marlowe-Cardano Specification: "Constraint 18. Final balance."] + -- [Marlowe-Cardano Specification: "Constraint 13. Positive balances".] + -- [Marlowe-Cardano Specification: "Constraint 19. No duplicates".] + -- Check that the final state obeys the Semantic's invariants. + && checkState "o" finalBalance txOutState preconditionsOk && inputsOk && payoutsOk && checkContinuation Error TEAmbiguousTimeIntervalError -> traceError "i" Error TEApplyNoMatchError -> traceError "n" @@ -311,6 +307,33 @@ mkMarloweValidator TxInInfo{txInInfoResolved=TxOut{txOutAddress=Ledger.Address (ScriptCredential vh2) _}} = vh1 == vh2 sameValidatorHash _ _ = False + -- Check a state for the correct value, positive accounts, and no duplicates. + checkState :: BuiltinString -> Val.Value -> State -> Bool + checkState tag expected State{..} = + let + positiveBalance :: (a, Integer) -> Bool + positiveBalance (_, balance) = balance > 0 + noDuplicates :: Eq k => AssocMap.Map k v -> Bool + noDuplicates am = + let + test [] = True -- An empty list has no duplicates. + test (x : xs) -- Look for a duplicate of the head in the tail. + | elem x xs = False -- A duplicate is present. + | otherwise = test xs -- Continue searching for a duplicate. + in + test $ AssocMap.keys am + in + -- [Marlowe-Cardano Specification: "Constraint 5. Input value from script".] + -- and/or + -- [Marlowe-Cardano Specification: "Constraint 18. Final balance."] + traceIfFalse ("v" <> tag) (totalBalance accounts == expected) + -- [Marlowe-Cardano Specification: "Constraint 13. Positive balances".] + && traceIfFalse ("b" <> tag) (all positiveBalance $ AssocMap.toList accounts) + -- [Marlowe-Cardano Specification: "Constraint 19. No duplicates".] + && traceIfFalse ("ea" <> tag) (noDuplicates accounts) + && traceIfFalse ("ec" <> tag) (noDuplicates choices) + && traceIfFalse ("eb" <> tag) (noDuplicates boundValues) + -- Look up the Datum hash for specific data. findDatumHash' :: PlutusTx.ToData o => o -> Maybe DatumHash findDatumHash' datum = findDatumHash (Datum $ PlutusTx.toBuiltinData datum) scriptContextTxInfo