2023-02-03 Audit report - Mars Protocol Envoy module

Security Audit Report

Mars Protocol Envoy module: Source Code Analysis

03.02.2023 Last revised 2023/02/27

Contents Audit Overview 4 The Project . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Scope of this report . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Conducted work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Timeline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Further Increasing Confidence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

System Overview 6 Behavior . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Keeper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Transaction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Query . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

Methodology 13 Vulnerability classification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Impact Score . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Exploitability Score . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Severity Score . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

Audit Dashboard 16

Findings 17

Contributions 18

Iterate over all Interchain Accounts 19 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

Mars Hub as Interchain Account Host chain 20 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

Redundant use of ScopedKeeper 21 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

Inconsistent Gov module CLI help 22 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

Non-exhaustive unit tests 24 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

Audit Overview The Project The Delphi Labs LTD team engaged with Informal Systems to conduct a security audit of their implementation of Envoy module as part of their Mars Hub implementation. This module is responsible for automated communication between Mars Hub - the sovereign blockchain implementing Mars Protocol; and its corresponding account, modules, or smart contracts deployed on other IBC-connected chains or outposts. It leverages Interchain Accounts (ICS-27) to make this possible. The module is initiated with a module account. It has three ways to make changes to the blockchain state. • Anyone can create an interchain account of the module account at a given IBC connection. • The other two are done via governance proposal. Anyone can submit a governance proposal to execute a transaction in this module. – To send funds from its account or community fee pool to a remote interchain account over the transfer channel. – To execute some transactions at a remote interchain account over the icacontroller-* channel. The module includes two query APIs that let anyone query the interchain account of the module at a given connection ID or all active interchain accounts of the module.

Scope of this report The agreed-upon work plan was to audit the /x/envoy module in the Mars Hub blockchain at commit c7795c. This report covers the work of the above task that was conducted from January 23, 2023, through February 3, 2023, by Informal Systems by the following personnel: • Ranadeep Biswas • Andrey Kuprianov

Conducted work The Mars protocol team shared onboarding materials and a code walkthrough recording with the Informal Systems team. The Informal Systems team performed manual code analysis and improved the existing tests in the source code. Mars Protocol and Informal Systems teams met weekly to share the findings and the progress.

Timeline • 17 January 2023: Kickoff meeting. – Attendees: Larry and Kris from Delphi Labs LTD, Ranadeep and Tesnim from Informal Systems • 26 January 2023: Sync meeting. (Shared the found issues. Suggested to avoid iterating over all possible ICAs) – Attendees: Larry, Dane, and Kris from Delphi Labs LTD, Ranadeep and Tesnim from Informal Systems • 3 February 2023: Sync meeting. (Patched found issues in a fork. Created an E2E test for the Envoy module) – Attendees: Larry and Kris from Delphi Labs LTD, Ranadeep and Tesnim from Informal Systems

Conclusions The module source code is of high quality - concise and well-documented with explanation and design choices. One High severity issue was found during this audit; the rest were marked Medium or Informational severity. A solution is proposed in a pull request for the high-severity issue. For others, we recommended details that should be addressed to raise the code quality of the module.

Further Increasing Confidence The scope of this audit was limited to manual code review and manual analysis and reconstruction of the protocols. To further increase confidence in the protocol and the implementation, we recommend following up with more rigorous formal measures, including automated model checking and model-based adversarial testing. Our experience shows that incorporating test suites driven by TLA+ models that can lead the implementation into suspected edge cases and error scenarios enable the discovery of issues that are unlikely to be identified through manual review.

System Overview Mars Protocol is a credit protocol that is decentralized, interchain, non-custodial, transparent, algorithmic, and community governed. The entire design of the protocol is out of the scope of this audit. We will only focus on the Envoy module that the Mars Hub (the sovereign blockchain that implements the Mars Protocol) will use to communicate among corresponding accounts, modules, or smart contracts deployed in other chains or outposts as part of the Mars Protocol. It is assumed that the reader is familiar with the Cosmos-SDK and the IBC protocol, specifically IBC token transfer (ICS-20) and Interchain Accounts (ICS-27).

