From 4a1ae7644bb1757c359044737f1ac2516f52e635 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Thu, 1 Aug 2024 20:40:35 +0000 Subject: [PATCH 1/2] rework message injection --- APApbft.tla | 2 +- pbft.tla | 80 ++++++++++++++++++++++++++++++++++++----------------- 2 files changed, 55 insertions(+), 27 deletions(-) diff --git a/APApbft.tla b/APApbft.tla index c42566c..a9987cc 100644 --- a/APApbft.tla +++ b/APApbft.tla @@ -8,7 +8,7 @@ MC_R == 0..3 \* Set of requests which are byzantine \* @type: Set(Int); -MC_ByzR == {} +MC_ByzR == {1} MC_Tstamps == 1..3 diff --git a/pbft.tla b/pbft.tla index c9588a9..173ef59 100644 --- a/pbft.tla +++ b/pbft.tla @@ -606,7 +606,7 @@ AcceptNewView(i) == \E m \in msgs.newview : /\ m.v = views[i] + 1 /\ m.p = m.v % N - /\ \A vcm \in m.vc: ValidViewChange(vcm,views[i] + 1) + /\ \A vcm \in m.vc: ValidViewChange(vcm,m.v) /\ m.o = GenerateO(m.vc, m.p, m.v) /\ LET pms == {[ v |-> ppm.v, @@ -674,51 +674,79 @@ CommittedInv == ---- \* The following is a variant of spec for modeling byzantine behavior +\* We assume that replicas cannot impersonate other replicas InjectPreprepare(i) == - /\ \E m \in PrePrepareMessages : - \* Replicas cannot impersonate other replicas - /\ m.p = i - \* Similarly, we do not model non-primary replicas sending preprepares - /\ m.p = m.v % N - /\ msgs' = [msgs EXCEPT !.preprepare = @ \cup {m}] + /\ \E v \in Views, n \in SeqNums, d \in RequestDigests : + \* We do not model non-primary replicas sending preprepares + /\ i = v % N + /\ msgs' = [msgs EXCEPT !.preprepare = @ \cup {[ + v |-> v, + p |-> i, + n |-> n, + d |-> d]}] /\ UNCHANGED <> InjectPrepare(i) == - /\ \E m \in PrepareMessages : - /\ m.i = i - /\ msgs' = [msgs EXCEPT !.prepare = @ \cup {m}] + /\ \E v \in Views, n \in SeqNums, d \in RequestDigests : + /\ msgs' = [msgs EXCEPT !.prepare = @ \cup {[ + v |-> v, + i |-> i, + n |-> n, + d |-> d]}] /\ UNCHANGED <> InjectCommit(i) == - /\ \E m \in CommitMessages : - /\ m.i = i - /\ msgs' = [msgs EXCEPT !.commit = @ \cup {m}] + /\ \E v \in Views, n \in SeqNums, d \in RequestDigests : + /\ msgs' = [msgs EXCEPT !.commit = @ \cup {[ + v |-> v, + i |-> i, + n |-> n, + d |-> d]}] /\ UNCHANGED <> InjectReply(i) == - /\ \E m \in ReplyMessages : - /\ m.i = i - /\ msgs' = [msgs EXCEPT !.reply = @ \cup {m}] + /\ \E v \in Views, t \in Tstamps, r \in Results : + /\ msgs' = [msgs EXCEPT !.reply = @ \cup {[ + v |-> v, + t |-> t, + i |-> i, + r |-> r]}] /\ UNCHANGED <> InjectCheckpoint(i) == - /\ \E m \in CheckpointMessages : - /\ m.i = i - /\ msgs' = [msgs EXCEPT !.checkpoint = @ \cup {m}] + /\ \E n \in SeqNums, d \in StateDigests : + /\ msgs' = [msgs EXCEPT !.checkpoint = @ \cup {[ + n |-> n, + d |-> d, + i |-> i]}] /\ UNCHANGED <> InjectViewChange(i) == - /\ \E m \in ViewChangeMessages : - /\ m.i = i - /\ msgs' = [msgs EXCEPT !.viewchange = @ \cup {m}] + /\ \E v \in Views, n \in (SeqNums \cup {0}), + c \in SUBSET msgs.checkpoint, p \in [preprepare : msgs.preprepare, prepare : SUBSET msgs.prepare] : + \* Any replica that receive a view change message will check that the checkpoint/prepare proofs are valid + \* Therefore, we do not need to brother injecting view change messages with invalid proofs + /\ ValidCheckpointProof(c, n) + /\ \A pp \in p: ValidPrepareProof(pp, n) + /\ msgs' = [msgs EXCEPT !.viewchange = @ \cup {[ + v |-> v, + n |-> n, + c |-> c, + p |-> p, + i |-> i]}] /\ UNCHANGED <> InjectNewView(i) == - /\ \E m \in NewViewMessages : - /\ m.p = i - /\ m.p = m.v % N - /\ msgs' = [msgs EXCEPT !.newview = @ \cup {m}] + /\ \E v \in Views, vc \in SUBSET msgs.viewchange, o \in SUBSET msgs.prepare : + /\ i = v % N + /\ \A vcm \in vc: ValidViewChange(vcm, v) + /\ o = GenerateO(vc, i, v) + /\ msgs' = [msgs EXCEPT !.newview = @ \cup {[ + v |-> v, + vc |-> vc, + o |-> o, + p |-> i]}] /\ UNCHANGED <> \* Any message sent by a Byzantine replica can be injected into the network From 7a7209304cd61374c356231f9cbcf4bb453915ea Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Fri, 2 Aug 2024 10:04:00 +0000 Subject: [PATCH 2/2] fixing #3 --- APApbft.tla | 2 +- pbft.tla | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/APApbft.tla b/APApbft.tla index a9987cc..c42566c 100644 --- a/APApbft.tla +++ b/APApbft.tla @@ -8,7 +8,7 @@ MC_R == 0..3 \* Set of requests which are byzantine \* @type: Set(Int); -MC_ByzR == {1} +MC_ByzR == {} MC_Tstamps == 1..3 diff --git a/pbft.tla b/pbft.tla index 173ef59..259e4c3 100644 --- a/pbft.tla +++ b/pbft.tla @@ -607,6 +607,8 @@ AcceptNewView(i) == /\ m.v = views[i] + 1 /\ m.p = m.v % N /\ \A vcm \in m.vc: ValidViewChange(vcm,m.v) + \* there must be sufficient view change messages + /\ Cardinality(m.vc) = 2*F +1 /\ m.o = GenerateO(m.vc, m.p, m.v) /\ LET pms == {[ v |-> ppm.v, @@ -724,7 +726,8 @@ InjectCheckpoint(i) == InjectViewChange(i) == /\ \E v \in Views, n \in (SeqNums \cup {0}), - c \in SUBSET msgs.checkpoint, p \in [preprepare : msgs.preprepare, prepare : SUBSET msgs.prepare] : + c \in SUBSET msgs.checkpoint, + p \in SUBSET [preprepare : msgs.preprepare, prepare : SUBSET msgs.prepare] : \* Any replica that receive a view change message will check that the checkpoint/prepare proofs are valid \* Therefore, we do not need to brother injecting view change messages with invalid proofs /\ ValidCheckpointProof(c, n) @@ -758,7 +761,7 @@ InjectMessage == \/ InjectReply(i) \/ InjectCheckpoint(i) \/ InjectViewChange(i) - \/ InjectNewView(i) + \* \/ InjectNewView(i) \* Extends Next to allow message injection from byzantine replicas NextByz ==