2024-04-30 Namada ABCI, Replay Protection, Fee And Gas Metering Final Report

Security Audit Report

Namada ABCI, Replay Protection, Fee And Gas Metering

Authors: Manuel Bravo, Aleksandar Ljahovic, Ivan Golubovic

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 ABCI 3 Replay Protection 3 Fee and gas metering 3 Threat Analysis ............................................................................................................ 5 ABCI 5 Replay protection 8 Fees and gas metering 10 Findings ..................................................................................................................... 12 Block could be rejected due to proposer and validators using different minimum gas price 13 Inconsistent Block Size Limit Handling in Proposal Preparation 14 The replay protection hash register is never garbage collected 15 Replay protection can be significantly simplified 16 Incorrect Error Code Mapping in check_proposal_tx Description 18 Error Propagation Issue in EndBlock Handling 19 Code Optimization Recommendations 20 On Streamlining Validation Logic Across Proposal Lifecycle 21 Vulnerability Classification ....................................................................................... 22 Impact Score 22 Exploitability Score 22 Severity Score 23 Disclaimer.................................................................................................................. 25 © 2024 Informal Systems Namada ABCI, Replay Protection, Fee And Gas Metering

Audit Overview Scope In April 2024, Informal Systems conducted a security audit for Heliax. The audit aimed at inspecting the correctness and security properties of Namada’s ABCI custom implementation, fee system and gas metering and replay protection implementation, with a focus on the following components: • The following files in https://github.com/anoma/namada • crates/apps/src/lib/node/ledger/shims • crates/apps/src/lib/node/ledger/shell • crates/apps/src/lib/node/ledger/mod.rs • crates/apps/src/lib/node/ledger/storage/rocksdb.rs (partially) • crates/apps/src/lib/node/ledger/shell/mod.rs (partially) • crates/gas • crates/state/src/wl_state.rs (partially) • crates/state/src/write_log.rs (partially) • crates/namada/src/ledger/protocol/mod.rs (partially) • crates/replay_protection/src/lib.rs • crates/parameters/src 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 the repository at the following commit:

• anoma/namada : hash f4c838d2c53b28091af9b9a2f10b5b53e55fe65e

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 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

Engagement Summary • Dates: 28.03.2024 - 30.04.2024 • Method: Manual code review, protocol analysis

Severity Summary Finding Severity #

Critical 2

High 0

Medium 1

Low 0

Informational 5

Total 8

System Overview Namada is a proof-of-stake layer-one blockchain, powered by the CometBFT (formerly Tendermint) BFT consensus algorithm. This blockchain ecosystem includes multi-asset shielded transfers through a versatile multi-asset shielded pool derived from the Sapling circuit. Offering comprehensive support for the Inter-Blockchain Communication (IBC) protocol and integrated Ethereum bridge, Namada introduces a robust proof-of-stake system with cubic slashing, stake-weighted governance signaling, and a novel dual public goods funding approach. Users are incentivized through native protocol tokens (NAM) for their contributions to the shielded set, reinforcing a commitment to data protection. The report is focused on three parts of this audit: ABCI, Replay protection and fee and gas metering.

ABCI Namada has developed a custom ABCI (Application Blockchain Interface) implementation built upon CometBFT v0.37. They have implemented a wrapper around CometBFT to incorporate ABCI++ features. The system comprises a shell that implements ABCI++ and a shim that wraps it. The shim is utilized to translate between the ABCI interface of the current CometBFT version and the shell's interface. For instance, the shim implements BeginBlock, DeliverTx, and EndBlock functions, which gather data and, ultimately, invoke the shell's FinalizeBlock function at the EndBlock stage. In this part of the code, the prepare proposal is also implemented, where the selected proposer decides on the transactions to be included in the block, and the process proposal through which other validators verify that proposal. Since there are Protocol and Wrapper transactions (which include inner transactions), their distribution in the block is managed through a block allocator. Additionally, a mechanism for vote extensions has been implemented, although it was not within the scope of the audit.

Replay Protection Replay protection is safeguarding against malicious actors attempting replay attacks, where previously executed transactions are resubmitted to the ledger. Such attacks disrupt the intended state of the system, inflicting economic harm on the fee payer by causing them to incur additional costs. If the original transaction involved value transfer, the sender may suffer further financial loss. Given that attackers can exploit well-formatted transactions without modification, replay attacks pose a significant threat and must be effectively countered. Namada's implementation of replay protection mitigates the risk posed by replay attacks by preventing the execution of duplicate transactions. Leveraging the encrypted and authenticated communication channels provided by CometBFT, Namada ensures secure transmission of transactions between nodes. Transactions consist of two components: a WrapperTx and an inner Tx, facilitating the exchange of data defining ledger state transitions within the Namada protocol. The implementation of replay protection in Namada comprises several key components aimed at replay attacks and ensuring the integrity of transactions. These include a robust hash-based solution for both WrapperTx and EncryptedTx, mitigating the risk of attackers extracting and replaying inner transactions. Additionally, Namada implements checks within mempool_validate and process_proposal to verify the uniqueness of transactions, rejecting any duplicates. The inclusion of a ChainId identifier and transaction expiration further enhances security by binding transactions to specific forks and imposing a time limit for execution, respectively.

