Skip to main content

Review Summary: Bitcoin Trace-Net: Formal Contract Verification at Signing Time

Published onOct 22, 2021
Review Summary: Bitcoin Trace-Net: Formal Contract Verification at Signing Time
·

Abstract

Smart contracting protocols promise to regulate the transfer of bitcoins amongst participants in a trustless manner. A safe smart contract implementation should ensure that each participant can always append a contract transaction to the blockchain in order move the contract towards secure completion. To this goal, we propose Bitcoin Trace-Net, a contract verification framework which generates an executable model from the symbolic analysis of the underlying contract implementation. A Trace-Net model consists of a Petri Net formalism enriched with a Dolev-Yao-like actor knowledge model, enabling the verification of smart contract implementations featuring cryptographic sub-protocols. Trace-Net is sufficiently expressive to accurately model blockchain semantics such as the delay between a transaction broadcast and its subsequent confirmation, as well as blockchain reorganizations of finite depths, both of which can break smart contract safety. Implementation level verification also allows Trace-Net to be instantiated at run-time as an effective monitoring framework for secure smart contract protocol executions.

Paper Summaries

“The paper introduces a Trace-Net, a verification framework for Bitcoin contracts. Trace-Net takes as an input a set of Bitcoin transactions that form a contract. It then models all possible execution paths.”


“The problem of the formal analysis of bitcoin smart contracts has been partly solved by Richie Klomp and Andrea Bracciano. This article suggests here another solution based on the recent MINISCRIPT tool as both creator and analyzer of smart contracts. This article considers in detail HTLC and atomic swap contracts. It explains how to create a rooted graph that represents the states of a smart contract. This rooted graph makes it possible to recursively identify the safe states from terminal states (=leaves of the graph) leading to a desired execution of the contract. This theoretical framework for analyzing a smart contract is called Trace-Net because a ‘trace,’ in the article's terminology, represents a possible path connecting the root of the graph to one of its leaves. A contract is safe if there is a trace linking only safe states. Ultimately, Trace-Net could formally guarantee the correct implementation of a smart contract and verify in real time that it is executed correctly.”


“This paper describes a contract verification framework for blockchain-based financial systems. This captures, not only the semantics of the contract, but other factors that affect the correct execution of the contract such as underlying cryptographic protocols, delay between a transaction broadcast and its confirmations, and adversarial reorganization of block chains of bounded depth. The intended application of is real-time analysis of Bitcoin contracts at the point of signing.”


“The paper develops a Petri-Net approach for formally modeling Bitcoin script executions. The goal is to reason about temporal properties and automate the verification process.

More precisely, the paper introduces a model that allows for symbolic execution of bitcoin script transactions and expresses them using a Petri-Net formalism and then explores all possible execution paths.”


“The authors lay out a method to formally verify protocols executed via Bitcoin transactions by generating a ‘reachability graph’ that contains all outcomes allowed by initial conditions. They define models for actor knowledge and capabilities, and include blockchain reorganizations in their analysis.”

Paper Strengths

“The paper addresses an important problem. Since blockchain contracts are intended to be irrevocable, it is very important that they be correct. Moreover, since errors can rise from implementation as well as design, it is important that the implementation be correct as well. The authors show a good command of where problems can arise in blockchain based systems, and address this in their framework. Finally, although the framework is intended for Bitcoin, it appears that it should be extendable to other systems as well.”


“The authors thoroughly describe the model, based on the Petri Net formalism and the Dolev-Yao actor knowledge model. Among other things, Trace-Net accounts for adversarial blockchain reorganizations of a given finite depth, and for confirmation delays. The framework accurately* models Bitcoin's script logic and would indeed be useful for ensuring the desirable properties of Bitcoin contracts.”


“Bitcoin Trace-Net is a promising research project. We can imagine implementing Trace-Net in wallets where MINISCRIPT has been implemented. Then, we'll be able to create watching towers on the Lightning network to monitor the network and ensure that nodes behave correctly. We can also imagine endow Trace-Net with a probability measure so as to run Monte-Carlo simulations and evaluate the execution time of a transaction.”


