informal-report-interlay-audit-2021Q3

Security Audit Report

InterBTC Parachain Modules and Vault Client: Protocol Design and Source Code

2021/09/09 Last revised 2021/09/28

Contents Audit overview 5 The Project . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Scope of this report . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Aims of audit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Conducted work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Timeline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Fee model at protocol level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Vault client . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 On-chain crates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Further Increasing Confidence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

Audit Dashboard 8

Coverage 9 Fee model at protocol level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Vault client . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 On-chain crates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

Recommendations 11 Middle term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Long term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

Specification comments on the economic model 12 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Comments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 The new fee model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Nomination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Issue discussed in collaboration with Interlay . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

Findings 15

IF-INTERLAY2-CMP: Use cmp for clearer case analysis of inequalities 16 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

IF-INTERLAY2-EXPIRATION: Possible disagreement on expiration status from request cancel- lation 17 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

IF-INTERLAY2-FEE: Discrepancies between implementation and spec in fee crate 18 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 fn distribute_rewards . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 fn withdraw_rewards . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

IF-INTERLAY2-ISSUE: Discrepancies between implementation and spec in issue crate 20 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Name of IssueRequest struct . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Discrepancies with spec for request_issue function . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Discrepancies with spec for execute_issue function . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Discrepancies with spec for cancel_issue function . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

IF-INTERLAY2-MINTING: Vault not banned precondition not enforced on minting tokens 24 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

IF-INTERLAY2-NOMINATION: Discrepancies between implementation and spec in nomination crate 25 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Specified Nominator struct is not implemented . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 fn set_nomination_enabled . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 fn opt_in_to_nomination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 fn opt_out_of_nomination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

IF-INTERLAY2-REDEEM: Discrepancies between implementation and spec in redeem crate 28 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 fn request_reedem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 fn liquidation_redeem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 fn execute_redeem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 fn cancel_redeem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 fn mint_tokens_for_reimbursed_redeem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Events . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

IF-INTERLAY2-REFUND: Discrepancies between implementation and spec in refund crate 35 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 fn execute_refund . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

IF-INTERLAY2-REPLACE: Discrepancies between implementation and spec in replace crate 37 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Outdated characterization of the fee model as a optional . . . . . . . . . . . . . . . . . . . . . . . . . 37 fn accept_replace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

IF-INTERLAY2-SPEC: Specification of Concurrent Behaviors 39 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Atomicity of operations: . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

IF-INTERLAY2-STORAGE: Redundant lookups in Substrate storage 42 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

IF-INTERLAY2-VAULT-SPEC: Vault client is undocumented and unspecified 44 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Problem Scenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

Audit overview The Project During our 2021/Q3 InterBTC audit, Interlay engaged Informal Systems to conduct a security audit over the documentation and the current state of the implementation of the new InterBTC fee model, and several crates that were out of scope of the audit in 2021/Q2. InterBTC is a bridge between bitcoin and Polkadot. The link is achieved by BTC-Relay, which, according to its specification, acts a Bitcoin SPV/light client on Polkadot, storing only Bitcoin block headers and allowing users to verify transaction inclusion proofs. Further, it is able to handle forks and follows the chain with the most accumulated Proof-of-Work. An economic fee model is included to align incentives of the actors with correct protocol execution.

Scope of this report • Protocol completeness and compliance between code and specification • Error handling and state validity • Code organization and ease of review The previous audit, in Q2 of 2021, focused on the main parts of the protocol and on auditing the source code of the btc-relay, bitcoin, and vault-registry crates. The current audit focused on the protocol aspects of the fee/sla and nomination protocols, as well as an audit of source code in the following crates:

crate loc vault (client) 4370 issue 1525 redeem 1868 replace 1467 refund 744 fee 733 sla 720 nomination 1088 TOTAL 12515

We conducted an audit, bounded in time to 3 person weeks. The audit was conducted by: • Josef Widder (Principal Scientist) • Shon Feder (Senior Software Engineer) and • Cezara Dragoi (Principal Scientist). This report covers the above tasks that were conducted between July, 12, 2021 and August, 17, 2021 by Informal Systems (the extended duration owing to overlap with vacation season).