Fee and gas metering Namada's fee system plays a crucial role in maintaining the integrity and efficiency of its ledger. Transaction fees serve a dual purpose: to allocate block space and gas efficiently and to incentivize block producers to prioritize transactions. These fees can be paid in any fungible token listed on Namada's whitelist, with minimum fee rates set

by governance. Additionally, when utilizing the shielded pool, transactions can unshield tokens to cover the required fees. The token whitelist, comprising token identifiers and minimum gas prices, is periodically updated through governance proposals. All fees collected are directly paid to the block proposer, ensuring an incentive-compatible system. Namada's upfront fee payment mechanism prevents denial-of-service attacks by ensuring transactions pay for resources upfront, enhancing block inclusion efficiency and discouraging spam.

The Fee field within the WrapperTx struct encapsulates the payment data, including the fee amount and token address. The fee payer, typically the signer of the wrapper transaction, specifies the token and amount, meeting the minimum gas price set by the whitelist. These parameters incentivize block proposers to prioritize transactions. Validators validate these parameters during block construction, ensuring the integrity of the process. Gas accounting in Namada is a process designed to manage the utilization of two critical resources within a block: gas and space. Each transaction incurs a fixed amount of gas per byte to address the space limit, ensuring efficient allocation. Gas limits are calculated for transactions and validity predicates, considering factors such as the runtime cost of wasm code and validity predicate requirements. To prevent transactions from exceeding their gas limits, a gas counter is embedded within each transaction and VP, allowing real-time monitoring of gas consumption. This mechanism enables immediate validation against the declared GasLimit set in the corresponding wrapper transaction.

In this audit, the fee payment system and gas metering were followed through prepare_proposal , process_proposal and finalize_block .

Threat Analysis ABCI

The set of transactions in Namada’s prepareProposal response exceeds the maximum amount of bytes Consequences:

• It violates Requirement 2 [ PrepareProposal , tx-size] of the ABCI++ 0.37 specification: when p's Application calls ResponsePrepareProposal , the total size in bytes of the transactions returned does not exceed RequestPrepareProposal.max_tx_bytes . • It compromises liveness as the consensus engine will reject proposals from honest validators that exceed the maximum allowed. Conclusion: The implementation suffers from this threat, see Inconsistent Block Size Limit Handling in Proposal Preparation

Honest validators reject proposals from honest proposers Consequences:

• It violates Requirement 3 [ PrepareProposal , ProcessProposal , coherence] of the ABCI++ 0.37 specification: for any two correct processes p and q, if q's CometBFT calls RequestProcessProposal on up, q's Application returns Accept in ResponseProcessProposal . • It compromises liveness as validators will reject proposals coming from honest proposers. Conclusion: The implementation does not suffer from this threat. It has been verified that every proposal generated from prepareProposal will be guaranteed to be accepted by processProposal . Some checks are performed by the proposer in the prepare proposal phase, while others are done when adding to the mempool. Certain validations related to time (expiration, epoch) are correctly verified in the mempool through Recheck .

Namada’s processProposal is non-deterministic, i.e., its result does not depend exclusively on the proposal and the committed blockchain state Consequences:

• It violates Requirement 4 [ ProcessProposal , determinism-1]: of the ABCI++ 0.37 specification: ProcessProposal is a (deterministic) function of the current state and the block that is about to be applied. In other words, for any correct process p, and any arbitrary block u, if p's CometBFT calls RequestProcessProposal on u at height h, then p's Application's acceptance or rejection exclusively depends on u and sp,h-1. • It compromises liveness as validators will reject proposals coming from honest proposers.

Conclusion: Upon analysis of ProcessProposal , it has been determined that it executes deterministically, meaning that the outcome depends exclusively on the proposal and the committed blockchain state.

Additionally, it is important to note that functions validate_eth_events_vext , validate_bp_roots_vext , and validate_valset_upd_vext , located on the Ethereum bridge, were

not extensively analyzed within this determinism assessment. However, it was assumed that these functions are deterministic.

Namada’s prepareProposal and/or processProposal modify the blockchain state Consequences: • It violates Requirement 9 [all, no-side-effects]: of the ABCI++ 0.37 specification: p’s calls to RequestPrepareProposal , RequestProcessProposal at height h do not modify sp,h-1. • It compromises safety, as at prepareProposal and processProposal , the proposal has not yet been decided, so it may need to be rolled back. Conclusion: Through analysis, it has been determined that the requirement is satisfied. The original states are only used for retrieving information, while all modifications are performed on a temporary object ( temp_state = self.state.with_temp_write_log(); ) which is re-instantiated in each prepareProposal and processProposal executions.
Namada’s beginBlock , deliverTx and endBlock are non- deterministic, i.e., its result does not depend exclusively on the proposal and the committed state Consequences:

• It violates Requirement 11 [ BeginBlock - DeliverTx - EndBlock , determinism-1] of the ABCI++ 0.37 specification: for any correct process p, sp,h exclusively depends on sp,h-1 and vp,h. • It violates Requirement 12 [ BeginBlock - DeliverTx - EndBlock , determinism-2] of the ABCI++ 0.37 specification: for any correct process p, the contents of Tp,h exclusively depend on sp,h-1 and vp,h. • It may violate safety as validators may end up with different blockchain states after processing the same set of blocks in the same order.

Conclusion: This threat has been analyzed specifically for the requests BeginBlock , DeliverTx , and EndBlock within the run function in abcipp_shim.rs (/shims/abcipp_shim.rs#L105-L174).

• BeginBlock and DeliverTx : These requests simply store data received from CometBFT, which is part of the proposal. Adding events to the response in DeliverTx does not affect determinism. • EndBlock : In this phase, all data is obtained from the proposal and the current state ( block_time , block_proposer , etc.). All subsequent functions called are deterministic ( process_tx , swap , zip , push , etc.) and are invoked exclusively with data from the proposal or the state.

Therefore, based on the analysis, it can be concluded that the operations performed within BeginBlock , DeliverTx , and EndBlock requests do not compromise determinism as they strictly adhere to using proposal data or current state information.

Namada persists blockchain state before commit is called Consequences: It may violate safety as validators may end up with different blockchain states after processing the same set of blocks in the same order. This is because each validator may execute a different set of ABCI calls. The

consensus engine only guarantees that all validators eventually commit the same set of blocks in the same order, but each validator may execute different sets of processProposal calls.

Conclusion: The implementation does not suffer from this threat. Any changes made to transaction-related states will be rolled back in case of an error during transaction execution. On the other hand, information related to the block (block height, epoch, block hash, etc.) must be stored regardless of the success of transaction execution, which is correctly implemented.

The shim implementation of finalizeBlock from the CometBFT 0.37 ABCI API is incorrect Consequences: Unknown/unpredictable behavior. Conclusion: The implementation does not suffer from this threat, but during the analysis, we caught this related informational finding:Error Propagation Issue in EndBlock Handling
Malicious proposers can censor non-expired transactions by biasing the block time Consequences: Malicious validators can censor valid transactions at will. Conclusion: Through the analysis of this threat, it has been determined that a malicious proposer does not have the ability to censor non-expired transactions. On CometBFT, the block time is generated and distributed to validators through requests, both in the prepare proposal phase and the process proposal phase. Furthermore, any attempts by a proposer to manipulate the time would be ineffective, as validators verify the expiration of transactions during the process proposal phase using the time provided by CometBFT through requests. The expiration time of a transaction is located in the transaction header and is signed by the transaction creator. Since the transaction signature is verified during the process proposal phase, it is not feasible for a malicious proposer to alter the expiration time of a transaction. This analysis provides assurance that the integrity of transactions remains protected from malicious attempts at censorship by proposers.
Proposals generated by honest proposers include invalid wrapper transactions Consequences: It compromises liveness, as honest proposers may get their proposals rejected because of this. Conclusion: The implementation does not suffer from this threat. The proposer in the prepare proposal phase checks the following aspects related to wrapper transactions: signature validity, ensuring that the gas limit is below the block gas limit, correctness of the ChainId , ensuring that the transaction has not expired, acceptance of tokens for fee payment and possession of the minimum required amount. If the transaction includes an unshielding transaction, it is considered valid.
Validators accept proposals that include invalid wrapper transactions Consequences: Malicious proposers can waste block space by including invalid wrapper transactions. Conclusion: The implementation does not suffer from this threat. Validators in the process proposal phase verify the following aspects related to wrapper transactions, and in case of invalidity of any wrapper transaction, they will reject the proposal: signature validity, ensuring that the gas limit is below the block gas limit, correctness of the ChainId , ensuring that the transaction has not expired, acceptance of tokens for fee payment and possession of the minimum required amount. If the transaction includes an unshielding transaction, it is considered valid.

Proposals generated by honest proposers include invalid inner transactions Consequences: It compromises liveness, as honest proposers may get their proposals rejected because of this. Conclusion: The implementation does not suffer from this threat. In the prepare proposal phase, the proposer verifies the following aspects related to inner transactions: it passes the replay protection check, and it is one of the predefined transactions. If an error occurs, transaction will not be included in the proposal.
Validators accept proposals that include invalid inner transactions Consequences: Malicious proposers can waste block space by including invalid inner transactions. Conclusion: The implementation does not suffer from this threat. Validators in the process proposal phase verify the following aspects related to inner transactions, and in case of invalidity of any inner transaction, they will reject the proposal: it passes the replay protection check, and it is one of the predefined transactions.

Replay protection

A committed inner transaction can be

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

← Back to Documentation