“The authors lay out a method to formally verify protocols executed via Bitcoin transactions by generating a "reachability graph" that contains all outcomes allowed by initial conditions. They define models for actor knowledge and capabilities, and include blockchain reorganizations in their analysis.”

Paper Critiques and Author Responses

“Bitcoin Trace-Net has apparently not been implemented.”

Author Response: No it has not. This paper focused on formalizing the execution model (Trace-Net). We propose this as future work, together with studies of state-space reduction approaches.


“Bitcoin Trace-Net ignores transaction fees.”

Author Response: The current formulation in the paper says it ignores fees, and that it assumes adjustment prior to broadcast is possible. It would be more precise to write Trace-Net neglects fee adjustment schemes, as fees are simply implied in the output amounts, which Trace-Net does not ignore.

For simplicity we assume fees are adjustable (without resigning) such as the child-pays-for-parent (CPFP) scheme which also do not malleate TXIDs involved in the contract. To address the reviewer’s point, we propose to note this explicitly in Section 3.3. CPFP may be implemented by adding zero-value output “hooks,” which can be included in Trace-Net as is. However, we do not actually model the CPFP mempool logic in Trace-Net, we assume it will succeed (which is a simplification, e.g., low-fee anchoring attacks and mitigation via mempool carve-out logic).


“Due to the lack of formal models of Script, not all Bitcoin protocols with the Trustless Execution property may have that property verified by Trace-Net.”

Author Response: Yes, we also note that another challenge is the potential state-explosion problem of unfolding a Trace-Net model of more complex contracts. We believe model-checking theory provides potential answers to this problem (state-space reduction methods), and will consider this for future work.


“I would be interested to see the model evaluated on more interesting / complex / real-world contracts. Also, swapping bitcoins for bitcoins feels somewhat artificial (this construction is usually employed to exchange different cryptocurrencies, e.g., bitcoins to litecoins, which is understandably outside of the scope).”

Author Response: We have decided to defer the verification of more complex contracts for future work, as this paper focuses on introducing the formalization of Trace-Net. The decision to include atomic swaps (AS) as a running example was made due its simplicity and usage of HTLC scripts which are also used in Lightning. The ability to illustrate an entire Trace-Net figure of an AS was also a motivation for focusing on this “artificial” contract type.

Swapping bitcoins to litecoins would indeed be a more meaningful exchange, but introduces a synchronicity assumption between the chains. Weakening this assumption and modelling potential asynchronicity between chains would be interesting, as it extends Trace-Net verification to cross-chain contracts, but also introduce complexity unrelated to the basic Trace-Net formalism.

“The model does not seem to account for the P2PKH / P2SH / P2WSH types of outputs.”

Author Response: Yes, we have omitted this for simplicity. We assume all scripts/keys committed to the the script schemes above to be known, or else assumed to be un-spendable by the verifying actor. We propose to add a footnote to explicitly state this.


“It is not clear how such a framework would be instantiated, or even if it would be possible to instantiate it… The authors say the framework generates an executable framework from the underlying contract implementation. It’s not clear how such this would be done, or how difficult this would be, even if the source code of the contract were available (which according to this paper, is not the case in Bitcoin).”

Author Response: The goal of the paper is to provide a formalization of our model, to convince the potential reader of the accuracy thereof. To illustrate the instantiation of our model on a specific contract, we provide a running example with an atomic swap contract.

By underlying contract implementation we intend to refer to the underlying Bitcoin transactions. These are necessarily known to actors involved in the contract, as they are passed as messages and ultimately signed and broadcast on the Bitcoin network, observable to all actors.

We agree with the reviewer that inputs/outputs to Trace-Net may be introduced more clearly and propose to clarify that Trace-Net is intended as a verification framework which can be instantiated from Bitcoin transactions alone. To this end we also suggest an amended schematic which clarifies inputs to and outputs from Trace-Net.


“The fact that the contract runs correctly if there is a safe trace in Trace-Net should be a theorem and there should be a proof. The keywords "Theorem" and "Proof" are absent from the article.”

