The case of mixed forks in Emmy+


Note: This analysis was done with the help of Bruno Blanchet (Inria). The interested reader can experiment with our code used in the analysis. As in the previous analysis, we do not present any security proofs.

This is the fourth in a series of posts on Emmy+:

1. After our initial analysis,
2. recently revisited and
3. extended to the partial synchronous network model,
4. we now consider so-called “mixed forks”.

So far, we assumed that malicious bakers wanted to undo a transaction. In this post, we consider instead that they want to maintain a (malicious) fork for as long as possible.

We provide experimental data that such scenarios do not have a significant impact on the previous analysis, which thus remains robust in the presence of this kind of attack.

## Mixed forks

For readability we introduce some notation: we use $$\hb$$, resp. $$\cb$$ to distinguish between honest and corrupt.

We can think of several dishonest bakers $$\cb_i$$ as being a single ‘composite’ dishonest baker $$\cb$$ having as stake fraction the sum of the stake fractions of $$\cb_i$$, and similarly for the honest bakers.

So for simplicity, we reason henceforth using a pair of an honest baker $$\hb$$ and a dishonest baker $$\cb$$ acting as an adversary.

In our previous analyses (as above) we assumed $$\cb$$ wants to undo a transaction, so:

1. $$\cb$$ bakes a secret chain $$\cchain$$ and
2. once $$\cchain$$ is faster than $$\hb$$s chain $$\hchain$$, $$\cb$$ reveals it, and
3. honest $$\hb$$ adopts $$\cchain$$ and bakes on it thenceforth.

Now, suppose $$\cb$$ wants to maintain the system in a forked state1 as long as possible. So:

1. $$\cb$$ still bakes a secret chain $$\cchain$$,
2. $$\cb$$ still reveals it once it is faster than $$\hchain$$, and
3. $$\hb$$ still adopts $$\cchain$$ and bakes on it — but now,
4. $$\cb$$ continues to secretly bake, this time on $$\hchain$$.

The roles of the two chains are thus swapped, and that’s why we talk about mixed forks: the same chain may be $$\hb$$s chain at some point and $$\cb$$s chain at some other point, and this swapping of roles may happen more than once.

We illustrate such a scenario in Figure 1 below, where:

• Blocks (and their timestamps) baked by $$\hb$$ are identified by the “$$^\star$$” superscript.
• Blocks baked by $$\cb$$ are in red.
• The hashed red pattern denotes a block that $$\cb$$ bakes but does not reveal.
• A block index represents the level at which the block is baked.
• The number in each block denotes the block’s priority.

We assume $$\cb$$ has enough stake and chance to have consecutive 0 priorities for the blocks following $$b_1$$, so that $$\cb$$ can bake those blocks sooner than $$\hb$$.

Figure 1 shows that:

1. At level 1, $$\cb$$ starts a fork from $$b^\star_0$$ by baking $$b_1$$; $$\cb$$ cannot reveal $$b_1$$ because $$b_1$$ has a larger timestamp than $$b^\star_1$$ baked by $$\hb$$.

2. At level 2, $$\cb$$ double-bakes (bakes on its own secret chain and on the chain of $$\hb$$) and reveals $$b_2$$, the block baked on its own secret chain before $$\hb$$ bakes at this level (the block $$b^\star_2$$ which $$\hb$$ would have baked had it not been $$b_2$$ is in gray, drawn with dashed lines).

3. At level 3, $$\cb$$ bakes $$b_3$$ on top of $$b'_2$$ while $$\hb$$ bakes $$b^\star_3$$ on top of $$b_2$$; $$\hb$$ does so because $$\hb$$ swapped chains once $$\cb$$ revealed $$b_2$$: at that point, $$\cb$$s alternative chain $$b_0^\star b_1b_2$$ is longer than $$\hb$$s chain $$b_0^\star b_1^\star$$.

4. At level 4, $$\cb$$ bakes $$b_4$$ on top of $$b_3$$ and reveals it before $$\hb$$ bakes at this level (note that we are in a similar situation as that at level 2).

5. At level 5, $$\hb$$ bakes $$b^\star_5$$ on top of $$b_4$$: once $$\cb$$ revealed $$b_4$$, $$\hb$$ swapped again chains because the alternative chain is longer than the one on which $$\hb$$ was baking. This is the same reasoning as at level 3. Note that $$\hb$$ bakes $$b^\star_5$$ on the chain $$\hb$$ initially started baking on.

$$\cb$$ could in theory continue baking on both chains and force $$\hb$$ to swap chains repeatedly, assuming $$\cb$$ receives priorities and endorsement slots to allow it. We would thus like to quantify to what extent can $$\cb$$ do that: how often and for how long.

### Probabilities of mixed forks

To experimentally show that the probability that $$\cb$$ can maintain a fork decreases (sufficiently rapidly) as fork length increases, we revisit the scenario “forks starting now”. We consider the following question:

How long can $$\cb$$ maintain the system in a forked state?

