SCP-4108 Vulnerability Analysis of Marlowe Contracts

[bwbush]

Requirements

The Summary of Testing History and Results highlights several situations where the Marlowe validator does or can not guard against Marlowe contract instances that are either partly or wholly unexecutable. There are also situations where it is unwise to deploy a particular Marlowe contract.

1. Invalid preconditions for computeTransaction:
   1. Non-positive account balances (unexecutable)
   2. Duplicate accounts, choices, or bound values (undefined behavior).
2. Role token with blank currency and name (anyone can redeem payouts), or role names longer than 32 bytes (exceeds ledger limit).
3. Asset names longer than 32 bytes (exceeds ledger limit).
4. Protocol limits (block or lock):
   1. Transaction size.
   2. Execution memory.
   3. Execution steps.
   4. Maximum value.
   5. Minimum UTxO.

We need library functions and a CLI tool that allows users to check whether a contract might be subject to the above limitations.

Approach

We're considering a multi-pronged approach to analyzing contract instances to determine whether they are subject to any of these problems:

1. Simple analysis: Applies to invalid preconditions and role tokens.
2. Simple upper bounds: The maximum-value and minimum-UTxO can be bounded by just counting the tokens in the contract instance.
3. Path-based upper bounds: A tighter bound for maximum-value and minimum-UTxO can be made by counting tokens along all paths in the contract instance. Similarly, the size of State in the transaction can also be bounded via this method. This involves bounding accounts, choices, and boundValues at each transaction step, which is slightly tricky because it involves bounding the size of Integers present.
4. Executing computeTransaction along all paths identified by getAllInputs: The actual value of maximum-value and minimum-UTxO can be computed by semantic execution along all paths of the contract.
5. Executing validator along all paths identified by getAllInputs: A safe value for execution memory and steps can be computed by running all transaction paths through evaluateScriptCounting, which executes the validator using the Plutus interpreter. This involves creating a minimally viable ScriptContext for each transaction.
6. Executing transactions along all paths identified by getAllInputs: A safe value for transaction size can be computed by running all transaction paths through makeTransactionBodyAutoBalance. This involves creating a minimally viable TxBody for each transaction.

By "safe value" we mean that there exists some valid Cardano transaction for which the particular path will validate. It might be the case that the validator fails for a ScriptContext with excess inputs or outputs, but there exists an minimal ScriptContext for which it succeeds.

Why take a multpronged approach? The two simple analyses above will be extremely fast for any contract. The "path-based upper bounds" method will also run fast, but it does involve full DAG traversal of the contract. Methods that rely on getAllInputs will be slow or impractical for large contracts.

Will executing all transactions along all paths prove the safety of a contract instance? This will find all unsafe contracts, under the assumptions that getAllInputs returns all execution paths, that makeTransactionBodyAutoBlance is faithful to the ledger and to Plutus, and that the path traversal is correct.

Questions

• What are the guarantees on getAllInputs?
• Could getAllInputs be made incremental?
• Could getAllInputs support merkleized contracts?
• Are there faster pure Haskell alternatives to getAllInputs?

Implementation

• Spec.Marlowe.Plutus.Transaction already can create the minimally viable ScriptContext and Spec.Marlowe.Plutus.Scripts supports executing scripts with the Plutus intepreter, but off chain, which is much faster than on chain.
• Language.Marlowe.CLI.Run already can create the minimally viable TxBody can catch validation and ledger errors. It runs off chain but is faithful to the chain rules.
• The implementation requires a general traversal capability for the tree or DAG of possible execution paths.
• The implementation will do bounds arithmetic along traversal paths.

CLI interface

marlowe-cli run analyze --help

Usage: marlowe-cli run analyze
         --testnet-magic INTEGER --socket-path SOCKET_FILE 
         --marlowe-file MARLOWE_FILE [--out-file FILE]
         (--all | [--preconditions] [--roles] [--tokens]
         [--maximum-value] [--minimum-utxo]
         [--transaction-size] [--execution-cost])
         ([--fast] | --best)

  Analyze a Marlowe contract and report issues that might cause paths in it to
  fail executing on the Cardano blockchain. This estimates bounds

Available options:
  --testnet-magic INTEGER  Network magic. Defaults to the CARDANO_TESTNET_MAGIC
                           environment variable's value.
  --socket-path SOCKET_FILE
                           Location of the cardano-node socket file. Defaults to
                           the CARDANO_NODE_SOCKET_PATH environment variable's
                           value.
  --marlowe-file MARLOWE_FILE
                           JSON file with the Marlowe initial state and initial
                           contract.
  --out-file FILE          Output JSON file for the report.
  --all                    Perform all checks.
  --preconditions          Check preconditions for Marlowe state.
  --roles                  Check for blank role names or role names longer
                           than 32 bytes.
  --tokens                 Check for token names longer than 32 bytes.
  --maximum-value          Check for violations of the `maxValueSize` protocol
                           parameter.
  --minimum-utxo           Check for violations of the `utxoCostPerWord`
                           protocol parameter.
  --transaction-size       Check for violations of the `maxTxSize` protocol
                           parameter.
  --execution-cost         Check for violations of the `maxTxExecutionUnits`
                           protocol parameter.
  --fast                   Quickly compute generous estimates of worst-case
                           bounds.
  --best                   Compute tight estimates of worst-case bounds. 
  -h,--help                Show this help text

[bwbush]

Here are our first empirical results studying execution cost. I just varied the number of single-letter ValueIds in boundValues, where 0 was bound to each variable; the contract is Close and the accounts is just a single account with 1 Ada. This is pretty much the simplest Marlowe execution.

This is encouraging enough that I'll continue the exploration. This part is linear, but there will be interaction between the state and the contract terms, and I don't know if that interaction will be linear or not. It might be that a large GLM could fit this. Alternatively, finding bounds on nonlinear interactions would be more like mapping a Pareto surface. So there is some chance this will map to a well-known statistics problem.