A comprehensive guide to Marlowe's security: audit outcomes, built-in functional restrictions, and ledger security features

Disclaimer: The content in this Marlowe Security article is provided “AS IS” with no guarantees of any kind. Nothing in this document is intended to be professional advice, including without limitation, financial, investment, legal, or tax advice. Input Output Global is not responsible for your use of or reliance on any information in this document.

Introduction

In most blockchains, a smart contract is a computer program that self-executes once certain predefined conditions are met. In Cardano, it's a little different, as smart contract execution happens in a transaction submitted externally to the Cardano node. But irrespective of how it works under the hood, smart contracts are useful for many industries: financial, real estate, commerce, and many others.

Transactions using smart contracts may involve the movement and transfer of substantial value, which may be a prized target for bad actors. Equally, this value may become locked, or be lost altogether, due to flaws or vulnerabilities in the coding.

Avoiding any undesired outcome requires the implementation of a robust security framework, which involves a combination of design principles, audits, and best practices by developers, exchanges, and any other parties handling smart contracts.

Adding to an ever-growing range of resources from across Cardano’s technical community, Marlowe is an ecosystem of tools and languages created by Input Output Global (IOG) to enable development of financial and transactional smart contracts on the Cardano blockchain.

The Marlowe suite has been designed and developed with a security-centric focus. Marlowe's creators have built in functional limitations that ensure that contracts are finite and always terminate, for example. Marlowe also avoids certain programming constructs to prevent undesired outcomes, eg recursion and looping. A third party, Tweag, conducted a static and dynamic audit prior to Marlowe's deployment on mainnet. The result of all these security features, and many others, is a safe and secure smart contract creation and development platform.

This article delves into Marlowe's security, explaining the findings of the security audit, and how the team responded to them, built-in functional limitations, security analysis tools included in the deployment, and some precautions and considerations that must be taken when using Marlowe.

Structure of this document

This document is divided into six clearly defined sections:

1. Smart contract auditing
2. Smart contract-based attacks
3. Tweag audit
4. Built-in security-enhancing functional limitations in Marlowe
5. Transaction validation
6. Monetary policies

As a whole, this document intends to provide a comprehensive understanding of the importance of smart contract auditing and the different types of smart contract-based attacks that exist today, before delving specifically into how the Marlowe suite of tools utilizes auditing and strong security principles to maintain a safe and secure smart contract development environment.

Smart contract auditing

Overview

The inherent autonomy of smart contracts and the relatively high stakes involved in certain transactions mean that ensuring consistency and security is paramount. This requires knowing exactly how a smart contract will behave when it executes so that any potential flaws or intentional malicious code can be detected and addressed. Auditing smart contracts from a security standpoint is the best way to prevent subsequent failures or damage. An audit thoroughly examines the smart contract's code and conditions before deployment, to ensure the contract behaves as expected.

Auditing methods

Though approaches to smart contract auditing may differ and vary from project to project, smart contracts can be analyzed using manual or automated methods. Usually, most projects employ a combination of both.

Documentation gathering

Before the auditing process starts, auditors may spend some time gathering any project-related documentation. This may include technical documents, whitepapers, codebase, and any other material that may be relevant and helpful in the auditing process.

Manual auditing

This form of smart contract auditing involves a group of people analyzing each line of code, contract logic, contract architecture, and any built-in security measures to ensure efficient design and correctness. Apart from revealing coding errors, a manual audit may also discover design flaws. Manual auditing tends to be considered a very thorough and accurate method.

Automated auditing

Unlike manual auditing, automated auditing normally takes a software-centric approach to testing. Proprietary or off-the-shelf software auditing tools might help to detect bugs, but certain vulnerabilities might not become apparent.

Because of the complementary nature of these methods, the best auditing practices involve a combination of manual and automated auditing to ensure that all potential flaws, bugs, and vulnerabilities are detected and corrected.

Post-audit actions

Once the auditing process is complete, the auditor/s will produce a report detailing their findings. These may include error classification by severity and a series of recommendations.

Contract errors can be classified as:

• Critical: this type of flaw will likely prevent safe functioning of a contract and/or protocol.
• Major: certain errors in coding or logic may lead to fund loss, or an uncontrolled protocol state.
• Medium: while funds may not be at risk, these types of errors may affect the contract’s performance or reliability.
• Minor: this classification usually includes inefficient code with little or no impact on security. Informational: usually refers to coding style or best practice issues.

Advantages of smart contract auditing

While auditing is important for any application, it is especially crucial for smart contracts and decentralized applications (DApps) running on blockchain because of the immutable nature of these decentralized ledgers.

Advantages of smart contract auditing include proactive identification of risks, avoidance of potentially costly errors, a better development environment overall, and the obtention of insights about vulnerabilities, and how to eliminate them.