To answer this, we use an approach similar to the one for computing the probabilities of forks in the non-mixed forks case. We presented the methodology behind the analysis in a previous post. However, the key aspects needing careful consideration are:

• how to identify when a swap is feasible and advantageous for $$\cb$$, and
• how the update the time difference between chains at the moment of a swap.

Using our updated analysis, we plot the probabilities of mixed forks and compare them with the probabilities of non-mixed forks as already computed in the previous analysis). In this experiment we assumed that the network is synchronous.2

The plot suggests that, for decent attacker stake fractions such as .2, or even .3, the expected number of confirmations in the mixed case is only a bit larger than in the non-mixed case. For instance, for .3 attacker stake fraction, one needs to wait a priori for 20 confirmations instead of 16. The expected number of confirmations gets larger for higher attacker stakes: for .4, the expected number of confirmations is 85, vs. 67 for the non-mixed case.

To conclude, our experiments show that, even if $$\cb$$ tries to repeatedly make $$\hb$$ swap chains, $$\cb$$ cannot do this for too long: the number of expected confirmations when considering “mixed forks” is only slightly higher than without them.

1. This post considers specifically the case that $$\cb$$ tries to maintain one fork. Of course we could generalise this to multiple forks, but our simulations on a simplified model suggest that one fork is already a good approximation to the more general case.

2. We recall that $$\Delta = 30$$ represents the case when the network is synchronous

Regular Scheduling For Our Tezos Proposals

The teams at Nomadic Labs, Metastate, Marigold, and DaiLambda have participated in a number of joint protocol proposals for Tezos; some of us have been working on the code since the original launch of the Tezos network, and have been involved with updates from Athens through the recent Delphi proposal. Over time, we have gained more and more experience and have learned what practices seem to work best for updates to the...

It’s been a while since we published a post in our meanwhile series, and as always we’ve been working hard behind the scenes to improve the Tezos ecosystem. August marked a milestone: we launched Dalphanet, a dedicated test network designed to examine features from all developers involved in submitting the more extensive and long-awaited protocol proposal, including Sapling, a new protocol environment, among other improvements. For more information on Dalphanet see: Agora Forum Reddit On...

Dexter: Decentralized exchange for Tezos, formal verification work by Nomadic Labs

The Dexter smart contract is the cornerstone of the Dexter. We outline a formal verification of its functional specification, in Coq.

On September 30th, camlCase released Dexter. Dexter is a smart contract empowering decentralized exchange, performing the same function for tez as Uniswap on Ethereum does for ether; it enables trade between tez and any other token implemented by an FA1.2 contract. To this day, the following efforts have been undertaken to ensure Dexter’s quality, including: a security audit by Trail of Bits, Read More

Emmy+ in the partial synchrony model


On “Defending Against Malicious Reorgs in Tezos Proof-of-Stake”

Note: We would like to acknowledge Bruno Blanchet (Inria) for his feedback. The interested reader can experiment with our code used in the analysis. We are happy to note a new paper on Emmy+: “Defending Against Malicious Reorgs in Tezos Proof-of-Stake” by Michael Neuder, Daniel J. Moroz, Rithvik Rao, and David C. Parkes in the ACM Advances in Financial Technologies 2020 conference. We are delighted that Tezos and Emmy+ are stimulating independent research activity, and we hope to see much...

Delphi: official release

Delphi This is a joint post from Nomadic Labs, Metastate and Gabriel Alfour. We’re happy to announce that we have compiled a Tezos protocol proposal we’re dubbing “Delphi”, with hash PsDELPH1Kxsxt8f9eWbxQeRxkjfbxoqM52jvs5Y5fBxWWh4ifpo. Delphi contains a number of small bug fixes, but, more importantly, it makes substantial improvements to the performance of the Michelson interpreter and to the gas model, and thus dramatically improves gas costs. In addition, it reduces storage costs by a factor of 4 to reflect...

Delphi: changelog

007 Delphi Changelog Getting the source code of the proposal The source code of this proposal is available in this tar archive: https://blog.nomadic-labs.com/files/delphi_007_PsDELPH1.tar. To compute the hash, you can use the tezos-protocol-compiler as follows. The result should be PsDELPH1Kxsxt8f9eWbxQeRxkjfbxoqM52jvs5Y5fBxWWh4ifpo. mkdir proposal && cd proposal curl https://blog.nomadic-labs.com/files/delphi_007_PsDELPH1.tar | tar -x tezos-protocol-compiler -hash-only delphi_007_PsDELPH1 If you want to directly investigate how Delphi differs from the current protocol, you can use diff against folder proto_006_PsCARTHA of the mainnet source code....

Measuring test coverage

An in-depth look on how we measure test coverage of the OCaml implementation of Tezos.

As we have discussed earlier on this blog, notably in the post on regression testing, testing is an important complement to formal verification. A critical task when testing is to ensure a high degree on test coverage. In this post we discuss how we measure test coverage of the OCaml implementation of tezos using bisect_ppx, and our work towards ensuring that the Michelson interpreter of the node is fully covered by tests. Test coverage Testing is simpler to set up than formal verification but...