Behavior The Mars Hub is the sovereign blockchain implementing the Mars Protocol. It controls the artifacts and assets deployed in other chains as part of the entire protocol. It leverages Interchain Accounts (ICS-27) to operate in a decentralized, non-custodial way. The implementation is seemingly adapted from the intertx module in the interchain-accounts-demo repo. The Envoy module in Mars Hub is responsible for communicating among different outposts. The module has a module account that can act as any other Cosmos-SDK bank account i.e., it can send and receive balances (on-chain or over IBC). The only way to perform these critical transactions for the Envoy module accounts is via the module itself. The Envoy module requires these critical transactions to be submitted via the Governance module account. So a user can only submit a governance proposal to execute an Envoy module account transactions that send funds or executes transactions on an outpost. Since the entire community will scrutinize the governance proposal, it is fair to assume that it is nearly impossible to execute a malicious critical transaction on behalf of the Envoy module account. Although, the Envoy module allows anyone to register Interchain Accounts of its module account on the outposts. The registration is permissionless because it is harmless to register an interchain account on an open connection to an outpost. If there exists an interchain account already, the transaction does not do anything. Note the outpost must also implement the Interchain Account Host app. Once the Envoy module account has Interchain Accounts registered on an outpost, it is ready to communicate with it. The Envoy module provides two major transaction APIs. • To send funds from its module account to an interchain account at a given IBC channel ID. If the module account does not have enough balance, it will take from the community fee module. Otherwise, it fails. The IBC packets for this transaction are sent via the ibc-transfer channel. • To execute transactions at an interchain account at a given IBC connection ID. The IBC packets for this transaction are sent via the interchain accounts channel. As already mentioned before, these transactions can not be submitted directly. They are supposed to be executed by the Governance module when a governance proposal is passed. Additionally, these behaviors are formally specified in TLA+ language. We verified the specification against few critical invariants. The specification and invariant will be discussed in following sections.

Implementation In this section, we give a detailed analysis of the main components of the Enovy module. We look into the implementation of the application state of the module (Keeper), transaction validation (ValidateBasic and GetSigners), and application logic for executing transactions and querying the application state of the module. We will also describe how the TLA+ specification models the module state and the implementation logic.

Keeper The module consists of a data structure called Keeper, a Cosmos-SDK convention that stores the application state. Usually, a module keeper consists of other module keepers (i.e., the current module is dependent on these other modules) and some other data specific to the module. The following table lists the fields used in the Envoy module keeper and their purpose.

Field Module Purpose accountKeeper auth Calculate the module account bankKeeper bank Calculate the balance of the module account distrKeeper distribution Perform bank transfer from Fee Pool channelKeeper 04-channel IBC information icaControllerKeeper 27-interchain-accounts/controller Interchain Account information scopedKeeper capability Capability keeper authority - The authorized address (gov module)

The formal specification uses the following state variable to model the keeper. VARIABLES * @type: $bankKeeper; bank_keeper,

* @type: $channelKeeper; channel_keeper,

* @type: $icaControllerKeeper; ica_controller_keeper,

* @type: Seq($ibcPacket); ibc_packets,

* @type: $accountId; authority,

* @type: {msg: $msg, success: Bool}; action

• bank_keeper models the bank balances of different accounts including module accounts. • channel_keeper models the keeper of the active channels. • ica_controller_keeper models the keeper for ICA controller keeper. • ibc_packets models the queue for IBC packets. • authority models the authorized address. • action models the executed transaction. accountKeeper, distrKeeper, scopedKeeper are ignored for the sake of simplicity. The following constants are used in the specification. GOV_ACCOUNT == "gov" FEE_POOL_ACCOUNT == "fee_pool" IBC_ESCROW_ACCOUNT == "ibc_escrow" ENVOY_ACCOUNT == "envoy"

ACCOUNTS == {GOV_ACCOUNT, FEE_POOL_ACCOUNT, IBC_ESCROW_ACCOUNT, ENVOY_ACCOUNT, "Alice", "Bob"}

DENOMS == {"umars", "uosmo"}

* connection-0 CONNECTION_ID == 0

REMOTE_MSGS == {"bank/send", "cw/update"}

IBC_TRANSFER_PORT == "transfer" ICA_CONTROLLER_PORT == "ica-controller"

Constant string IDs are used for module accounts for governance module, community fee pool, ibc escrow account, envoy module account. Some additional accounts, Alice and Bob, are included as non-module accounts. Two denoms umars and uosmo are used to model multi-denom balances. The specification models the application behavior on a single connection. It assumes the connection is already established with ID connection-0. Two different strings are used to model multiple types of sdk messages to execute on the interchain account. Lastly, two unique strings are used to model the port IDs for transfer channel and interchain account channel. The model state is initialized with the following predicate. Init == \E _channel_id \in Nat: \E _bank_keeper \in [ACCOUNTS -> [DENOMS -> 0..10]]: /\ bank_keeper = _bank_keeper /\ channel_keeper = SetAsFun({<<_channel_id, [connection_id |-> CONNECTION_ID, port |-> ,→ IBC_TRANSFER_PORT]>>}) /\ ica_controller_keeper = SetAsFun({}) /\ ibc_packets = <<>> * Envoy authority is set to gov module account /\ authority = GOV_ACCOUNT /\ action = [msg |-> Variant("Genesis", 0), success |-> TRUE]

