Namada Q2 2025 E2E Shielded Transaction & Balance Consistency Audit Report Final

Security Audit Report

Q2 2025 NAMADA: E2E SHIELDED TRANSACTION & BALANCE CONSISTENCY

Authors: Last Revised Manuel Bravo, Aleksandar Sto- 2025/07/24 janovic, Ivan Golubovic, Tatjana Kirda Q2 2025 Namada Security Audit Report

Contents Audit overview 3 The Project . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Scope of this report . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Audit plan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

Audit Dashboard 5 Target Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Engagement Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Severity Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

System Overview 6

Threat Model 8 Property 01: The transaction builders guarantee at execution time that (i) the fee amount of the fee token is greater than or equal to the minimum fee amount, and (ii) the fee payer has enough balance . . . 8 Property 02: Fee payer has sufficient funds and fee meets minimum requirements during prepare proposal 9 Property 03: Fee payer has sufficient funds and fee meets minimum requirements during process proposal 10 Property 04: An executed transfer transaction decreases the fee payer balance of the fee token by (gas limit * fee amount). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Property 05: An executed transfer transaction increases the block proposer’s balance of the fee token by (gas limit * fee amount) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Property 06: Let t be a transaction included in a decided block b and assume that the transaction is committed, i.e., passes validation. Then, the transaction uses at most the gas limit of the transaction. 13 Property 07: Let t be a committed transfer transaction, c its corresponding transfer command and s a source component in c.sources. Then, the s.source balance for s.token is greater than or equal to the s.amount right before the execution of the transaction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Property 08: Given a transfer transaction t built via a transfer command, then it is committed if it is accepted, the transaction uses no more gas than the transaction’s gas limit, and let c be the transaction’s corresponding transfer command. For any source component s in c.sources, the s.source balance for s.token is greater than or equal to the s.amount right before the execution of the transaction. . . 15 Property 09: Let t be a committed transfer transaction, then the balances of the involved parties decrease and increase accordingly. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Property 10: Let t be a committed shielding transaction and c its corresponding transfer command Then, for each target component g in c, the MASP balance for g.token increases by g.amount. . . . . . . . . 19 Property 11: Let t be a committed unshielding transaction and c its corresponding transfer command. Then, for each source s in c, the MASP balance for s.token decreases by s.amount. . . . . . . . . . . . 20 Property 12: Let t be a committed shielded transaction and c its corresponding transfer command. Then, the balance of the MASP address remains unchanged. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Property 13: If a transaction t increases or decreases the balance associated with the MASP address, then the MASP VP is used for validation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Property 14: If a transaction t increases or decreases the balance associated with a given extended full viewing key, then the MASP VP is used for validation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Property 15: The balance associated with a viewing key only decreases if the corresponding user authorizes it. 23 Property 16: The balance associated with a viewing key only increases as a consequence of a shielding or shielded transaction that authorizes a transfer targeting the viewing key. . . . . . . . . . . . . . . . . . . 25

Property 17: Let n be an honest node. After a client synchronizes its shielded state with n via shielded sync the client’s note commitment tree matches the node’s note commitment tree, the client’s the notes index matches the node’s the notes index, the client’s the witnesses map matches the node’s the witnesses map, the client’s the set of nullifiers matches the node’s the set of nullifiers, the set of non-spent notes owned by the client’s spending key . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Property 18: Let c be a transfer command. Assume that the command is successfully executed and let t be the resulting transaction. The transaction is then well-formed. . . . . . . . . . . . . . . . . . . . . . . . 29

Findings 33 Transactions doing masp fee payment may be executed an unbounded number of times for free . . . . . 34 Inconsistent handling of overflowing transactions between prepare and process proposal . . . . . . . . . . 35 Overflow due to expiration height computation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Potential height inconsistency between shielded state components when fetching from indexers . . . . . 37 Shielded sync recovery after dishonest node . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Unused recoverable error logic in process proposal and finalize block . . . . . . . . . . . . . . . . . . . . . . . 39

Appendix: Vulnerability classification 40

Disclaimer 43

Audit overview The Project From May 2025 to June 2025, the Anoma Foundation engaged Informal Systems to work on a partnership and conduct a security audit. The audit was concerned with the end-to-end execution of shielded transactions with a focus on the consistency of user balances.

Scope of this report The scope includes the following main items from the Namada codebase ↗:

