Summa Proofs Are Not Composable
A concrete attack against Summa
NIPoPoWs and cross-chain transfers
It is sometimes useful to prove to a blockchain, say Ethereum, that an event took place within another blockchain, say Bitcoin. This concept of cross-chain information transfer has incredibly useful applications, including one-way and two-way pegging of coins, sidechains, and atomic swaps. One of the most interesting applications is the decoupling of a cryptocurrency from its respective blockchain. If these transfers are possible bidirectionally, it is completely possible to own Bitcoin Cash currency within the Ethereum blockchain; or ether within the Cardano blockchain. It’s also possible to move your ether back and forth between the Ethereum blockchain and the Ethereum Classic blockchain, all while never touching the ether classic currency or exchanging between currencies. These concepts are explored in our paper, Proof-of-Work Sidechains, which appeared in this year’s Financial Crypto workshop on Trusted Smart Contracts.
The core building block to create these constructions is the cross-chain transfer of information, the idea to use an Ethereum smart contract to verify that something took place in the Bitcoin blockchain. Such cross-chain proofs are called Non-Interactive Proofs of Proof-of-Work (NIPoPoWs). They’re a short string which can be produced by inspecting the Bitcoin blockchain and can later be fed to an Ethereum smart contract, which can subsequently validate the NIPoPoW locally as a direct computation, without network access to the Bitcoin blockchain itself. We introduced how to construct NIPoPoWs and proved that they are secure in our paper, Non-Interactive Proofs of Proof-of-Work.
Our NIPoPoW construction is a particular type of NIPoPoW we call a superblock NIPoPoW. In a superblock NIPoPoW, we collect a sequence of representative blocks that have achieved a higher difficulty than necessary, which we call superblocks. I know these are a lot of terms to swallow, so if you want a more digestable overview of the scheme, we presented it in our recent paper, Compact Storage of Superblocks for NIPoPoW Applications, which was published in the MARBLE conference this year. For an even more accessible approach, we have created the NIPoPoWs website which has helpful videos describing the scheme in an attempt to popularize our work and does not require a background in cryptography.
Another NIPoPoW construction in addition to ours is the FlyClient NIPoPoW, a protocol developed by Benedikt Bünz of Stanford University et al. Similarly to our construction, they create these cross-chain proofs by including several sample blocks representing the proof-of-work that took place in the source blockchain.
In short, it seems to some degree necessary to present a sequence of blocks in order to securely illustrate that an event took place in a blockchain.
The value of proofs
In the NIPoPoWs paper, we use a cryptographic approach to show that our construction is secure. We state and prove a mathematical security theorem which shows that no polynomial-time adversary can attack the scheme, except with negligible probability, unless Bitcoin itself is broken. We clearly articulate the desirable properties of our scheme, which are falsifiable (but not false). This proof style, showing that any polynomial-time adversary will fail, is the core technique used in all of the field of cryptography. It is a very powerful technique, because it illustrates that there is no adversary in our model which can attack our scheme. Contrary to techniques in which the authors think of particular adversaries and show that their scheme is secure against all the adversaries they can think of, this cryptographic technique rules out even adversaries that we cannot even conceive of, because it uses a for all quantifier and proves a statement about an arbitrary adversary. For an introduction to the cryptographic technique, consult the book Introduction to Modern Cryptography, which you can directly (and ethically) pirate from here. The FlyClient paper also follows the cryptographic model.
This style of security proof is a difficult endeavour that can take a significant amount of time, requires technicality, and needs to be rewritten many times to get right. However, science is not easy, and this is the barrier we have to overcome if we want to claim to understand the security of our protocols.
The Summa protocol
Last year, Summa introduced a different way of creating cross-chain proofs. Their scheme is described in their blogpost, in which they also claim to have better gas performance than our construction. In their scheme, instead of presenting a carefully crafted sample of blocks from the blockchain from genesis till the tip, they only present a few recent blocks (k blocks in the language of the Bitcoin Backbone) burying the transaction of interest. Before you read further, I recommend that you go read their blog post describing their scheme — both for fairness and to acquire a better understanding of what it is we’re going to attack here.
First, I must say that I do like their scheme. It is a cryptoeconomic scheme, which differs in its model and assumptions from our work. Contrary to our approach, in which we prove security against any adversary, the scheme of James Prestwich of Summa creates a construction which is designed to only be resilient against a particular type of adversary: a rational adversary. A rational adversary is an adversary acting selfishly, i.e., not willing to lose money to attack the scheme. I think the rational approach is a reasonable approach here. It falls within the field of game theory rather than cryptography and uses different styles of proof techniques. I’m happy to see constructions that are rational rather than cryptographic. Rational schemes are, in a sense, better reflecting reality, because in practice people will not generally play irrationally. Additionally, a rational approach could allow many important assumptions to be weakened (therefore, making the theorems stronger) such as the honest majority assumption prevalent in blockchain protocols.
Another aspect of Summa that I like is that they have developed some very useful Solidity smart contracts for verification of Bitcoin-sourced cross-chain transfers, which they graciously open sourced under LGPL and have been very useful to us. The fact that they have a working implementation and have run their protocol in practice is quite nice and useful.
Unfortunately, Summa do not make an attempt to prove their construction is secure. While a lack of security proof is not uncommon in the era of blockchains, this creates a dangerous precedent. Anyone can create a scheme which they, themselves, cannot break; the question is whether they can create a scheme which they can convincingly illustrate to their colleagues, rather than to themselves, is secure. When I say convincingly, I mean using the standard notation and established practices of the field, including rigorous mathematical proofs. The practice of writing proofs allows one to find mistakes in their construction –I have found serious security mistakes in my own constructions numerous times– refine their model, and clearly articulate their assumptions. Some constructions may even seem to be obviously or trivially secure, and perhaps the Summa authors believe their scheme falls within this category. It is especially those that should be proven secure, first because “trivially secure” is an easy trap to fall into and create an insecure scheme; secondly, because if it really were trivially secure, it should be easy to prove secure — right?
Before we get into the attack against Summa, let me restate their game theoretic argument about why their system is secure.
In his blogpost, James Prestwich argues that it is sufficient to provide only k blocks on top of the transaction of interest as a proof of cross-chain transfer. The string that is given to the receiving smart contract is then, literally, the block headers of k blocks burrying the transaction of interest. The smart contract then verifies the proof-of-work within these k blocks (where k is a constant hard-coded into the smart contract code) and accepts the transaction as valid and confirmed if it is proven to be included in the first block in the sequence by a Merkle inclusion proof. The idea is that, if a transaction is not really part of the blockchain, it will be computationally, and therefore economically, expensive to mount such an attack. They attempt to actually quantify the cost of such an attack: Because those k blocks will be wasted and their proceeds will not be delivered to their miner, the cost of production is k c, where c is the amount of coin mined per block. They suggest setting k = 6, which, in current prices, according to their calculations, amounts to a mining cost of €65,000. This parameter is configurable.
“In other words, validation gives us $X of confidence in the proof, and we can require X be as high as we want.”
The critical idea in their construction is that, if a value of less than €65,000 is transferred in a cross-chain transaction, then a cross-chain proof with k = 6 and a mining cost of more than €65,000 is sufficient to secure the cross-chain transfer.
As seen in the above picture, an honest prover doesn’t have to perform any extra mining: They can get a correct cross-chain proof for free (blue dashed line). On the other hand, an adversarial prover needs to perform work in order to create a fake proof (blocks within the red dashed line). That work is costly, and if the cost is more than their proceeds obtained by stealing from the protocol, a rational adversary will not bother to perform the attack. Note that the blocks that the adversary mines in this attack never become members of the longest chain, and therefore the adversarial miner will lose the block rewards obtained by their mining.
Let’s look at what a cross-chain double spending attack would amount to in this example. What an adversary is interested in doing is to create a transaction, tx₂, within the source blockchain, which sends the money to the destination blockchain. However, they want tx₂ to never become confirmed within the honestly maintained longest source blockchain, but only to be included in a secret block and never seen by the source blockchain miners. Then, the adversary hopes that they can falsely convince the smart contract running on the destination blockchain that tx₂ really did get confirmed in the source blockchain, granting the adversary permission to spend the funds within the destination blockchain. This allows the adversary to both keep the money in the source blockchain (as the source miners never saw it moving away) as well as recover the money in the destination chain (as the smart contract verified that they have permission to do so) in a cross-chain double spend. However, because it is costly to mine all these rogue blocks in order to create the fake chain that convinces the destination blockchain smart contract, the adversary does not have incentive to do so unless tx₂ contains a lot of money — more money than they need to spend to mine for the alternative chain at the bottom.
A composability attack against Summa
I would like to use this opportunity to describe an attack I have discovered against the Summa scheme in order to illustrate the necessity for a security proof. I want to highlight here that the attack itself is unimportant, and fixing the particular attack or responding to this particular attack is not a sufficient response. The point I am trying to raise pertains to the necessity of security proofs. I invite the Summa authors to write a security proof for their scheme. During that process, they will be able to articulate their precise assumptions and model, which are not clear from the blogpost. Perhaps my attack falls outside of their assumptions or model, and that’s completely fine, but we cannot know this until they have articulated them, together with their goals, in precise mathematical language.
Let’s look at the incentive argument of the previous section again. It seems sound at first, until one starts thinking about composability (composability, by the way, is a central topic of cryptography). The critical point is that makes the implicit closed system assumption: that they operate a closed system in which all incentives are accounted for in their own transactions. However, imagine what can happen if there are multiple applications, similar to Summa, each acting independently of one another. For simplicity in this argument, imagine that there are two cross-chain transfer protocols, one operated by Summa, the other operated by an independent entity, Ammus. The two protocol operators are not aware of one another. What happens then?
On the one hand, imagine Summa creates a transaction tx₁ which has a value of €60,000 it attempts to move across blockchains and is included in source blockchain block B. Unbeknownst to Summa, Ammus creates a transaction tx₂ which also has a value of €60,000 it attempts to move across blockchains and is included in the same source blockchain block B. Summa now makes the argument that k = 6 blocks is sufficient to protect their investment, because an adversary would have to expend €65,000 to mine a chain competing with the main chain. At the same time, Ammus, not aware of Summa’s existence, makes the same economic argument about their own transfer and also uses k = 6.
But what happens if an adversary is mighty and powerful enough to be aware of both Summa and Ammus? The adversary creates an adversarial block B’ confirming two adversarial transactions tx₁’ and tx₂’ each of value €60,000 pertaining to the Summa and Ammus protocols respectively. The transactions are kept secret and are mined by the adversary into a block B’. The adversary then spends €65,000 to mine k = 6 blocks on top of B’. None of these blocks are published on the main chain, so the money never really leaves the chain. However, the adversary can readily produce a Summa-style proof for both protocols which validates correctly, therefore granting her an incoming transfer into the destination blockchain. The cost for mining this secret chain is just €65,000, but the proceeds can be €60,000 + €60,000 = €120,000. Note that this is extra money created on the destination chain which was never paid on the source chain — a cross-chain double spend. A rational adversary would happily perform this attack and present both protocols with perfectly valid proofs. Each protocol designer, upon becoming attacked, is then independently baffled by why the adversary were so irrational as to lose €5,000 to perform that attack against them! What has gone wrong is that the designer is myopic and only considers their own protocol in the big picture of a multitude of protocols which were never designed to be composable.
The fact that the attacker may have lower computational power than the rest of the network, say 10%, means that the adversary can only produce these adversarial chains at a rate which is 90% slower than the rest of the network, but no matter – the attack will still succeed, as the blocks will be accepted as valid proof-of-work by the stateless verifier, who cannot connect to the source network.
Worse yet, in real blockchain systems, there are numerous games taking place simultanously, all with economic incentives at play. For example, if the Ethereum blockchain is used as a source, there can be casino-style bets at play, with money at stake, which may incentivize an adversary to fork the blockchain. While the designer of each betting system may myopically argue that their proceeds are insufficient to incentivize the mining of a long fork, multiple bets, together with a construction like Summa, can compound to create sufficient incentives in the large picture. Professor Yannis Smaragdakis from our school at the University of Athens hits the nail on the head in his blogpost:
“Unfortunately, a single contract cannot know what other bets are taken by other contracts’ transactions in a single block, and an attacker could well be targeting multiple contracts to compound bets.”
There can be other incentives to create forking blockchains as well. A miner could be externally bribed to create a fork, and these bribes may compound with Summa’s incentives to create yet more reason to fork.
Summarizing, the security analysis of the Summa protocol is insufficient and the protocol is attackable. While this particular attack may be fixable or may not fall within the attacks the designers of the protocol are interested in, it highlights the fact that protocol designers must prove their protocols secure if they want to build confidence beyond gut feeling. Such proofs allow their peers to assess the model and assumptions in which their protocol functions and to see if they are appropriate for their applications. While the Summa designers might have been well aware of the attack I am highlighting and they might have been careful to look for the potential composability conflicts I have described, I am worried about software developers who will copy Summa’s protocol and take for granted that it is secure because it was intuitively argued so, without articulating the model in which it is applicable. A security proof would surface these points and make them explicit so that any reader would understand whether the protocol is applicable in their situation. In this particular case, the closed system assumption would be absolutely essential in writing down a complete game theoretic theorem and proof of security, making it clear that the system does not compose well.
