2024-02-26 Namada MASP Final Report

Security Audit Report

Namada Multi-asset shielded pool

Authors: Manuel Bravo, Ivan Golubovic, Aleksandar Ljahovic

Table of Contents Audit Overview ............................................................................................................ 1 Scope 1 Conclusion 1 Audit Dashboard ......................................................................................................... 2 Target Summary 2 Engagement Summary 2 Severity Summary 2 System Overview......................................................................................................... 3 Shielded transactions 3 Rewards and converts 4 On transaction validation and verification 4 Threat Analysis ............................................................................................................ 7 Safety Properties 7 Liveness Properties 8 Other Threats 9 Findings ..................................................................................................................... 10 Fully transparent transaction can be marked valid in MASP validity predicate 11 Non-authorized users may render useless an arbitrary number of notes 13 Missing privacy checks in the masp validity predicate 15 Requiring that convert descriptions must point to the latest anchor is unnecessarily strict 16 The reward system is limited for NAM owners 17 Earlier rejection of transactions with invalid sapling value balance 19 Minor code improvements 21 Appendix: Vulnerability Classification ..................................................................... 22 Impact Score 22 Exploitability Score 22 Severity Score 23 Disclaimer.................................................................................................................. 25 © 2024 Informal Systems Namada Multi-asset shielded pool

Audit Overview Scope In January and February 2024, Informal Systems conducted a security audit for Heliax. The audit aimed at inspecting the correctness and security properties of Namada’s multi-asset shielded pool (MASP) implementation, with a focus on the following components: • The following files in https://github.com/anoma/namada • crates/sdk/src/masp.rs • crates/core/src/types/masp.rs • crates/shielded_token/src/storage_keys.rs • crates/shielded_token/src/conversion.rs • crates/namada/src/ledger/native_vp/masp.rs • crates/apps/src/lib/node/ledger/shell/init_chain.rs • crates/apps/src/lib/node/ledger/shell/finalize_block.rs • Helper functions in https://github.com/anoma/masp The audit was performed from January 18, 2024 to February 22, 2024 by the following personnel: • Manuel Bravo • Ivan Golubovic • Aleksandar Ljahovic

Relevant Code Commits The audited code was from two repositories at the following commits:

• anoma/namada : hash f7532c20072fd877046857f567735770389cd1d0 • anoma/masp : hash c3c6047a9c9da54058afc71219b913ac9f79e48b

Conclusion We performed a thorough review of the project. We found some subtle problems - more on them in the section Findings. Those problems, if left unattended, would violate both safety and liveness properties. We are glad to report that the dev team has acknowledged our findings and is working towards fixing them.

Audit Dashboard Target Summary • Type: Protocol and Implementation • Platform: Rust • Artifacts: https://github.com/anoma/namada, https://github.com/anoma/masp

Engagement Summary • Dates: 18.01.2024 - 22.02.2024 • Method: Manual code review, protocol analysis

Severity Summary Finding Severity #

Critical 2

High 0

Medium 3

Low 1

Informational 1

Total 7

System Overview Namada’s multi-asset shielded pool (MASP) is a type of privacy-focused asset pool that allows for the shielding of multiple types of assets. It provides a way for users to pool their assets together in a way that hides the identities of the individuals involved and the amounts of the assets being traded. It is designed as an extension to the Sapling circuit which adds support for sending arbitrary assets. Furthermore, MASP is built with mechanisms to align the incentives of users, rewarding those that contribute to shielding by adding assets to the pool. The MASP system is built on top of Anoma’s execution model, which implements a generic computational substrate with WASM-based transactions and validity predicate verification. A validity predicate (VP) is a boolean function that takes four inputs: (i) the transaction itself; (ii) the addresses that are involved with that specific VP; (iii) The storage state before a transaction execution; and (iv) the storage state after the transaction execution. The execution system works as follows: • When a block is decided by the consensus engine, transactions are executed tentatively. A transaction may modify any data in the accounts' dynamic storage sub-space. • Upon transaction execution, the VPs associated with the accounts whose storage has been modified are invoked to verify the transaction. • If any of them reject the transaction, all of its storage modifications are discarded. • If all are accepted, the storage modifications are persisted.

Shielded transactions In Namada, the multi-asset shielded pool is a special Namada account (masp) with an associated validity predicate that handles the verification of shielded transactions, i.e., transactions that interact with the pool. There are three types of shielded transactions: • A fully shielded transaction moves assets within the shielded pool. • A shielding transaction moves assets from outside of the shielded pool to the shielded pool, i.e., shields assets. • An ushielding transaction moves assets out of the shielded pool, i.e., unshields assets. Throughout the report, we use transparent transactions to refer to those transactions that do not interact with the shielded pool: move assets from a transparent address to another transparent address. Shielded transactions are implemented as an optional extension to transparent transfers. The transfer format is as follows:

