Skip to content

Commit

Permalink
formal-models: extend dBFT with additional post-commit phase
Browse files Browse the repository at this point in the history
Close #111. The additional step is called RMSendAck and allows to send
Ack message once enough Commit messages are received. Block can be
accepted only if BFT number of Ack messages are collected.

Signed-off-by: Anna Shaleva <[email protected]>
  • Loading branch information
AnnaShaleva committed Jun 24, 2024
1 parent 96105d0 commit de50c7b
Show file tree
Hide file tree
Showing 6 changed files with 646 additions and 0 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ This document outlines major changes between releases.
## [Unreleased]

New features:
* TLA+ model for MEV-resistant dBFT extension (#116)

Behaviour changes:
* simplify PublicKey interface (#114)
Expand Down
111 changes: 111 additions & 0 deletions formal-models/.github/dbft_antiMEV.drawio
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
<mxfile host="app.diagrams.net" modified="2024-06-24T11:45:32.984Z" agent="Mozilla/5.0 (X11; Ubuntu; Linux x86_64; rv:126.0) Gecko/20100101 Firefox/126.0" etag="L3zGyTC-LyAz5kXq654f" version="24.5.5" type="google">
<diagram name="Page-1" id="gx1AT7QsytIHyGW8taHa">
<mxGraphModel grid="1" page="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" pageScale="1" pageWidth="850" pageHeight="1100" math="0" shadow="0">
<root>
<mxCell id="0" />
<mxCell id="1" parent="0" />
<mxCell id="zO6A_hVda2gypDU5CBnV-14" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=1;jumpSize=8;orthogonalLoop=1;jettySize=auto;html=1;strokeWidth=2;fontFamily=Comic Sans MS;fontSize=16;fontColor=#404040;startArrow=none;startFill=0;endArrow=classicThin;endFill=1;startSize=4;endSize=4;entryX=0.5;entryY=0;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" target="zO6A_hVda2gypDU5CBnV-6">
<mxGeometry relative="1" as="geometry">
<mxPoint x="471" y="35" as="sourcePoint" />
<mxPoint x="590" y="160" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-15" value="&lt;div style=&quot;font-size: 14px;&quot;&gt;&lt;font style=&quot;font-size: 14px;&quot;&gt;send PReq (primary)&lt;/font&gt;&lt;/div&gt;&lt;div style=&quot;font-size: 14px;&quot;&gt;&lt;font style=&quot;font-size: 14px;&quot;&gt;or&lt;/font&gt;&lt;/div&gt;&lt;div style=&quot;font-size: 14px;&quot;&gt;&lt;font style=&quot;font-size: 14px;&quot;&gt;send PResp (backup)&lt;br&gt;&lt;/font&gt;&lt;/div&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontSize=16;fontFamily=Comic Sans MS;fontColor=#404040;" connectable="0" vertex="1" parent="zO6A_hVda2gypDU5CBnV-14">
<mxGeometry x="0.175" y="3" relative="1" as="geometry">
<mxPoint x="-3" y="23" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-3" value="&lt;font style=&quot;font-size: 16px;&quot; face=&quot;Comic Sans MS&quot;&gt;initialized&lt;/font&gt;" style="strokeWidth=2;html=1;shape=mxgraph.flowchart.terminator;whiteSpace=wrap;fontFamily=Georgia;fontSize=16;strokeColor=#EA6B66;" vertex="1" parent="1">
<mxGeometry x="340" y="10" width="130" height="50" as="geometry" />
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-23" style="edgeStyle=orthogonalEdgeStyle;rounded=1;jumpSize=8;orthogonalLoop=1;jettySize=auto;html=1;entryX=0.5;entryY=0;entryDx=0;entryDy=0;entryPerimeter=0;strokeWidth=2;fontFamily=Comic Sans MS;fontSize=14;fontColor=#404040;startArrow=none;startFill=0;endArrow=classicThin;endFill=1;startSize=4;endSize=4;" edge="1" parent="1" source="zO6A_hVda2gypDU5CBnV-6" target="zO6A_hVda2gypDU5CBnV-7">
<mxGeometry relative="1" as="geometry" />
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-24" value="| PReq &lt;strong style=&quot;font-family: noto_regular; color: rgb(75, 75, 75); font-size: 10pt;&quot;&gt;∪ &lt;/strong&gt;PResp | ≥ M&lt;span style=&quot;font-family: noto_regular; color: rgb(75, 75, 75); font-size: 10pt;&quot;&gt;&lt;/span&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontSize=14;fontFamily=Comic Sans MS;fontColor=#404040;" connectable="0" vertex="1" parent="zO6A_hVda2gypDU5CBnV-23">
<mxGeometry x="-0.24" y="-1" relative="1" as="geometry">
<mxPoint x="4" y="8" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-6" value="prepareSent" style="strokeWidth=2;html=1;shape=mxgraph.flowchart.terminator;whiteSpace=wrap;fontFamily=Georgia;fontSize=16;strokeColor=#EA6B66;" vertex="1" parent="1">
<mxGeometry x="520" y="160" width="130" height="50" as="geometry" />
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-25" style="edgeStyle=orthogonalEdgeStyle;rounded=1;jumpSize=8;orthogonalLoop=1;jettySize=auto;html=1;entryX=0.5;entryY=0;entryDx=0;entryDy=0;entryPerimeter=0;strokeWidth=2;fontFamily=Comic Sans MS;fontSize=14;fontColor=#404040;startArrow=none;startFill=0;endArrow=classicThin;endFill=1;startSize=4;endSize=4;" edge="1" parent="1" source="zO6A_hVda2gypDU5CBnV-7" target="zO6A_hVda2gypDU5CBnV-8">
<mxGeometry relative="1" as="geometry" />
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-26" value="| Commit | ≥ M" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontSize=14;fontFamily=Comic Sans MS;fontColor=#404040;" connectable="0" vertex="1" parent="zO6A_hVda2gypDU5CBnV-25">
<mxGeometry x="-0.1818" y="-2" relative="1" as="geometry">
<mxPoint y="6" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-7" value="commitSent" style="strokeWidth=2;html=1;shape=mxgraph.flowchart.terminator;whiteSpace=wrap;fontFamily=Georgia;fontSize=16;strokeColor=#EA6B66;" vertex="1" parent="1">
<mxGeometry x="520" y="310" width="130" height="50" as="geometry" />
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-8" value="commitAckSent" style="strokeWidth=2;html=1;shape=mxgraph.flowchart.terminator;whiteSpace=wrap;fontFamily=Georgia;fontSize=16;strokeColor=#EA6B66;" vertex="1" parent="1">
<mxGeometry x="520" y="470" width="130" height="50" as="geometry" />
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-11" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=1;orthogonalLoop=1;jettySize=auto;html=1;fontFamily=Comic Sans MS;fontSize=16;entryX=0;entryY=0.5;entryDx=0;entryDy=0;entryPerimeter=0;endSize=4;startSize=4;jumpSize=8;strokeWidth=2;startArrow=classicThin;startFill=1;endArrow=none;endFill=0;" edge="1" parent="1" source="zO6A_hVda2gypDU5CBnV-9" target="zO6A_hVda2gypDU5CBnV-3">
<mxGeometry relative="1" as="geometry">
<mxPoint x="275" y="85" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-12" value="&lt;font style=&quot;font-size: 14px;&quot;&gt;t/o&lt;/font&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontSize=16;fontFamily=Comic Sans MS;fontColor=#404040;" connectable="0" vertex="1" parent="zO6A_hVda2gypDU5CBnV-11">
<mxGeometry x="-0.2125" y="1" relative="1" as="geometry">
<mxPoint as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-16" value="&amp;nbsp;t/o&amp;nbsp; " style="edgeStyle=orthogonalEdgeStyle;rounded=1;jumpSize=8;orthogonalLoop=1;jettySize=auto;html=1;entryX=0;entryY=0.5;entryDx=0;entryDy=0;entryPerimeter=0;strokeWidth=2;fontFamily=Comic Sans MS;fontSize=14;fontColor=#404040;startArrow=classicThin;startFill=1;endArrow=none;endFill=0;startSize=4;endSize=4;" edge="1" parent="1" target="zO6A_hVda2gypDU5CBnV-6">
<mxGeometry relative="1" as="geometry">
<mxPoint x="340" y="185" as="sourcePoint" />
<mxPoint x="470" y="185" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-17" style="edgeStyle=orthogonalEdgeStyle;rounded=1;jumpSize=8;orthogonalLoop=1;jettySize=auto;html=1;entryX=0.5;entryY=0;entryDx=0;entryDy=0;entryPerimeter=0;strokeWidth=2;fontFamily=Comic Sans MS;fontSize=14;fontColor=#404040;startArrow=none;startFill=0;endArrow=classicThin;endFill=1;startSize=4;endSize=4;" edge="1" parent="1" source="zO6A_hVda2gypDU5CBnV-9" target="zO6A_hVda2gypDU5CBnV-6">
<mxGeometry relative="1" as="geometry">
<Array as="points">
<mxPoint x="275" y="240" />
<mxPoint x="480" y="240" />
<mxPoint x="480" y="140" />
<mxPoint x="585" y="140" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-22" value="&amp;nbsp;| Commit | &amp;gt; F&amp;nbsp; " style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontSize=14;fontFamily=Comic Sans MS;fontColor=#404040;" connectable="0" vertex="1" parent="zO6A_hVda2gypDU5CBnV-17">
<mxGeometry x="-0.4" y="1" relative="1" as="geometry">
<mxPoint x="-8" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-27" style="edgeStyle=orthogonalEdgeStyle;rounded=1;jumpSize=8;orthogonalLoop=1;jettySize=auto;html=1;entryX=0.5;entryY=0;entryDx=0;entryDy=0;entryPerimeter=0;strokeWidth=2;fontFamily=Comic Sans MS;fontSize=14;fontColor=#404040;startArrow=none;startFill=0;endArrow=classicThin;endFill=1;startSize=4;endSize=4;" edge="1" parent="1" source="zO6A_hVda2gypDU5CBnV-9" target="zO6A_hVda2gypDU5CBnV-3">
<mxGeometry relative="1" as="geometry">
<Array as="points">
<mxPoint x="160" y="185" />
<mxPoint x="160" y="-20" />
<mxPoint x="405" y="-20" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-28" value="&amp;nbsp;| CV | ≥ M, init at next view&amp;nbsp; " style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontSize=14;fontFamily=Comic Sans MS;fontColor=#404040;" connectable="0" vertex="1" parent="zO6A_hVda2gypDU5CBnV-27">
<mxGeometry x="0.2286" y="-3" relative="1" as="geometry">
<mxPoint x="47" y="-4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="zO6A_hVda2gypDU5CBnV-9" value="cv" style="strokeWidth=2;html=1;shape=mxgraph.flowchart.terminator;whiteSpace=wrap;fontFamily=Georgia;fontSize=16;strokeColor=#EA6B66;" vertex="1" parent="1">
<mxGeometry x="210" y="160" width="130" height="50" as="geometry" />
</mxCell>
<mxCell id="bSvnLd7m7FiDBpnTT2Ld-1" style="edgeStyle=orthogonalEdgeStyle;rounded=1;jumpSize=8;orthogonalLoop=1;jettySize=auto;html=1;entryX=0.5;entryY=0;entryDx=0;entryDy=0;entryPerimeter=0;strokeWidth=2;fontFamily=Comic Sans MS;fontSize=14;fontColor=#404040;startArrow=none;startFill=0;endArrow=classicThin;endFill=1;startSize=4;endSize=4;" edge="1" parent="1">
<mxGeometry relative="1" as="geometry">
<mxPoint x="584.5" y="520" as="sourcePoint" />
<mxPoint x="584.5" y="630" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="bSvnLd7m7FiDBpnTT2Ld-2" value="| Ack | ≥ M" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontSize=14;fontFamily=Comic Sans MS;fontColor=#404040;" connectable="0" vertex="1" parent="bSvnLd7m7FiDBpnTT2Ld-1">
<mxGeometry x="-0.1818" y="-2" relative="1" as="geometry">
<mxPoint x="3" y="6" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="bSvnLd7m7FiDBpnTT2Ld-3" value="blockAccepted" style="strokeWidth=2;html=1;shape=mxgraph.flowchart.terminator;whiteSpace=wrap;fontFamily=Georgia;fontSize=16;strokeColor=#EA6B66;" vertex="1" parent="1">
<mxGeometry x="520" y="630" width="130" height="50" as="geometry" />
</mxCell>
</root>
</mxGraphModel>
</diagram>
</mxfile>
Binary file added formal-models/.github/dbft_antiMEV.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
62 changes: 62 additions & 0 deletions formal-models/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -356,6 +356,68 @@ configuration:
* [TLA⁺ specification](./dbft2.1_centralizedCV/dbftCentralizedCV.tla)
* [TLC Model Checker configuration](./dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch)

## MEV-resistant dBFT models

[Neo X chain](https://docs.banelabs.org/) uses dBFT 2.0 algorithm as a consensus engine. As a part of
the Neo X anti-MEV feature implementation, dBFT 2.0 extension was designed to
provide single-block finality for encrypted transactions (a.k.a. envelope
transactions). Compared to dBFT 2.0, MEV-resistant dBFT algorithm includes an
additional `post-Commit` phase that is required to be passed through by consensus
nodes before every block acceptance. This phase allows consensus nodes to exchange
some additional data related to encrypted transactions and to the final state of
accepting block using a new type of consensus messages. The improved protocol based
on dBFT 2.0 with an additional phase will be referred below as MEV-resistant dBFT.

We've checked MEV-resistant dBFT model with the TLC Model Checker against the same
set of launch configurations that was used to reveal the liveness problems of the
[basic dBFT 2.0 model](#basic-dbft-20-model). MEV-resistant dBFT model brings no extra problems to the
protocol, but it has been proved that this model has exactly the same
[liveness bug](https://github.com/neo-project/neo-modules/issues/792) that the
original dBFT 2.0 model has which is expected.

### Basic MEV-resistant dBFT model

This specification is an extension of the
[basic dBFT 2.0 model](#basic-dbft-20-model). Compared to the base model,
MEV-resistant dBFT specification additionally includes:

1. New message type `CommitAck` aimed to reflect an additional protocol
message that should be sent by resource manager if at least `M` `Commit`
messages were collected by the node (that confirms a.k.a. "PreBlock"
final acceptance).
2. New resource manager state `commitAckSent` aimed to reflect the additional phase
of the protocol needed for consensus nodes to exchange some data that was not
available at the time of the first commit. This RM state represents a consensus
node state when it has sent these additional post-commit data but has not accepted
the final block yet.
3. New specification step `RMSendCommitAck` describing the transition between
`commitSent` and `commitAckSent` phases of the protocol, or, which is the same,
corresponding resource managers states. This step allows the resource manager to
send `CommitAck` message if at least `M` valid `Commit` messages are collected.
4. Adjusted behaviour of `RMAcceptBlock` step: block acceptance is possible iff the
node has sent the `CommitAck` message and there are at least `M` `CommitAck`
messages collected by the node.
5. Adjusted behaviour of "faulty" resource managers: allow malicious nodes to send an
`CommitAck` message via `RMFaultySendCommitAck` step.

It should be noted that, in comparison with the dBFT 2.0 protocol where the node is
being locked in the `commitSent` state until the block acceptance, MEV-resistant dBFT
does not allow to accept the block right after the `commitSent` state. However, it
allows the node to move from `commitSent` phase further to the `commitAckSent` state
and locks the node at this state until the block acceptance. No view change may be
initiated or accepted by a node entered the `commitAckSent` state.

Here's the scheme of transitions between consensus node states for MEV-resistant dBFT
algorithm:

![Basic MEV-resistant dBFT model transitions scheme](./.github/dbft_antiMEV.png)

Here you can find the specification file and the basic MEV-resistant dBFT TLC Model
Checker launch configuration for the four "honest" consensus nodes scenario:

* [TLA⁺ specification](dbft_antiMEV/dbft.tla)
* [TLC Model Checker configuration](dbft_antiMEV/dbft___AllGoodModel.launch)

## How to run/check the TLA⁺ specification

### Prerequirements
Expand Down
Loading

0 comments on commit de50c7b

Please sign in to comment.