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 20, 2024 · 0095b94 · 0095b94
1 parent 6abc124
commit 0095b94
Show file tree

Hide file tree

Showing 5 changed files with 643 additions and 0 deletions.
diff --git a/formal-models/.github/dbft3.0.drawio b/formal-models/.github/dbft3.0.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/dbft3.0.png b/formal-models/.github/dbft3.0.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)
 
+## dBFT 3.0 (MEV-resistant) models
+
+The [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, the dBFT 2.0 extension was designed to
+provide a single-block finality for the encrypted transactions (a.k.a. envelope
+transactions). Compared to the dBFT 2.0, MEV-resistant dBFT algorithm includes an
+additional `post-Commit` phase that is required to be passed through by the consensus
+nodes before the block acceptance. This phase allows consensus nodes to exchange some
+additional data related to the encrypted transactions and to the final state of the
+accepting block using the new type of consensus messages. The improved protocol
+based on the dBFT 2.0 with an additional phase will be referred below as dBFT 3.0.
+
+We've checked dBFT 3.0 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). The extended 3.0 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 dBFT 3.0 (MEV-resistant) model
+
+This specification is an extension of the
+[basic dBFT 2.0 model](#basic-dbft-20-model). Compared to the base model, dBFT 3.0
+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, the extended dBFT 3.0
+does not allow to accept the block in 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 the dBFT 3.0
+algorithm:
+
+![Basic dBFT 3.0 (MEV-resistant) model transitions scheme](./.github/dbft3.0.png)
+
+Here you can find the specification file and the basic dBFT 3.0 TLC Model Checker
+launch configuration for the four "honest" consensus nodes scenario:
+
+* [TLA⁺ specification](./dbft3.0/dbft.tla)
+* [TLC Model Checker configuration](./dbft3.0/dbft___AllGoodModel.launch)
+
 ## How to run/check the TLA⁺ specification
 
 ### Prerequirements