nspcc-dev · roman-khimov · Jun 24, 2024 · Apr 25, 2024
@@ -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)

@@ -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>
@@ -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