informal-report-interlay-audit-2021Q2

Security Audit Report

InterBTC Parachain: Protocol Design and Source Code

2021/06/12 Last revised 2021/09/17

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

Audit Dashboard 7

Engagement Goals 8 Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Aims of audit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

Coverage 9

Recommendations 10 Short term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 Long term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

Minor comments 11 Fee / SLA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Vault nomination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Vault-registry . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Documentation improvements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Document the reference implementation and specs in the README of the bitcoin crate . . . . . . 11 Fix Broken links . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Code quality improvements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Avoid use of magic numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Avoid redundant and scattered computations and validations . . . . . . . . . . . . . . . . . . . . . . 12 Discrepancies with specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 bitcoin crate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 btc-relay crate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 vault-registry crate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

Findings 18

IF-INTERLAY-ADTS: Under-utilization of algebraic data types leads to confusing and error prone code 19 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

IF-INTERLAY-INTERACTION: Interaction between the issue and refund protocols 22 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

IF-INTERLAY-LIQUIDATION: Liquidation event incentives unclear 24 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Thresholds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Realistic scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Incentives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Reconsider Liquidation as Liveness concern . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

IF-INTERLAY-NAMING: Documentation and variable naming of check_and_do_reorg function is misleading 26 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

IF-INTERLAY-NO-BLOCK: Scenario of “no block being recently submitted” (all relayers offline) not handled gracefully 28 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

IF-INTERLAY-PARSING: raw_block_header parsing occurs at multiple locations, but should be moved to the edge of the program 29 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

IF-INTERLAY-SPEC: Specification of Concurrent Behaviors 30 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Protocol Level - System goals (as discussed in the paper) . . . . . . . . . . . . . . . . . . . . . . . . 30 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Global invariants between BTC and InterBTC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

IF-INTERLAY-STORAGE: Storage updates of Vault struct and cached values are not co-located 32 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

IF-INTERLAY-SUBJECTIVE: “Subjective initialization” condition assuming block_height is the correct height for the raw_block_header in relay initialization not specified 34 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

IF-INTERLAY-THEFT: Theft by redeeming (replacing) too much 35 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Collaborative discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

IF-INTERLAY-TIMEOUT: Timeouts (and races) on sender chain 37 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Clarify use cases around timeouts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Time parameters in the paper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

IF-INTERLAY-WITNESS: Missing check for illegal encoded witness in transaction parsing 39 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

Audit overview The Project In April 2021, Web3 and Interlay engaged Informal Systems to conduct a security audit over the documentation and the current state of the implementation of interBTC : a trustless bridge from Bitcoin to Polkadot formerly known as PolkaBTC. The bridge protocol is based on XCLAIM. XCLAIM is designed to support issuing, transferring, and redeeming Cryptocurrency Backed Assets (CbAs). XCLAIM is intentionally generic in order to support a wide range of assets but requires that one side of the bridge allows to execute smart contracts (Polkadot) while the other side just needs to provide a history of transaction in the backing currency (bitcoin).

Scope of this report The agreed-upon workplan consisted of the following tasks: • Task 1. Deep dive of the XCLAIM protocol and its sub-protocols – on tag 3.1.0 • Task 2. Crates to audit (parachain only) – bitcoin: on commit e4cb057. – btc-relay: on commit e4cb057. – vault-registry: on tag 0.7.4 This report covers Task 1 and Task 2 that were conducted May 10 through June 7, 2021 by Informal Systems under the lead of Josef Widder, with the support of Shon Feder.

Conducted work Starting May 10, the Informal Systems team conducted an audit of the existing documentation and the code. Interlay gave us a one-hour presentation with an overview over the protocol with focus on the scope of this audit. For the protocol deep dive, the team also reviewed the xclaim paper. Our team started with reviewing the paper to get an overview of the protocol design principles, and the “Security Analysis” parts of the protocol specs v3.1.0 in order to get an overview over the specifics of XCLAIM(BTC,DOT). We then continued with the specific subprotocols (redeem, replace, issue, refund, etc.) within the protocol specs v3.1.0 with special focus on correctness of concurrent execution of these protocols. For the code review, Interlay gave as two one-hour code walk-throughs to help us getting started. We then started the code audit with the bitcoin and the btc-relay crates, and held back with the vault-registry crate for a week as Interlay updated the code when we started the audit. We audited vault-registry in the last week of the audit period. Over the shared Discord channel we shared documents with preliminary findings, which we discussed during online meetings. In this document, we distilled the central findings into numbered findings, and the less central issues into a section called “minor comments”.

Timeline • 05/10/2021: Start • 05/10/2021: Interlay presentation (1 hour) • 05/11/2021: code walkthrough (1 hour) • 05/12/2021: code walkthrough (1 hour) • 05/19/2021: submitted first intermediate report on the protocol deep dive • 05/21/2021: meeting Informal/Interlay with discussion of first report • 05/26/2021: submitted first intermediate report on code audit (‘bitcoin’, ‘btc-relay’)