Proactive identification of risks

The deployment of unaudited smart contracts is a gamble that no developer or company should ever take. Some smart contracts may involve substantial funds, which, if lost or compromised, may lead to even bigger liabilities. By proactively working to remediate these risks, the possibility of something going badly wrong is greatly diminished.

Avoidance of potentially costly errors

Funds becoming forever locked because of coding/logic errors or as a result of malicious interference in a contract is something that no customer or developer ever wants to experience. The financial loss is just one side of it. There may also be serious legal ramifications.

A better development environment overall

Auditing software is not only recommended, it’s a requirement. Guaranteeing the security of an application or a suite of applications and following best practices strengthens the offering and creates a healthier development environment.

Obtention of insights about vulnerabilities, and how to eliminate them

In software development, prevention is better than patching. And when it comes to smart contracts, there is no chance for patching because of blockchain’s immutable nature. A thorough audit will yield much information about the code, the contract’s logic, the architecture, and many other parameters, enabling developers to refine and produce the best possible contract.

Smart contract-based attacks

Re-entrancy attacks

In this attack, a smart contract function temporarily gives up control of a transaction by making a call to a second contract, which begins making recursive withdrawal calls to the first contract, draining its funds before the first contract updates its state. These types of attacks become possible because of bugs in smart contract coding. The 2016 DAO event involved a re-entrancy attack.

The design of the Cardano blockchain makes re-entrancy attacks impossible. Because Cardano uses the EUTXO model, smart contracts are atomic and do not make calls to each other, which renders re-entrancy an impossibility.

Front-running invasions

Some blockchain designs allow for smart contracts and transactions to be publicly viewable for a time, before being confirmed on-chain. These pending transactions are shared throughout mempools across the network, which enables an adversary to see the intended outcome of a contract. Such an adversary with visibility of pending transactions can introduce a new trade or transaction with the knowledge that doing so will earn a profit based on the pending trade, at the expense of other users' profits. Essentially, an adversary manipulates the execution order of transactions to their own advantage.

While this type of event is a big issue on other blockchains, there is no evidence that Cardano (and by extension, Marlowe) would be vulnerable to front-running invasions.

Oracle manipulation

Oracles connect blockchains to external systems, and smart contracts might execute based on data received from oracles. This dependability on external systems means that if the input received by the oracle has been manipulated before being fed to the oracle, the security and integrity of the smart contract's execution might become compromised.

Other common smart contract-based security vulnerabilities include arithmetic errors, integer overflow and underflow, smart contract visibility settings, and timestamp manipulation.

The Tweag audit

This section focuses on the outcomes of the Tweag security audit, the response from the Marlowe team, and the security principles built into Marlowe’s design.

Key findings of the Tweag security audit and internal responses

Tweag performed a manual and an automated audit of the Marlowe language, which revealed several issues.

The high-severity findings included handling of negative deposits, prevention of ‘double satisfaction’, enforcement of state invariants, an implementation difference between the formal specification versus the Plutus implementation, and the proof of money preservation theorem.

Handling of negative deposits

The income from deposits is computed by adding up the deposit inputs, regardless of whether they are negative, while the semantics considers them as zero deposits. Combined with the absence of a balance check on the ending Marlowe state, this allows the ending balance to differ from the value paid to the Marlowe validator. This could be exploited by a Marlowe contract that allows negative deposits.

Internal response

This issue was resolved by adding a guard against negative deposits in the Marlowe semantics validator. That guard ensures that the validator's semantics for negative deposits matches Marlowe's Isabelle semantics. Specifically, a deposit of a negative quantity is treated as a deposit of zero. Thus a negative deposit will not decrement any of the account balances in the Plutus datum, and the total of the internal balances will match the value held in the UTXO to the Marlowe semantics script address.

Prevention of double satisfaction

Although the Marlowe validator prevented double satisfaction among multiple copies of the Marlowe validator script running in the same transaction, it did not prevent it in cases where the Marlowe validator ran alongside another Plutus validator in the same transaction.

Internal response

Double satisfaction is now prevented by enforcing that the Marlowe validator is the only Plutus script that runs during transactions that make payments to parties. This allows Marlowe contracts to coordinate with other Plutus scripts, but only under conditions where double satisfaction is impossible. Some property-based tests were added to check the correctness of this mitigation.

Enforcement of state invariants

Originally, the Marlowe validator had made optimistic assumptions about its own correct operation and did not check certain invariants in order to reduce Plutus execution costs.

Internal response

The Marlowe semantics validator now rigorously enforces invariants for initial and final states, ensuring that the three state-invariants of positive accounts, non-duplication of state entries (accounts, choices, and bound values), and a total internal value match the script UTXO's value.

