report

Security Audit Report

Interblockchain Communication Protocol: Specification and Code

Contents

Audit overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Audit Dashboard . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Engagement Goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Coverage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 Recommendations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Short term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Long term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Findings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Specification Findings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 ICS20 - Refund logic differs between code and specification . . . . . . . . . . . 16 Faulty semantics underspecified . . . . . . . . . . . . . . . . . . . . . . . . . . 18 ICS04 - Incorrect Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 ICS18 - Relayer underspecified . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 ICS02 - Suggestions for restructuring . . . . . . . . . . . . . . . . . . . . . . . 24 ICS20 - Specification allows token lost issue in the crossing hellos scenario . . . 26 ICS20 - Type mismatch for amount packet field between code and spec . . . . . 28 Code Findings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ICS07 - Tendermint Client: wrong usage of unbonding period . . . . . . . . . . 30 Malicious IBC app module can claim any port or channel capability using Lookup- ModuleByPort/ByChannel . . . . . . . . . . . . . . . . . . . . . . . . . 32 ICS20 - Escrow address collisions . . . . . . . . . . . . . . . . . . . . . . . . . 36 ICS03/04 - Crossing hellos with fixed identifier are not live . . . . . . . . . . . . 41 Non-atomicity of operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ICS20 - Model and Model-based Tests for Token Transfer . . . . . . . . . . . . 48 ICS20 - Panic on receiving multi-chain denominations . . . . . . . . . . . . . . 51

Audit overview

