formal-models: extend dBFT with additional post-commit phase

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]>
nspcc-dev · Jun 21, 2024 · 5124528 · 5124528
1 parent 96105d0
commit 5124528
Show file tree

Hide file tree

Showing 6 changed files with 644 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -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)

diff --git a/formal-models/.github/dbft_antiMEV.drawio b/formal-models/.github/dbft_antiMEV.drawio
@@ -0,0 +1,111 @@
+<mxfile host="app.diagrams.net" modified="2024-06-20T11:50:15.322Z" agent="Mozilla/5.0 (X11; Ubuntu; Linux x86_64; rv:126.0) Gecko/20100101 Firefox/126.0" etag="7q_jvA6ZN1I2lI1y4_W7" 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="ackSent" 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>
diff --git a/formal-models/.github/dbft_antiMEV.png b/formal-models/.github/dbft_antiMEV.png
diff --git a/formal-models/README.md b/formal-models/README.md
@@ -356,6 +356,66 @@ 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 `Ack` aimed to reflect the additional `Acknowledgement` protocol
+   message that should be sent by resource manager if at least `M` `Commit`
+   messages were collected by the node.
+2. New resource manager state `ackSent` aimed to reflect the `post-Commit` phase of
+   the protocol, i.e. a consensus node state when it has sent the `Acknowledgement`
+   message but has not accepted the block yet.
+3. New specification step `RMSendAck` describing the transition between `Commit` and
+   `post-Commit` phases of the protocol, or, which is the same, the transition from
+   `commitSent` to `ackSent` resource managers state. This step allows the resource
+   manager to send `Ack` 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 `Acknowledgement` message and there are at least `M` `Ack`
+   messages collected by the node.
+5. Adjusted behaviour of "faulty" resource managers: allow malicious nodes to send an
+   `Ack` message via `RMFaultySendAck` step.
+
+It should be noted that, in comparison with the dBFT 2.0 protocol where the node is
+being locked in the `Commit` phase until the block acceptance, MEV-resistant dBFT
+does not allow to accept the block right after the `Commit` phase. However, it allows
+the node to move from `Commit` phase further to the `post-Commit` phase and locks
+the node at this state until the block acceptance. No view change may be initiated or
+accepted by a node entered the `post-Commit` phase.
+
+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