Implementation difference between the formal specification versus the Plutus implementation

The audit revealed some differences between the formal specification and the actual Plutus implementation. Specifically, language differences and efficiency considerations with respect to Isabelle, Haskell, and Plutus Tx.

The formal specification is written in Isabelle, a language for formal methods, while the actual Marlowe implementation is written in Haskell and Plutus Tx. The Marlowe team worked to follow the Isabelle specification as closely as possible, but some deviations were inevitable because of the different languages. For example, some aspects of the Marlowe implementation would be inefficient in Isabelle, so changes were necessary for a more efficient Haskell implementation.

Internal response

This issue was mitigated via code analysis and property-based testing

Proof of money preservation theorem

The money preservation theorem had only taken into account the amount of assets but not their type. This meant that the proof would not consider a case where a contract could, for example, receive 20 ada and 15 Djed and pay back 20 Djed and 15 ada.

Internal response

A revision of the Isabelle code remedied this problem. Specifically, the addition of a new MultiAssets type and the refactoring of the Isabelle code (without modifying the interpreter) to prove that the assets are preserved.

Built-in security-enhancing functional limitations in Marlowe

Marlowe features several limitations to ensure that certain security risks cannot occur.

• Contracts are finite
• Contracts will terminate
• Contracts have a definite lifetime
• No assets are retained when the contract closes
• Value is conserved

Besides these limitations, some programming language constructs are absent from Marlowe to ensure safety:

• Recursion is not allowed
• Looping is not supported
• Functions or macros may not be defined
• Timeouts must be numeric constants
• Only Case continuations may be merkleized. The Faustus programming language relaxes some of the limitations above, yet it compiles to secure Marlowe.

Security analysis tools

The Marlowe team-designed marlowe-cli run analyze analysis tool checks a Marlowe contract’s compatibility with the Cardano ledger rules.

The Cardano ledger has built-in restrictions that could prevent a Marlowe contract from running on-chain, even if the contract itself was valid with respect to the Marlowe language. For example, the ledger imposes restrictions on the length of role and token names, and also limits Plutus execution costs. Any contract violating any of these rules would not run on-chain, even though the contract might be correctly constructed. Equally, while contracts might run on the Playground, they would not run on-chain if the contract violates ledger restrictions. Learn more about built-in ledger design restrictions.

Key takeaway: whereas the Playground is about the language, Runtime is about implementing the Marlowe contract on the Cardano blockchain specifically. If someone implements Marlowe on another blockchain, you can still use the Playground, but you cannot use Runtime on another blockchain.

Note: a contract can get locked if the datum doesn't fit on-chain, but the Marlowe suite includes tools to evaluate this risk. These tools should be used before deploying a contract.

Transaction validation

Two types of Plutus validator scripts are involved in validating UTXO spending:

• Semantics validator
• Payout validator

Security practices dictate that transactions should not be signed unless the contents and implications of the transaction have been reviewed and are well understood. In the Marlowe environment, this means verifying the Marlowe contract, its input, and its state. It also means ensuring that the role minting policy (if any) and Marlowe validator used are the right ones.

The security considerations below apply to both validator script types.

Semantics validator

The following concepts should be well understood before signing a Marlowe transaction:

• Does the transaction operate a Marlowe contract?
• What is its role minting policy (if any)?
• How have role tokens been distributed (if any)?
• What is the current contract and its state?
• What input is being applied to the contract?
• What else is occurring in the transaction?

Does the transaction operate a Marlowe contract?

Plutus validator scripts are universal interpreters for all Marlowe contracts of a specified version, which means the UTXO for a Marlowe contract resides in a script hash. Verifying that a transaction spends from an address that has the Marlowe script hash as its payment part confirms that the true Marlowe validator will run to validate the spending of that specific UTXO. It's possible to compute the script hash of the Marlowe validator from the first principles by compiling the validator and computing its hash, assuming that the Marlowe script source code in this repository can be trusted.

What is its role minting policy (if any)?

A minting policy is the set of rules for the creation of tokens of a given token type, which is identified by the hash of their minting policy. This is known as minting policy ID. A minting policy determines whether new tokens can be created, or whether the tokens that have been created are all there will ever be.

For example, the parties to a Marlowe contract, such as lender and borrower, can be represented in two ways:

• By an address: each party of the type address corresponds to an instance of a pair of a public and a private key that is presumably held by a wallet of one of the parties. Using addresses to represent parties is simpler and cheaper than using roles. To authenticate themselves, parties represented by an address simply need to sign the transactions that require them to be authenticated (ie those that execute deposits or choices for the party).
• By a role token: each party of the type role corresponds to a token stored on-chain. For a contract to use role tokens as authentication, the contract needs to declare that its role token minting policy ID is the minting policy ID of the token that it wants to use as role token. In this case, each of the asset names of the token identified by the minting policy ID represents a different party. To authenticate a transaction, a role token owner just needs to include it as part of the transaction that requires authentication of the role token owner. There can potentially be more than one token with the same asset name, so you don’t technically own a role party unless you own all the instances of the role token that has the party's asset name.