● Shielded sync – crates/apps_lib/src/client/masp.rs. Main function: syncing ● Transaction construction – crates/apps_lib/src/cli/client.rs. Main functions: TxShieldedTransfer, TxShieldingTransfer, TxUn- shieldingTransfer – crates/apps_lib/src/client/tx.rs. Main functions: submit_shielded_transfer, submit_shielding_- transfer, submit_unshielding_transfer and submit_ibc_transfer – crates/sdk/src/tx.rs. Main functions: build_shielded_transfer, build_shielding_transfer, and build_unshielding_transfer – crates/shielded_token/src/masp/shielded_wallet.rs. Main function: gen_shielded_transfer – masp_primitives-1.4.0/src/transaction/builder.rs. Main function: build – crates/sdk/src/tx.rs. Main functions: build, prepare_tx, process_tx, broadcast_tx, and submit_tx ● Transaction execution: – crates/node/src/shell/prepare_proposal.rs – crates/node/src/shell/process_proposal.rs – crates/node/src/shell/finalize_block.rs. Main functions: finalize_block, retrieve_and_execute_- transactions, and execute_tx_batches – crates/node/src/protocol.rs. Main functions: apply_wrapper_tx, dispatch_tx, dispatch_inner_txs, ap- ply_wasm_tx, and execute_tx – crates/vm/src/wasm/run.rs. Main function: tx – wasm/tx_transfer/src/lib.rs. Main function: apply_tx ➞ Other related functions such as token::multi_transfer, apply_transparent_transfers, multi_trans- fer, and apply_shielded_transferwere also included in scope. – crates/token/src/tx.rs. Main functions: multi_transfer, and apply_shielded_transfer ● Transaction validation: – crates/node/src/protocol.rs. Main functions: check_vps, and execute_vps – MASP VP: crates/shielded_token/src/vp.rs – Multitoken VP: crates/trans_token/src/vp.rs

The code in scope was audited at the 3531f980fa5be4274d5b50f52e165f3b6b2882db commit hash. Notably, the MASP code ↗ was out of the scope of this audit, and the zk-related verification logic was not inspected.

Audit plan The audit was conducted between May 27, 2025 and June 24, 2025 by the following personnel:

● Ivan Golubovic ● Tatjana Kirda ● Aleksandar Stojanovic

● Manuel Bravo

Conclusions No critical issues were identified within the defined scope of this audit. However, two medium severity issues were found in components outside the audit scope, specifically within the process_proposal and prepare_proposal code paths. In total, six findings were reported: two classified as medium severity, two as low severity, and two as informational. Detailed information on each issue is provided on the Findings page. Notably, validity predicates assume that only predefined, whitelisted transactions are executed, introducing implicit dependencies on specific transaction execution logic. While transaction types are restricted via allowlists (code ref ↗), VPs assume that certain invariants hold based on the expected transaction implementation. These include, for example, source and target accounts balance changes being enforced accurately by the transfer WASM code (code ref ↗), and the correct population of the debited_accounts (code ref ↗).

Audit Dashboard Target Summary ● Type: Implementation ● Platform: Rust ● Artifacts: Namada repository ↗

Engagement Summary ● Dates: 27.05.2025 - 24.06.2025 ● Method: Manual code review

Severity Summary

Finding Severity Number

Critical 0 High 0 Medium 2 Low 2 Informational 2 Total 6

System Overview We include a set of definitions and assumptions that will be used in the threat model. The properties in the threat model define the desired behavior of the components under scope.

Definitions A transfer command is one of the following cli commands: TxShieldedTransfer, TxShieldingTransfer, TxUn- shieldingTransfer and includes at least the following arguments:

● A set of sources. Each is composed by: – source is an extended spending key or a Namada address – token address – amount is any quantity ● A set of targets. Each is composed by: – target is a shielded payment address or a Namada address – token address – amount is any quantity ● Fee payer defines the fee payer. It can be an extended spending key if the fee is paid with tokens managed by MASP, or a Namada address if not. ● Fee token is the token in which the fee will be paid by the fee payer.

● Fee amount is the amount of fee tokens that the fee payer is willing to pay per gas unit.

● Gas limit is the maximum amount of gas that the fee payer is willing to pay.

A transfer transaction is the result of executing a transfer command. Their builders define its validity and well- formedness. It includes the following arguments:

● A transparent bundle with a set of transparent inputs (vin) and outputs (vout). A transparent input includes an asset, amount, and source address. A transparent output includes an asset, amount, and target address. ● A sapling bundle with shielded spends, converts, and outputs descriptions.

● Fee payer, fee token, fee amount, and gas limit.

Four transaction states:

● Submitted: A transaction is considered submitted once it is being successfully created. It is the transaction’s initial state. ● Accepted: A transaction becomes accepted when it is included in a block proposal that is accepted by the

validators. ● Executed: A transaction becomes executed after its execution in finalize block.

● Validated: A transaction becomes validated after its validation in finalize block. If the transaction passes validation,

we say that the transaction is committed, i.e., its state changes are persisted. If the transaction fails validation, we say that the transaction is rejected, i.e., its state changes are discarded.

Assumptions Assumption 1: A client always executes shielded synchronization before submitting a shielded, shielding, or unshielding command. Assumption 2: A submitted transaction is eventually included in a block proposal of an honest proposer under

good network conditions, i.e., if validators accepts the proposal via processProposal, the block will be committed. Assumption 3: The MASP rewards inflation is well computed, and sufficient funds are minted at the MASP address.

Threat Model Property 01: The transaction builders guarantee at execution time that (i) the fee amount of the fee token is greater than or equal to the minimum fee amount, and (ii) the fee payer has enough balance Violation consequences If there is no check and the user picks a fee amount that it is smaller than the fee amount, it is then likely that the transaction is never included in a block. This would pose a liveness issue. Missing the balance check would pose a similar problem.