• 05/26/2021: meeting Informal/Interlay with discussion of code report • 05/28/2021: submitted second intermediate report on the protocol deep dive • 05/28/2021: meeting Informal/Interlay with discussion of second protocol report + code report • 06/02/2021: submitted third intermediate report on the protocol deep dive • 06/07/2021: submitted second intermediate report on code audit (‘vault-registry’) • 06/07/2021: meeting Informal/Interlay with discussion of intermediate reports • 06/07/2021: End of audit • 06/16/2021: submission of first draft of this report

Conclusions We found that the XCLAIM(BTC,DOT) design and security model in general is well thought out and addresses the challenges in bridge design, given the limitation that smart contracts can only be run on one side of the bridge. Despite the general high quality in the protocol design, we found some details that need to be addressed. We highlighted potential security issues in IF-INTERLAY-THEFT that are the result of the code of several protocols differing from the specification, and in IF-INTERLAY-NO-BLOCK where on-chain safety is based on an off-chain liveness assumption (existence of a correct and timely relayer). We highlighted two issues that are related to making more explicit incentives and rational behavior, namely, IF-INTERLAY-LIQUIDATION and IF-INTERLAY-TIMEOUT . This should help users of the bridge to understand the inherent risk they are taking and what are the beneficial actions in dynamic scenarios (exchange rate fluctuations, being close to timeout expiration). Finally, we gave some recommendations in IF-INTERLAY-SPEC to clarify the high-level temporal properties and invariants maintained by the protocol. Overall we found the code well organized, well documented, and faithful to the specification. Despite the general high quality of the implementation work, we found seven issues regarding code quality, data representation, code organization, and divergence from the specification. These are detailed in the relevant findings. We also found a number of minor imperfections, which we note in the minor comments. With one exception, all the findings we identified during the audit have been resolved at the time this report was last updates. The sole exception is IF-INTERLAY-SPEC, which sets out recommendations towards a more exhaustive and formalized specification.

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 enables discovery of issues that are unlikely to be identified through manual review. It is our understanding that the Interlay team intends to pursue such measures to further improve the confidence in their system.

Audit Dashboard Target Summary • Name: Selected Crates in the InterBTC Parachain • Code Version: – bitcoin: on commit e4cb057. – btc-relay: on commit e4cb057. – vault-registry: on tag 0.7.4 • Specification Version: tag 3.1.0 • Type: Specification and Implementation • Platform: Rust, using the Substrate framework Engagement Summary • Dates: 5/10/2021 to 6/15/2021 • Method: Manual review • Employees Engaged: 2 • Time Spent: 3 person-weeks

Engagement Goals Scope • Deep dive of the XCLAIM protocol and its sub-protocols – on tag 3.1.0 • Crates to audit (parachain only) – bitcoin: on commit e4cb057. – btc-relay: on commit e4cb057. – vault-registry: on tag 0.7.4

Aims of audit (From the scoping doc)

Process/specification :: are there any flaws in the specification of the different protocols?
Implementation/specification mismatches :: are there discrepancies between the specification of the InterBTC protocols and their implementation?
Bitcoin implementation issues :: are there any issues in terms of Bitcoin compatibility (e.g. parsing, fork handling etc.)?
Implementation issues :: are there issues in the implementation that may introduce failures?
Testing issues :: are there cases/states of the parachain or clients not covered as part of the tests?

Coverage Informal Systems manually reviewed, the xclaim paper, the protocol specs v3.1.0 the code of the crate bitcoin on commit e4cb057, of the crate btc-relay on commit e4cb057, and the crate vault-registry on tag 0.7.4. Manual review resulted in the folowing findings: • Reviewing the paper lead to finding unclear incentives IF-INTERLAY-LIQUIDATION, and unclear high-level properties and invariants as noted in IF-INTERLAY-SPEC. • Reviewing the code and the specification we identified potential attacks in IF-INTERLAY-THEFT, IF- INTERLAY-NO-BLOCK as well as potential races in IF-INTERLAY-TIMEOUT. • Reviewing the specification we found that the interaction between issue and refund are somewhat unclear, as reported in IF-INTERLAY-INTERACTION. • Comparing specifications against the implementation, and reviewing the source code in detail yielded the various findings in IF-INTERLAY-ADTS, IF-INTERLAY-SUBJECTIVE, IF-INTERLAY-PARSING, IF- INTERLAY-NAMING, IF-INTERLAY-STORAGE, and IF-INTERLAY-WITNESS. Details of each are to be found in the relevant sections. • From these activities, we also collected an extensive list of extensive minor comments. These remarks do not address major security or code quality risks, but aim to indicate minor defects or suggest helpful improvements.

Recommendations This section summarizes key

Excerpt (19988 of 76090 characters). Read the whole page on informalsystems/audits ↗

← Back to Documentation