Author Response: We agree and propose to formulate both theorem for Trusted Execution property, and a proof sketch thereof.


“The author devotes a chapter to explain Miniscript, but then says this is not needed for their model.”

Author Response: This is a misunderstanding: At the beginning of Section 3.2 we note that Miniscript provides a useful framework for symbolic execution of ‘a fragment’ Bitcoin Script, but any symbolic execution approach to Script can be used to instantiate Trace-Net. To the best of our knowledge, due to the lack of formalization of Bitcoin Script, symbolic execution is not possible for all of Bitcoin Script (Section 3.1), but future work may achieve this.

Miniscript (MS) enables symbolic execution for a fragment of Bitcoin Script used by common contract types (e.g., HTLCs, lightning). So although MS does not cover all of Script, the fragment it does include is useful to analyze many existing contracting protocols, which is why we dedicate a chapter to introducing it.


“Trace-Net can be analyzed automatically by enumerating all possible execution traces. Clearly, its complexity is overwhelming. No concrete software or benchmark results for this automated analysis are contained.”

Author Response: We agree that the Trace-Net state-space can suffer from the ‘state explosion’ problem arbitrarily complex contracts, which we have left untreated in this paper (mentioned briefly in the conclusion). For this work, we focus on formalizing an execution model for Bitcoin contracts (blockchain & actor knowledge models). We propose to address this point by providing an initial discussion of potential state-space reduction approaches, which reduce the number of states, but retain the properties of interest (e.g., Trustless Execution property). Benchmarking such state-space reduction approaches would be very interesting in this context, but would require introduction of specific contracting protocols under study.


“For this framework to be useful for its intended application, it needs to be able to analyze contracts in real time. But, considering its expressiveness, which covers such things as Dolev-Yao-like models of cryptographic protocols, it is unclear that this would be possible. Even if the framework ensures that the search space would be finite, that does not mean that the problem would be tractable.”

Author Response: We agree that for application, the searchable state-space must be practical and do not address this in this work (as mentioned in the conclusion). State-space explosion is a common problem in model-checking. We propose to expand on a discussion on the necessity of state-space reduction for future work and why it this is important for more complex contract types, which we have not described in this paper (e.g., Lightning, Eltoo, etc).


“There is an example of an atomic swap, but no formal guarantees are shown, such as the predicates that this protocol uses to ensure fairness.”

Author Response: We have provided a definition of the “Trusted Execution” property (Definition 6.1), which is partially illustrated for the atomic swap contract (Figure 5). Trusted Execution implies a notion of fairness, since this property ensures the verifying actor can reach a satisfactory terminal state regardless of the counter-party’s potential strategies.

A formal guarantee would imply presence of an execution trace, executable by the firing actor along safe states, as shown in Figure 5 (sigma d). We propose to amend a simplified figure with this trace explicitly, but find it challenging provide an exhaustive Trace-Net Reachability Graph figure for an atomic swap due to the number of states involved.


“Section 3.1 mentions that only a fragment of Script is suitable for symbolic execution. Why is this the case?”

Author Response: To clarify, the best of our knowledge, only a fragment of Script has been formalized, by Klomp & Bracciali. These operational semantics provide a framework to perform symbolic execution of the limited Script fragment, which does not include time-locks. Miniscript’s “sat” semantics provide rules to derive satisfying input constraints for a given Miniscript expression, and does include time-locks, though it also does not cover the entire Script language.

Additional Comments

“The authors mention a serious vulnerability discovered in Lightning in 2019. Could Trace-Net have discovered it?”

Author Response: [This vulnerability] occurred since the funding transaction output was not “checked/parsed” by Lightning implementations. We believe a verification framework, (e.g., Trace-Net) would have prevented this, as the instantiation of Trace-Net involves the symbolic execution of all transaction output Scripts which are part of the verifying actor’s knowledge. A malicious funding output would result in the generation of a reachability graph with unsafe execution traces.


Comments
0
comment

No comments here