In December 2019, the Interchain Foundation engaged Informal Systems to take leadership over the implementation of the Inter-Blockchain Communication (IBC) Protocol in Rust and to formally specify the protocol in TLA+. Starting October 26 2020, the Informal Systems team conducted an internal audit of the existing IBC specification in English and implementation in Go. The audit was conducted over the course of eight person-weeks with four research engineers. Note that engineers involved in the audit were primarily those that had not worked on the Rust and TLA+ IBC deliverables; that said, some members of the audit team already had a good understanding of the IBC protocols and familiarity with the SDK code base. We audited the relevant components in the IBC directory of the Cosmos-SDK, working from commit hash 6cbbe0d, and the corresponding IBC specification, working from commit hash 7e6978a. The github.com/cosmos/relayer repository, which implements the IBC relayer in Golang, was not in the scope. Throughout the process, we worked closely with the Interchain GmbH team in order to continuously integrate the outputs of the audit, so the code and the specification were moving targets during the audit. We want also to note that many of our recommendations were already addressed in the meantime (SDK#8006, SDK#7993, SDK#8145, SDK#8119, SDK#7967, SDK#7770 and ICS#493). The audit was conducted in a top down approach, starting from the implementation of the token transfer application (ICS20), and moving down the IBC stack analysing the implementations of channels and packets (ICS04), connections (ICS03) and clients (ICS02 and ICS07). For each ICS we started by thoroughly inspecting the specification; we formalized the protocol by writing pre-conditions and post-conditions of the core functions that constitute the protocol (see models directory). We then reviewed the code with a focus on finding (a) discrepancies between the code and the specification and, (b) possible vulnerabilities. The audit of the Token Transfer application (ICS20) surfaced several issues: • IF-IBC-01, IF-IBC-02, IF-IBC-06 and IF-IBC-07 pointed out the discrepancies between the implementation and the specification that might lead to some attack scenarios due to user misunderstanding the specification. Furthermore, it could lead to the insecure (future) implementations of the protocols. • IF-IBC-10 captures the protocol/implementation bug related to escrow address collisions • IF-IBC-12 points to some poor software practices and lack of proper documentations. • IF-IBC-13 and IF-IBC-14 capture the initial work on model based testing (MBT) of token transfer application, which caught a panic triggered by multi-chain token denominations. After ICS20, we moved to channels and packets (ICS04). In addition to the imprecise specifications

and discrepancies between the implementations and the specification (IF-IBC-02), we realised that the definitions of properties were imprecise and that they might mislead users, leading to risky scenarios that could result in loss of funds (IF-IBC-03). Furthermore, we identified a protocol/implementation bug whereby a malicious relayer could prevent the connection and channel handshakes from terminating (IF-IBC-11). In parallel with the audit of the ICS04 implementation, we took a more general look at the object capabilities implementation in the Cosmos SDK as it is a critical security component. We captured some issues in IF-IBC-09 in the context of the IBC port and channel keepers, although it can be seen as a more general issue of the SDK’s object capability system. Apart from IF-IBC-11, no major issues were found with respect to ICS03. With respect to clients (bottom of the IBC stack), we found a protocol bug in the Tendermint light client implementation (IF-IBC-08), and suggested major restructuring of ICS02 in IF-IBC-05 to improve its clarity and rigor. Furthermore, we reviewed ICS18 (though we haven’t carefully reviewed Go implementation of the relayer), and wrote up our findings in IF-IBC-04; in short, the relayer logic is significantly underspecified with several important points left open, that could lead to wrong implementations. Considering the importance and security risks of Token Transfer (ICS-20), we have invested some time into developing model based tests based on TLA+ specifications. The approach taken is captured in IF-IBC-13 and the bug found using MBT is explained in IF-IBC-14. Note that two additional aspects of IBC were not covered in this audit. The first is ICS23 and its implementation. The second is the upgrade logic for connections and channels, which is not captured in the specification. We recommend the upgrade logic be captured more clearly in the specification, and that both these aspects of the specification and code receive further review. In addition to those major findings, we have created several issues on both cosmos-sdk and cosmos/ics repositories and engaged with the team at Interchain Berlin in helping them address the most critical ones. Overall, our team found the protocol to be well designed and implemented. However, we anticipate that early IBC adopters may have a hard time correctly navigating through and understanding the specification, i.e., the specification could benefit from improved clarity and better organisation. Furthermore, misunderstanding of the guaranteed properties might lead to insecure implementations and wrong usage. We have made several concrete recommendations in this report how this can be improved. At the implementation level, the major issues come from the integration of the IBC implementation in the Cosmos SDK framework. This made it hard to understand the execution model in which IBC handlers run, the atomicity assumptions of functions and error handling and propagation. Furthermore, the implementation of capabilities framework might lead to security issues where a malicious IBC module could be able to obtain the capability associated with any

channel, and send/receive messages on another modules channel. Although code has pretty good test coverage, our recommendation is to take advantage of the TLA+ specifications of the IBC protocol to implement model based tests (MBT) for the complex corner cases of the critical components of the stack, following the example demonstrated during the audit. Finally, we want to note that although we have found several discrepancies between the code and the specification, the code had usually implemented things correctly or took other defensive measures.

Audit Dashboard

Target Summary • Name: Interblockchain Communication Protocol • Code Version: 6cbbe0d4ef90f886dfc356979b89979ddfcd00d8 • Specification Version: 7e6978ae551bbed439c69178184dea0a25d0e747 • Type: Implementation • Platform: Golang Engagement Summary • Dates: October 26 through November 19 2020 • Method: Whitebox • Employees Engaged: 4 • Time Spent: 8 person-weeks Vulnerability Summary

Issue Type # Finding Total High-Severity Issues 4 IF-IBC-06, IF-IBC-09, IF-IBC-10, IF-IBC-14 Total Medium-Severity Issues 5 IF-IBC-01, IF-IBC-02, IF-IBC-03, IF-IBC-08, IF-IBC-11 Total Low-Severity Issues 2 IF-IBC-04, IF-IBC-07 Total Informative-Severity Issues 3 IF-IBC-05, IF-IBC-12, IF-IBC-13 Total 14

Category Breakdown

Finding Type # Specification deviation 6 Protocol/Implementation bug 3 Implementation bug 2 Specification restructuring proposals 1 Code restructuring proposals 2 Total 14

Severity Categories

Severity Description Informational The issue does not pose an immediate risk (it is subjective in nature); they are typically suggestions around best practices or readability Low The issue is objective in nature, but the security risk is relatively small or does not represent security vulnerability Medium The issue is a security vulnerability that may not be directly exploitable or may require certain complex conditions in order to be exploited High The issue is exploitable security vulnerability

Engagement Goals

This audit was scoped by the Informal Systems team in order to assess the correctness and security of the IBC Go implementation. The timing of this internal audit coincides with the upcoming deployment of the IBC protocol to the Cosmos Hub, which marks a critical release in the evolution of the Cosmos Network – the ability for arbitrary blockchains to communicate with one another. The primary focus of the audit was on the upcoming Stargate launch, but we also reviewed the code and specification from the IBC as a development environment perspective for cross-chain applications. Therefore, not all findings present issues with the existing code but might become security vulnerability in the context of IBC applications and new implementations of the IBC specifications. Specifically, during the audit, we sought to answer the following questions: • Is the protocol defined unambiguously? • Are there discrepancies between the code and the specifications? • Are the stated properties and invariants ambiguous? Can we find violations of the properties and invariants? • Are IBC messages correctly validated? • How is error handling and checking state validity done? Are invalid transactions handled correctly? Can malicious inputs cause crashes or invalid states? • Is the code/specification organized in a way that simplifies reviews?

Coverage

Informal Systems manually reviewed the relevant components in the IBC directory of the Cosmos- SDK starting at commit hash 6cbbe0d. Manual review resulted in findings IF-IBC-001 through IF-IBC-012. We also did a preliminary model-based testing of the ICS-20 token transfer app based on the TLA+ specification of the ICS20 that resulted in IF-IBC-13 and IF-IBC-14. This audit focused on implementation and specification of token transfer application (ICS20), channels and packets (ICS04), connections (ICS03), clients (ICS02 and ICS07), and the relayer specification (ICS18), but the relayer implementation was not in the scope. A non-exhaustive list of some approaches taken, and their results include: • Capturing pre and post conditions of the core IBC handlers helped us identify ambiguities and bugs in the IBC specifications that could lead to invalid usage of IBC and insecure IBC implementations (IF-IBC-01) • Carefully reviewing (manually) the code and the specifications led to IF-IBC-06 and IF-IBC- 07. • Understanding execution model and implementation of object capabilities in SDK helped us identify the following issues: IF-IBC-02, IF-IBC-09, IF-IBC-10 and IF-IBC-12. • Analysing handler executions under the worst case scenarios (allowed by the model) confirmed that, besides IF-IBC-08 and IF-IBC-11, which were addressed in the meantime, protocols are safe under the threat model assumed. Note that ensuring protocol liveness heavily depends on the correct relayer implementations, and it was left off the scope of this audit. • Using model based testing (IF-IBC-13), where tests are automatically generated using Apalache model checker from TLA+ specification, surfaced IF-IBC-14, and suggests that it might be useful to expand this exercise further in the future. • Finally, carefully reading specifications in order to understand expected behaviour led to several findings that suggest possible improvements in making properties more clear (IF-IBC- 03), relayer specification more complete (IF-IBC-04) and restructuring of ICS02 in order to simplify onboarding of IBC adopters (IF-IBC-05).

Recommendations

This section aggregates all the recommendations made during the audit. Short-term recommen- dations address the immediate causes of issues. Long-term recommendations pertain to the development process and long-term design goals.

Short term • Separate application-level acknowledgement codes from low level infrastructure aborts (IF-IBC-01). The easiest way to fix this issue would be aligning specification of ICS20 with the code. • Distinguish between valid and invalid counterparty semantics in all function defi- nitions of ICS20 (IF-IBC-02). A user not aware of the Byzantine semantics of recvPacket may not be aware of this, which hinders a proper risk assessment, and development of application-level counter measures. Not taking this into account opens an area of attack that may lead to substantial financial loss. Furthermore, in the discussion be precise about what is meant when referring to actions on the counterparty. E.g., make clear what is meant by “sent” in “IBC packet sent on the corresponding channel end on the counterparty chain”. • Provide more precise properties in ICS04 (IF-IBC-03). Application developer may be lured into the trap of assuming these wrong properties and building their application on top of it, which opens a wide range of exploitable attack scenarios. Also distinguish between properties between two valid chains, and properties a valid chain can expect if the counterparty chain is invalid (Byzantine). • Make explicit all the ordering constraints (IF-IBC-04). The order in which datagrams are submitted is crucial to ensure progress in IBC. An exhaustive representations of these constraints need to be made explicit in the relayer specification (ICS018). Otherwise, it might lead to the incorrect relayer implementations that fail to ensure liveness, or results in transaction fees being spent unnecessarily. Furthermore, the required behavior of the relayer for timeout handling should be specified. • Improve ICS020 specification to prevent token lost issue in the crossing hellos scenario (IF-IBC-06). In onChanOpenTry, the escrow account should be created only if it does not exist, i.e., a check should be added to create an escrow account only if channelEscrowAddresses[channelIdentifier] does not exist.

• Align the type of FungibleTokenPacketData.Amount in ICS020 specification and implementation (IF-IBC-07) • Correct wrong usage of unbonding period in the Tendermint client (IF-IBC-08). Document and specify the misbehavior treatment, and make explicit timing assumptions. Change the code to if currentTimestamp.Sub(consState.Timestamp) >= clientState.TrustingPeriod { instead of if currentTimestamp.Sub(consState.Timestamp) >= clientState.UnbondingPeriod { • Correct handshake liveness issue with crossing hellos in ICS03/ICS04 (IF-IBC-11) Add a mechanism in both the specification, and the implementation to deal with mismatched parameters. • Document in the developer documentation the implicit assumption on error prop- agation up the stack (IF-IBC-12). At the moment, there are only hints regarding this in the form similar to this paragraph in the OnRecvPacket. Such hints do not constitute enough developer guidance to avoid introducing severe bugs, especially for Cosmos SDK newcomers.

Long term • Improve ICS 20 implementation to serve as a template for future IBC applications (IF-IBC-01). As ICS 20 also will serve as a template for future IBC applications, a clearer separation between application-level errors and infrastructure roll-backs (and panics) would be advantageous. For that purpose we suggest a more robust implementation of token transfer that does not rely on the bank module panicking. • Provide test cases that involve corner cases (IF-IBC-04). What complicates the situation with testing relayer is the fact that ordering constraints involve concurrency effects that should be mitigated (serialized) at the relayer. Such issues are typically hard to reproduce or debug. Relying on model-based testing (IF-IBC-13) could be useful in this context. • Major refactoring of ICS02 specification (IF-IBC-05). ICS02 (due to its number) serves as de facto entry point for newcomers who want to learn about IBC. The current structure of the text does not serve that purpose well. We suggest a major reorganization, perhaps along the following ideas in IF-IBC-05.

• Prevent malicious IBC app module to claim any port or channel capability (IF-IBC- 09) Using LookupModuleByPort/ByChannelKeeper methods should be restricted from outside the module - whoever is composing modules, presumably in app.go, should explicitly define which methods of a keeper each module gets. Otherwise, a malicious IBC application module could add the LookupModuleByPort method to its expected PortKeeper interface, and then open channels on some other module’s port. This would allow a malicious IBC module to grab the capability associated with any channel, and send/recv messages on another module’s channel. • Prevent escrow address collisions in ICS20 (IF-IBC-10). In order to mitigate the address collision problems, several recommendations are made: (1) limit the pre-image space, (2) use slow hash function, (3) change the channel establishment protocols and/or (4) redesign the Cosmos address space. • Document non-atomicity assumptions of operations (IF-IBC-12). Either make the SDK functions atomic or introduce a separate explicit step for handlers, say CommitState, that the handler will need to call to write state changes to the store. Otherwise, non-atomicity of operations can lead to bugs. • Use model based testing on critical components, ICS20 and ICS04

Excerpt (19990 of 77248 characters). Read the whole page on informalsystems/audits ↗

← Back to Documentation