pub struct Transfer { /// Source address will spend the tokens pub source: Address, /// Target address will receive the tokens pub target: Address, /// Token's address pub token: Address, /// The amount of tokens pub amount: DenominatedAmount, /// The unused storage location at which to place TxId pub key: Option<String>, /// Shielded transaction part pub shielded: Option<Hash>, }

The optional shielded field in combination with the source and target field determines whether the transfer is fully shielded, shielding or unshielding.

• In a fully shielded transaction both the source and target addresses are the masp address. • In a shielding transaction, only the target address is the masp address. • In an unshielding transactions, only the source address is the masp address.

If it is a shielded transaction, through the shielded field one can retrieve a shielded transaction data that with the following format:

pub struct TransactionData<A: Authorization> { /// Transaction format version version: TxVersion, /// A globally-unique identifier for a set of /// consensus rules within the Zcash chain. consensus_branch_id: BranchId, lock_time: u32, /// Latest epoch at which the transaction can be executed expiry_height: BlockHeight, /// Transparent inputs and outputs transparent_bundle: Option<transparent::Bundle<A::TransparentAuth>>, /// Shielded inputs, converts (later introduced) and outputs sapling_bundle: Option<sapling::Bundle<A::SaplingAuth>>, }

In more detail:

• transparent_bundle includes a set of transparent inputs descriptions ( vin ) and outputs descriptions ( vout ). • sapling_bundle includes the set of shielded inputs (aka shielded_spends ), shielded outputs (aka shielded_outputs ), converts (aka shielded_converts ), which we explain later, and the value_balance , which informally is sum(shielded_inputs) + sum(converts) - sum(shielded_outputs).

Rewards and converts To incentivize the use of the multi-asset shielded pool, Namada rewards users who keep their assets shielded in the pool in Namada’s native token (NAM). This is because the more volume of shielded transactions, the more serves its purpose: the more coverage for other users of the shielded pool; privacy is strengthened. The set of assets that participate in the reward system is agreed upon via governance. Rewards are computed at the end of each epoch. This procedure consists of computing how many rewards an amount of a given asset type produces at a given epoch. This information is represented as conversions: an amount Y of an asset type A can be converted to the same amount of the same asset type plus XNAM (YA → YA+XNAM). For instance, if the protocol decides to give 5NAM reward for each shielded BTC during epoch e , the protocol will create a conversion 1BTC@e → 1BTC@(e+1) + 5NAM(e+1). Conversions are stored in a conversion Merkle Tree. The set of conversions that the protocol creates at the end of each epoch defines the set of conversions that users can use to claim their rewards when executing transactions. To claim rewards, users must include convert descriptions in their sapling_bundle . Only convert descriptions that can be proved to exist in the conversion Merkle Tree are allowed by the protocol, i.e., a transaction that includes an invalid convert description is rejected.

On transaction validation and verification Shielded transactions are validated by the masp validity predicate. We now informally describe the conditions by which a shielded transaction must be accepted or rejected by the validity predicate.

Shielding transactions • The source address is transparent. • The target address is the masp address. • Shielded transactions well-formedness: • There are no shielded_spends in the transactions sapling_bundle . • There are no shielded_converts in the transactions sapling_bundle . • Consistency between the Transfer record and the shielded transaction (from Transfer.shielded ) : • The address in each of the transparent inputs ( transparent_bundle.vin ) must match the source address in the transfer record. • The sum of all transparent inputs must match the amount in the transfer record. • The sapling_bundle.value_balance must match the amount in the transfer record. • The asset type of each transparent input must have the current epoch associated. • The token in the asset type of each transparent input must match the token in the transfer record. • Changes to the masp state: • The shileded_output descriptions must be appended to the commitment tree. • No nullifiers must be revealed. • It must pass the verification of verify_shielded_tx , which verifies among other things the integrity of value commitment, note commitment, and ephemeral public key of shielded_outputs , and that the sapling_bundle.value_balance is well computed.

Unshielding transactions • The source address is the masp address. • The target address is transparent. • Shielded transactions well-formedness: • There are no shielded_outputs in the transactions sapling_bundle . • The anchor of the shielded_spends must be valid. • The anchor of the shielded_converts must be valid. • Consistency between the Transfer record and the shielded transaction (from Transfer.shielded ) : • The address in each of the transparent outputs ( transparent_bundle.vout ) must match the target address in the transfer record. • The sum of all transparent outputs must match the amount in the transfer record. • The sapling_bundle.value_balance must match the amount in the transfer record. • The asset type of each transparent output must have an epoch associated not greater than the current epoch. • The token in the asset type of each transparent output must match the token in the transfer record. • Changes to the masp state: • Only the nullifiers associated with the shielded_spends must be revealed. • It must pass the verification of verify_shielded_tx , which verifies among other things the integrity of value commitment, note commitment, and the nullifier of shielded_spends , and that the sapling_bundle.value_balance is well computed.

Fully shielded transactions • The source address is the masp address. • The target address is the masp address. • Shielded transaction well-formedness: • There are no transparent inputs or outputs. • The anchor of the shielded_spends must be valid. • The anchor of the shielded_converts must be valid. • Changes to the masp state: • The shileded_output descriptions must be appended to the commitment tree. • Only the nullifiers associated with the shielded_spends must be revealed. • Privacy: • The tokens in the transfer record must be the native one. • The transfer amount in the transfer record must be zero. • It must pass the verification of verify_shielded_tx , which verifies among other things the integrity of value commitment, note commitment of shielded_spends and shielded_outputs , and that the sapling_bundle.value_balance is well computed.

Threat Analysis In our threat analysis, we start by defining a set of properties required for the correctness of MASP. We separate them into safety and liveness. We have then analyzed them individually to see if they can be violated. A property violation is a potential threat, as detailed for each property. Additionally, we have inspected a set of threats related to integer-type conversions, integer overflow, and DoS attacks. We have listed them at the bottom of this section. We have inspected the listed threats, resulting in the findings presented in the Findings section.

Safety Properties We list a total of 6 safety properties. Each of the properties has been verified assuming both malicious and well- behaving users.

Users cannot steal assets. • Verify that a user can only spend notes if it is authorized. • Verify that a user can only transfer assets to the shielded pool if it owns them. Threat: Users can steal assets. Conclusion: Under the assumption that a different validity predicate validates the ownership of assets for shielding transactions and that the check_spend function verifies that a user can only spend the notes it is authorized to, we conclude that the implementation prevents users from transferring assets or tokens they do not own.
Users cannot double spend: spend more than once the same set of assets. • Verify that when a user spends a note, it reveals the corresponding nullifier. • Verify that when a user attempts to spend a note, the validity predicate checks if its corresponding nullifier has already been revealed. Threat: Users can double spend. Conclusion: The implementation ensures the property.
Users cannot mint or burn assets: create or destroy assets. • Verify that a shielded transaction achieves a net sapling value balance of 0. • Verify that the sum of the net sapling value balance and transparent inputs of a shielding transaction is 0. • Verify that the sum of the net sapling value balance and transparent outputs of an unshielding transaction is

• Verify that a transaction only reveals the nullifiers of the notes it spends. Threat: Users can create or destroy assets. Conclusion: The implementation does not ensure the property. This finding describes a scenario in which users may reveal nullifiers of notes that they do not spend, effectively burning assets.

Users can only issue valid conversions. • Verify that users can only issue conversions between assets in the allowed conversion set. Threat: Users can issue non-allowed conversions by converting incompatible asset types or applying invalid ratios.

Conclusion: Under the assumption that check_convert verifies that the user can only apply allowed conversions, the implementation ensures the property.

The computation of allowed conversions at the end of each epoch is implemented as intended. • Verify that the inflation computed is enough to guarantee that there are enough funds if all clients claim their rewards. • Verify that the parallel computation of the conversions tree is correct. • Verify that the computation of allowed conversions for the native token is as intended. • Verify that the computation of allowed conversions for non-native tokens is as intended. • Verify that the protocol does not create allowed conversions that allow users to mint or burn tokens. Threat(s): Users can mint tokens by applying allowed conversions. The reward system is not working as expected. Conclusion: The implementation ensures the property.
Validity: Only valid shielded transactions pass validation. • Verify that an invalid shielded transaction fails validation. • Verify that a transparent transaction either does not reach validation or fails it. Threat: Invalid transactions pass validation. Conclusion: The implementation does not ensure the property. This describes a scenario in which a transparent transaction passes validation.
Privacy: Fully shielded transactions are private. • Verify that the validity predicate checks that fully shielded transactions are private: the transfer record uses the native token and the transfer amount is zero. Threat: Users can observe the amount and tokens being transferred within the shielded pool. Conclusion: The implementation does not ensure the property. This finding argues that privacy checks are missing in the validity predicate to reject fully shielded transactions that disclose either the token being transferred or the amount.

Liveness Properties

No transaction makes validation crash the node. • Verify that there is no way to crash a node during validation. Threat: Users can crash the system by submitting a transaction that makes the masp validity predicate to panic. Conclusion: The implementation ensures the property.
Assume that the chain is live. If a user submits a valid transaction, then the transaction passes validation and the chain state is eventually updated accordingly. • Verify that if validation is called on a valid transaction, then the transaction passes validation. • Verify that if a user submits a valid fully shielded or unshielding transaction in which it spends some unspent notes it owns, then the transaction passes validation. • Verify that if a user submits a valid fully shielded or unshielding transaction with valid converts, then the transaction passes validation. Threat: Users cannot interact with the shielded pool seamlessly, which may discourage them from using it. Conclusion: The implementation does not ensure the property. This finding describes a scenario in which users may reveal nullifiers of notes that they do not spend. Thus, when a user attempts to spend its unspent notes, it may

be unable to. This other finding argues that the validity check for converts is too strict and may lead to fail valid transactions.

Other Threats

Threat: Type conversions between different integer types are wrong Conclusion: The implementation does not suffer from this issue.

Threat: Overflows and underflows due to inflation computations in the validator Conclusion: The implementation does not suffer from this issue. We still highlight here a couple of computations in the code where we recommend checking for overflows - even if it is very unlikely.

Threat: Data structures in the shielded pool grow without bound by just executing valid shielded transactions. This may result in DoS attacks. Conclusion: The implementation does

Excerpt (19996 of 46983 characters). Read the whole page on informalsystems/audits ↗

← Back to Documentation