• bank_keeper is initialized with accounts with multiple denoms with arbitrary balances. • channel_keeper is initialized with a single token transfer channel (ICS20) with an arbitrary channel ID. • ica_controller_keeper is initialized as empty. • ibc_packets is initialized as empty. • authority is initialized to the governance module account. • action is initialized with an empty action called Genesis.

Transaction There are three transaction types for the Envoy module. • MsgRegisterAccount • MsgSendFunds • MsgSendMessages ValidateBasic and GetSigners methods are implemented for these transactions. These interface methods are responsible for validating submitted transactions during blockchain runtime. ValidateBasic implementations check if the provided account addresses are valid. Also, they check if the sent fund is non-empty for MsgSendFunds and if the sent list of messages is non-empty for MsgSendMessages, and contains valid messages. GetSigners implementations return the Sender field for MsgRegisterAccount and the Authority field for MsgSendFunds and MsgSendMessages. The application logic for these transaction types is implemented at msg_server.go.

In the specification, the transaction effects are modeled as a disjunction of three different operators corresponding to different transactions RegisterAccountNext, SendFundsNext and SendMessagesNext. Next == / RegisterAccountNext / SendFundsNext / SendMessagesNext

Each operator is described along with the corresponding transactions.

MsgRegisterAccount This takes an IBC connection ID as input. The app logic uses the connection ID to register the interchain account of the Envoy module account at that connection ID. An icacontroller transaction is created using the input and then executed. The IBC events are emitted for relayers to listen and act accordingly. The effect of this transaction is modeled as follows. RegisterAccountNext == \E _connection_id \in Nat: \E _new_channel_id \in Nat: LET _msg == Variant("RegisterAccount", [connection_id |-> _connection_id]) _is_success == * the connection ID must be active /\ _connection_id \in {CONNECTION_ID} * there should not be an existing ICA /\ _connection_id \notin DOMAIN ica_controller_keeper * the new channel ID must be unused /\ _new_channel_id \notin DOMAIN channel_keeper IN IF _is_success THEN /\ channel_keeper' = channel_keeper @@ (_new_channel_id :> [connection_id |-> ,→ _connection_id, port |-> ICA_CONTROLLER_PORT]) /\ ica_controller_keeper' = ica_controller_keeper @@ (_connection_id :> ,→ _new_channel_id) /\ action' = [msg |-> _msg, success |-> TRUE] /\ UNCHANGED <<bank_keeper, ibc_packets, authority>> ELSE /\ action' = [msg |-> _msg, success |-> FALSE] /\ UNCHANGED <<bank_keeper, channel_keeper, ica_controller_keeper, ibc_packets, ,→ authority>>

An arbitrary connection ID is chosen as input. _is_success is defined to be the precondition for a successful execution. The transaction is successful when • The connection ID is active. • There is no other ICA on the same connection ID. • There is a new channel ID to create a new ICA channel over the connection. If the precondition is met, the state variables are updated accordingly. The msg field of action variable is updated to be the transaction message and the success field is set accordingly. For a failure, the state variables are unchanged except the action variable.

MsgSendFunds As inputs, this takes an IBC channel ID, an account address as the authority that submitted this transaction, and a set of coins to be sent from the module account.

IBC channel ID is required because the IBC denoms sent over different channels are non-fungible. So a specific channel ID is necessary. The application logic checks and rejects the transaction if the submitter address is not equal to the authority address maintained by the module keeper - which is set to the Governance module account. The transaction is also rejected if the IBC channel is multi-hop. Mars Hub does not support multi hop channels and intends to connect to their outposts directly. The app logic performs a successful IBC transfer to the interchain account if the bag of coins is non-empty. If the module account does not have the required minimum balance for the transfer, the remaining balance is funded from the Community Fee pool. The application logic uses ibc-transfer app to send the tokens. Unfortunately, it does not support multi-coin transfers. So the coins are sent one by one iteratively. For each ibc-transfer execution, the IBC events are emitted for relayers to listen and act

Excerpt (19999 of 42203 characters). Read the whole page on informalsystems/audits ↗

← Back to Documentation