Aims of audit • Protocol completeness and compliance between code and specification • Error handling and state validity • Code organization and ease of review

Conducted work Starting July 12, the Informal Systems team conducted an audit of the documentation and the code. For the protocol part, we reviewed the documentation of the fee model. Our team started with reviewing the papers that explain the underlying protocol as well as the documentation written by Interlay. For the code review, Cezara Dragoi focussed on the off-chain software (vault-client) and Shon Feder focused on the onchain parts, that is, the remaining crates from the list above. We set up a shared Github repository, wherein we documented the progress of the audit and collaborated with the Interlay team to record and refine our findings. We also used a shared Discord channel to exchange documents with preliminary findings, which we discussed during online meetings. In this summary document, we have distilled the central findings into uniquely identified findings, and reported specification-related suggestions.

Timeline • 07/12/2021: Start • 08/17/2021: Call to discuss findings of this audit • 08/17/2021: End of audit • 08/18/2021: Start of writing this report as PRs on a private Informal GitHub repo, shared with Interlay • 09/08/2021: Complete draft of report fixed for final review by Interlay Remark. Compared to the last report we had less meetings because many questions could be addressed in the shared Discord channel. Also we shared a Github repository with Interlay so that Interlay could observe our notes and progress throughout the audit. As a result there was no formal submission of intermediate reports.

Conclusions Fee model at protocol level The protocol/specification work in the initial scoping document was to consider the Fee/SLA and Nomination protocols. The Fee/SLA part changed significantly during the audit. In particular, the SLA was removed from the protocol. At this point in the design/development progress, we think that removal of the SLA was a good decision: During the Q2 audit, it was not entirely clear what operations should have what impact on the SLA of an individual agent. Also, the relevant calls into the SLA crate where spread over many protocols, and the intuition behind it was not always clear. The new fee model based on the “stake” (that is, the backed interBTC) is simple and appears robust. The protocol might still be refined with the reintroduction of SLAs at later stages of the project. Overall, we found the documentation of the fee model and the economic incentives very clear. But we provide some suggestions for clarifying the documentation and to make economic implications more explicit.

Vault client In the course of this audit, we also reviewed the off-chain part of the bridge, that is, the vault client. In contrast to the on-chain software, there was no specification for the vault client. Thus part of the audit consisted in reverse-engineering the design. We had a meeting with Interlay to align our understanding. We found one medium- and one high-severity problem, detailed in the findings. These highlight the need for a system-level specification of the functionality, which would be helpful for evaluating the correctness of behavior and a prerequisite for more formal verification of the bridge. We propose a way to approach this in IF-INTERLAY2-SPEC.

On-chain crates Regarding the crates that implement on-chain functionality, we found the code well organized, well documented, and faithful to the specification. In the previous audit we highlighted a number of issues regarding code quality, data representation, and code organization. We observed virtually none of these issues in the artifacts under review in this phase. We attribute this difference in quality to three principle factors:

• The Interlay team’s rewrite of the interbtc specifications to adopt a pre- and post-condition style made the specs much clearer and more accurate. • The parts of the code under review at this phase were more recent additions to the code base. We suspect the improved clarity in the code reflects maturation of the team’s development practices. • The on-chain code in scope for this review was generally less critical and less complex: most of the functionality only involves piping data and performing validation checks. Nonetheless, we identified some divergence between the specification and the implementation. This is not unexpected for a project of this complexity which is still under active development. These discrepancies are detailed in the relevant findings and have all been addressed at the time this report was finalized. We also reported recommendation-level findings on 3 minor matters regarding clarity and condition of the code.

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 • Type: Specification and Implementation • Platform: Rust • Artifacts – interbtc-clients/vault @ 0.8.0 – interbtc/crates/issue @ 0.8.3 – interbtc/crates/redeem @ 0.8.3 – interbtc/crates/replace @ 0.8.3 – interbtc/crates/refund @ 0.8.3 – interbtc/crates/fee @ 0.8.3 – interbtc/crates/sla @ 0.8.3 – interbtc/crates/nomination @0.8.3 – interbtc-spec @ 5.2.1 – interbtc-spec @ 5.4.0 Engagement Summary • Dates: 07/12/2021 - 08/17/2021 • Method: Manual review

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

← Back to Documentation