How have role tokens been distributed?

If a contract only uses addresses for representing parties, minting policies for roles are not a concern. The disadvantage of addresses is that they cannot be provably transferred, so once the private key to an address is known, you cannot show you have forgotten it and deleted it. From an address recipient's perspective, the address is always insecure. The only way to have a secure address is to generate it yourself.

The advantage or roles is that, because tokens are treated as native assets on the chain, they can be transferred just like ada or any other asset. But anybody who owns a token with the right minting policy ID and asset name can act as the party it represents, so you need to ensure that you are the only one that owns such a token, or else you are not really in control of the party.

You can of course ensure you’re the only one owning that token by minting the role tokens yourself (Marlowe Runtime does this securely as part of the process of the contract creation process). If someone else minted the role tokens or created the contract, you need to make sure that:

• You have all the existing tokens that control the party
• No more such tokens can be created (because the minting policy doesn’t allow it)

If the minting policy is simple enough, the easiest way to check this is to use a Marlowe scanner to find out the contract's role minting policy ID. Then, use a Cardano explorer to check what the policy behind the minting policy is (to ensure no more roles can be produced) and to check the current distribution of the existing roles already minted (who has which tokens, in other words).

What is the current contract and its state?

The contract's pre-transaction state is defined in the Plutus datum associated with the UTXO being spent from the Marlowe script address. This datum must be provided in the transaction and must contain the following:

• the balances of the accounts internal to the contract
• the history of choices made up to this point in the contract's execution
• the current values of the contract's bound variables
• the part of the contract that remains to be executed

The datum can be extracted from the unsigned transaction body and deserialized to Language.Marlowe.Core.V1.Semantics.MarloweData using the function Plutus.V2.Ledger.Api.fromData.

Alternatively:

• the command-line tool marlowe log --show contract will display the contract's on-chain history.
• This online tool also enables viewing contracts and state on-chain
• A REST API provides the same information obtained via marlowe log --show

What input is being applied to the contract?

The Plutus redeemer associated with spending the UTXO from the Marlowe script address defines the input being applied to the contract, along with the slot validity interval for the transaction specified in the transaction body. The input is a sequence of zero or more deposits, choices, and notifications. Using tools like Marlowe Playground or marlowe-cli run prepare, it is possible to analyze the consequences of applying this input to the contract.

The redeemer can be extracted from the unsigned transaction body and deserialized to Language.Marlowe.Scripts.MarloweInput using the function Plutus.V2.Ledger.Api.fromData. The command-line tool marlowe-cli util slotting will compute the relationship between the slots mentioned in the validity interval to the POSIX times in the contract.

What else is occurring in the transaction?

The unsigned transaction may contain other spending and payments beyond that specified for the Marlowe contract. This can be examined with the tool cardano-cli transaction view.

Monetary policies

Typically, monetary policies (like those supported in Marlowe Runtime) enforcing a single minting event and single tokens for each role should be used. These policies ensure that the role tokens are true non-fungible tokens (NFTs), so role token holders are verifiably the only ones who can act as the parties in the contract.

Monetary policies that mint multiple copies of a particular role token, or policies with an open minting policy, support non-standard use cases. For instance, minting two copies of each role token and distributing them to the same party allows that party to place one token in cold storage as a backup if the wallet containing the ‘hot’ role token becomes inaccessible. Some novel crowdsourcing contracts might involve assigning the role (via identical role tokens that may be minted even after the contract commences) to many participants. Finally, a Plutus contract's minting policy for role tokens can coordinate with the operation of one or more Marlowe contracts.

Role tokens

Role tokens can authorize deposits and choices in Marlowe transactions. Authorizing the use of a role token is more flexible than authorizing with a public key, because a role token (and thus participation in a Marlowe contract) can be transferred between wallets or to someone else.

Marlowe validator scripts do not enforce any particular monetary policy for role tokens, to enable novel use cases. However, the security of authorizations in a role-based Marlowe contract does critically depend upon the role-token monetary policy. This means that both the monetary policy and the on-chain disbursement of the tokens should be carefully scrutinized before participating in a Marlowe contract. Verifying the monetary policy of a simple script involves retrieving the script from the blockchain and studying it. Verifying the monetary policy of a Plutus script involves obtaining and studying the Plutus source code for the script and hashing the source code to check the monetary policy ID.

Acknowledgment: Joseph Fajen, Brian Bush, and Omer Husain all made invaluable contributions to this article.