Threats ● Threat 1.1. There is no code checking that the fee amount is greater or equal to the minimum fee amount. ● Threat 1.2. There is no code checking that the balance of the fee payer is greater or equal to the total fee.

Conclusion The property does not hold. The main reason is that any blockchain state that the client uses to validate the transaction’s input may be outdated at the time of the transaction’s execution. This is a fundamental issue that cannot be overcome. Given this impossibility, we check a weaker property: Given a blockchain state fetched from an honest node, the builders check that based on the latest fetched blockchain state (i) the user’s proposed fee amount is greater than or equal to the minimum fee amount, and (ii) the fee payer has enough balance to pay for the transaction’s fee. We now provide conclusions for each of the threats.

Threat 1.1. conclusion The threat is not applicable. The builders validate fee-related data in the validate_fee function. Let minimum_fee be the minimum amount retrieved from the node and fee_amount the one provided by the user as input. If the user does not set the force flag to true (the relevant case), the function returns either an error, e.g., if there is no minimum fee for that token in the fetched state, or the maximum between minimum_fee and fee_amount. The function is used in the three transaction builders in scope: build_shielded_transfer, build_shielding_- transfer and build_unshielding_transfer. Furthermore, the value returned is used by the transaction builder at the end of this process to set the transaction’s fee amount, which ensures the required.

Threat 1.2. conclusion The threat is not applicable. The build_shielding_transfer builder validates the fee payer balance in validate_transparent_fee. The func- tion returns an error if the fee payer does not have enough balance to pay the fees, unless in force mode. The build_shielded_transfer and build_unshielding_transfer builders validate the fee payer’s balance either in get_masp_fee_payment_amount is the fees are paid from a transparent address or implicitely when they compute shielded inputs (in compute_change) if the fees are paid from MASP.

Property 02: Fee payer has sufficient funds and fee meets minimum require- ments during prepare proposal Let t be a transaction included in a block proposal b. An honest proposer includes t in a proposal via prepare_- proposal if

● the fee payer is guaranteed to have sufficient funds to cover the transaction execution, i.e., the fee payer balance of the fee token during the transaction’s execution is greater than or equal to (gas limit * fee amount) ● the fee amount is greater than or equal to the minimum fee amount for the given token during the transaction’s

execution.

Violation consequences ● Transactions with insufficient fee payer balances or inadequate fee amounts may be included in block proposals, leading to failed fee transfers during block execution. This results in transaction failures, wasted computational resources, and potential economic losses for validators who cannot collect fees from failed transactions.

Threats ● Threat 2.1. There is no code checking that the fee payer has sufficient funds. ● Threat 2.2. There is code checking that the fee payer has sufficient funds, but it does not consider that the fee payer may also be the fee payer of some preceding transactions in the same block. ● Threat 2.3. There is no code checking that the fee amount is greater than or equal to the minimum fee amount

for the given token. ● Threat 2.4. There is code checking that the fee amount is greater than or equal to the minimum fee amount for

the given token but it does not consider that the minimum can be updated via governance.

Conclusion The property holds.

Threat 2.1. conclusion The threat is not applicable. Check for sufficient funds is done in the transfer_fee function (ref ↗). The function reads the fee payer’s balance and uses checked_sub to verify sufficient funds before attempting the transfer. If insufficient funds are detected, MASP fee payment (ref ↗) is attempted by executing the first transaction of the batch to unshield funds, then balance check is done again. If the fee payer still has insufficient funds after the MASP payment attempt, the transaction is rejected.

Threat 2.2. conclusion The threat is not applicable. The temporary state mechanism in prepare_proposal (ref ↗) creates an isolated environment with its own write log for transaction simulation. Using this mechanism mitigates threat because when simulating transactions, each transaction’s effects, including fee payments, are accumulated in the temporary write log. All the balance changes from all preceding transactions are considered, as those changes are reflected in the write log.

Threat 2.3. conclusion The threat is not applicable.

Minimum gas price is determined (ref ↗) by comparing consensus-mandated minimum and proposer’s own minimum, using the higher value. The fee_data_check (ref ↗) ensures the fee amount per gas unit is greater than or equal to the minimum gas price for the given token.

Threat 2.4. conclusion The threat is not applicable. While the governance can update minimum fee amounts, these changes are applied during block finalization (ref ↗) and take effect in the next block. Even though finalize_gov is called before transaction executions during finalize_block, checks that use parameters that can be updated through governance are not done during finalize_block. For example, inside apply_wrapper_tx transfer_fee is called (ref ↗) without prior check if fee is above minimum fee as it is done during prepare and process proposal (ref ↗).

Property 03: Fee payer has sufficient funds and fee meets minimum require- ments during process proposal Let t be a transaction included in a block proposal b. A validator accepts a b in processProposal if

● the fee payer is guaranteed to have sufficient funds to cover the transaction execution, i.e., the fee payer balance of the fee token during the

Excerpt (19987 of 111768 characters). Read the whole page on informalsystems/audits ↗

← Back to Documentation