From 72e0487a9894a96f3d9411d65711e7e5f64fae23 Mon Sep 17 00:00:00 2001 From: Alex North <445306+anorth@users.noreply.github.com> Date: Tue, 26 Mar 2024 11:32:36 +1300 Subject: [PATCH 01/19] FIP-0086 Propagate some implementation decisions back to the spec. --- FIPS/fip-0086.md | 129 ++++++++++++++++++++++++++--------------------- 1 file changed, 71 insertions(+), 58 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index bde6ff7b..7483a20b 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -179,7 +179,7 @@ The algorithm starts by initializing $finalizedTipsets[0]$ with the genesis tips 3. Execute the instance $i$ of GossiPBFT consensus. 4. Add the returned tipset from the consensus execution to the $finalizedTipsets$ list. -To prevent useless instances of GossiPBFT deciding on the same $baseChain$ because of the lack of a new epoch that provides a new proposal, we make the $\texttt{ChainHead}()$ function blocking in that it does not return a proposal unless (i) the drand epoch value for the epoch immediately following the latest finalized tipset is received and (ii) the current chain head is different from the chain head of the finalized chain. +To prevent useless instances of GossiPBFT deciding on the same $baseChain$ because of the lack of a new epoch that provides a new proposal, we make the $\texttt{ChainHead}()$ function blocking in that it does not return a proposal unless the current chain head is different from the chain head of the finalized chain. ### Changes to EC: Fork Choice Rule @@ -225,39 +225,59 @@ GossiPBFT was designed with the Filecoin network in mind and presents a set of f #### Message format, signatures, and equivocation -Messages include the following fields: $\langle Sender, Signature, MsgType, Value, Instance, [Round, Evidence, Ticket] \rangle$. As $Round$, $Evidence$, and $Ticket$ are fields that not all message types require, when not required by a message type, their default value is used (i.e. $0$, $\texttt{AggregatedEvidence}(0, [] ECTipset \lbrace\rbrace, 0, 0, [] byte \lbrace\rbrace, [] byte \lbrace\rbrace)$, and $[] byte \lbrace\rbrace$, respectively). We refer to a _field_ of message $m$, with $m.field$: +Messages include the following fields: $\langle Sender, Signature, MsgType, Value, Instance, [Round, Justification, Ticket] \rangle$. As $Round$, Justification, and $Ticket$ are fields that not all message types require, when not required by a message type, their default value is used (i.e. $0$, $nil$, and $[] byte \lbrace\rbrace$, respectively). We refer to a _field_ of message $m$, with $m.field$: ``` -type GossiPBFTMessage struct { - // ID of the sender/signer of this message (a miner actor) +// A message in the Granite protocol. +// The same message structure is used for all rounds and phases. +// Note that the message is self-attesting so no separate envelope or signature is needed. +// - The signature field fixes the included sender ID via the implied public key; +// - The signature payload includes all fields a sender can freely choose; +// - The ticket field is a signature of the same public key, so also self-attesting. +type GMessage struct { + // ID of the sender/signer of this message (a miner actor ID). Sender ActorID - // BLS Signature - Signature []bytes - // Enumeration of QUALITY, PREPARE, COMMIT, CONVERGE, DECIDE - MsgType int - // Chain of tipsets proposed/voted for finalization in this instance. - // Non-empty: the first entry is the base tipset finalized in instance-1 + // Vote is the payload that is signed by the signature. + Vote Payload + // Signature by the sender's public key over serialized vote payload. + Signature []byte + // VRF ticket for CONVERGE messages (otherwise empty byte array). + Ticket Ticket + // Justification for this message, or nil. + Justification *Justification +} + +type Justification struct { + // Vote is the payload that is signed by the signature. + Vote Payload + // RLE+ serialization of the indexes in the base power table of the signers. + Signers []byte + // BLS aggregate signature of signers over the vote. + Signature []byte +} + +// Fields of the message that make up the signature payload. +type Payload struct { + // GossiPBFT instance number. + Instance uint64 + // GossiPBFT round number. + Round uint64 + // GossiPBFT step number. + Step uint64 + // Chain of tipsets proposed/voted for finalisation. + // Always non-empty; the first entry is the base tipset finalised in the previous instance. Value []ECTipset - // GossiPBFT instance number - Instance int - // GossiPBFT round for this message - Round int - // Aggregated GossiPBFTMessages that justify this message - Evidence AggregatedEvidence - // GossiPBFT ticket (only for CONVERGE) - Ticket []byte } type ECTipset struct { Epoch int - Tipset CID // Or TipsetKey (concat of block header CIDs) - Weight BigInt - PowerTable CID // CID of a PowerTable + Tipset []byte // CBOR-serialized tipset key, a canonical array of the tipset's block header CIDs. + PowerTable CID // Commitment to resulting power table. } // Table of nodes with power > 0 and their public keys. // This is expected to be calculated from the EC chain state and provided to GossiPBFT. -// In descending order to provide unique representation. +// Ordered by (power descending, participant ascending). type PowerTable { Entries []PowerTableEntry } @@ -267,23 +287,6 @@ type PowerTableEntry struct { Power BigInt Key BLSPublicKey } - -// Aggregated list of GossiPBFT messages with the same instance, round and value. Used as evidence for justification of messages -type AggregatedEvidence struct { - // Enumeration of QUALITY, PREPARE, COMMIT, CONVERGE, DECIDE - MsgType int - // Chain of tipsets proposed/voted for finalisation in this instance. - // Non-empty: the first entry is the base tipset finalised in instance-1 - Value []ECTipset - // GossiPBFT instance number - Instance int - // GossiPBFT round - Round int - // Indexes in the base power table of the signers (bitset) - Signers []bytes - // BLS aggregate signature of signers - Signature []bytes -} ``` All messages broadcast by a participant have their participant ID in the sender field and contain a digital signature by that participant $(m.Signature)$ over $(Instance || MsgType || Value || Round)$. The protocol assumes aggregatable signatures (e.g., BLS, Schnorr), resilient to [rogue public key attacks](https://crypto.stanford.edu/~dabo/pubs/papers/BLSmultisig.html) (see [Boneh, Drijvers, and Neven](https://eprint.iacr.org/2018/483.pdf) construction). @@ -345,14 +348,14 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: \*participants is implicitly used to calculate quorums 1: round ← 0; -2: decideSent ← False; +2: terminated ← False; 3: proposal ← inputChain; \* holds what the participant locally believes should be a decision 4: timeout ← 2*Δ 5: ECCompatibleChains ← all prefixes of proposal, not lighter than baseChain 6: value ← proposal \* used to communicate the voted value to others (proposal or 丄) 7: evidence ← nil \* used to communicate optional evidence for the voted value -8: while (not decideSent) { +8: while (not terminated) { 9: if (round = 0) 10: BEBroadcast ; trigger (timeout) 11: collect a clean set M of valid QUALITY messages @@ -393,7 +396,8 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 38: if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) \* decide 39: evidence ← Aggregate(M) 39: BEBroadcast -40: decideSent ← True +40: terminated ← True + return (StrongQuorumValue(M), Aggregate(M)) 41: if (∃ m ∈ M: m.value ≠ 丄) \* m.value was possibly decided by others 42: proposal ← m.value; \* sway local proposal to possibly decided value 43: evidence ← m.evidence \* strong PREPARE quorum is inherited evidence @@ -403,14 +407,10 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 47: timeout ← updateTimeout(timeout, round) 48: } \*end while -49: collect a clean set M of DECIDE messages +49: collect a clean set M of valid DECIDE messages until (HasStrongQuorumValue(M)) \* Collect a strong quorum of decide outside the round loop -50: return (StrongQuorumValue(M), Aggregate(M)) - -51: upon reception of a valid message and not decideSent -52: decideSent ← True -53: BEBroadcast -54: go to line 49 +50: terminated ← True + return (StrongQuorumValue(M), Aggregate(M)) ``` Note that the selection of the heaviest prefix in line 16 need not read the tipsets' weights, as only prefixes that extend each other can gather a strong quorum in QUALITY. In other words: if there are two tipsets $t_1, t_2$ that gather a strong quorum of QUALITY, then either the corresponding chain that has $t_1$ as head tipset is a prefix of the analogous chain that has $t_2$ as head, or viceversa (since the adversary controls < ⅓ of the QAP). As a result, selecting the heaviest prefix is as simple as selecting the highest blockheight, while ensuring all proposed prefixes that gather a strong quorum in QUALITY extend each other as a sanity check. @@ -425,7 +425,7 @@ ECupdate(chain): #### Valid messages and evidence -The $\texttt{Valid}()$ predicate (referred to in lines 11, 22, 29, 37, and 51) is defined below. +The $\texttt{Valid}()$ predicate (referred to in lines 11, 22, 29, and 37) is defined below. ``` Valid(m): | For a message m to be valid, @@ -434,15 +434,21 @@ If m is not properly signed: | m must be properly signed. return False if m.instance != instance | m must match the instance ID return False -If m.step = QUALITY AND | A QUALITY message must - NOT IsPrefix(baseChain, m.proposal) | contain a proposal prefixed - return False | with baseChain. +If not (IsPrefix(baseChain, m.value) | A value must be bottom + or m.value = 丄) | or start with baseChain. + return False +If m.step = QUALITY AND | A QUALITY message + m.round != 0 | must be for round 0 + return false +If m.step = DECIDE AND | A DECIDE message + m.round != 0 | must specify round = 0 + return false If m.step = CONVERGE AND | A CONVERGE message (m.ticket does not pass VRF validation | must have a valid VRF ticket OR m.round = 0) | and round > 0. return False -If m.step ∈ {CONVERGE, COMMIT} AND | CONVERGE, COMMIT - NOT ValidEvidence(m) | must contain valid evidence. +If m.step ∈ {CONVERGE, COMMIT, DECIDE} AND | CONVERGE, COMMIT, DECIDE + not ValidEvidence(m) | must contain valid evidence. return False return True ``` @@ -469,10 +475,17 @@ OR (m = | valid COMMIT AND ∀ m' ∈ M: m'.value = m.value) | for the same value, or OR (m.value = 丄)) | COMMIT is for 丄 with | no evidence + +OR (m = | valid DECIDE + AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a strong quorum + AND ∀ m' ∈ M: m'.step = COMMIT | of PREPARE messages + AND all the same round (!= m.round) | from some (all the same) round + AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance + AND ∀ m' ∈ M: m'.value = m.value) | for the same value ``` ### Evidence verification complexity -Note that during the validation of each CONVERGE and COMMIT message, two signatures need to be verified: (1) the signature of the message contents, produced by the sender of the message (first check above) and (2) the aggregate signature in $m.evidence$ ($\texttt{ValidEvidence}(m)$ above). The former can be verified using the sender's public key (stored in the power table). The latter, being an aggregated signature, requires aggregating public keys of all the participants whose signatures it combines. Notice that the evidence of each message can be signed by a different set of participants, which requires aggregating a linear number of public BLS keys (in system size) per evidence verification. +Note that during the validation of each CONVERGE, COMMIT and DECIDE message, two signatures need to be verified: (1) the signature of the message contents, produced by the sender of the message (first check above) and (2) the aggregate signature in $m.evidence$ ($\texttt{ValidEvidence}(m)$ above). The former can be verified using the sender's public key (stored in the power table). The latter, being an aggregated signature, requires aggregating public keys of all the participants whose signatures it combines. Notice that the evidence of each message can be signed by a different set of participants, which requires aggregating a linear number of public BLS keys (in system size) per evidence verification. However, a participant only needs to verify the evidence once for each *unique* message (in terms of (step, round, value)) received. Moreover, verification can further be reduced to those messages a participant uses to make progress (such as advancing to the next step or deciding), ignoring the rest as they are not needed for progress. This reduces the number of evidence verifications in each step to at most one. @@ -485,14 +498,14 @@ An instance of GossiPBFT requires a seed σ that must be common among all partic GossiPBFT ensures termination provided that (i) all participants start the instance at most $\Delta$ apart, and (ii) the estimate on Δ is large enough for $\Delta$-synchrony in some round (either because of the real network delay recovering from asynchrony or because of the estimate increasing). -[Given prior tests performed on GossipSub](https://research.protocol.ai/publications/gossipsub-v1.1-evaluation-report/vyzovitis2020.pdf) (see also [here](https://gist.github.com/jsoares/9ce4c0ba6ebcfd2afa8f8993890e2d98)), we expect that almost all participants will reach sent messages within $Δ=3s$, with a huge majority receiving them even after $Δ=2s$. However, if several participants start the instance $Δ + ε$ after some other participants, termination is not guaranteed for the selected timeouts of $2*Δ$. Thus, we do not rely on an explicit synchrony bound for correctness. Instead, we (i) use drand as a beacon to synchronize participants within an instance and (ii) increase the estimate of Δ locally within an instance as rounds progress without decision. +[Given prior tests performed on GossipSub](https://research.protocol.ai/publications/gossipsub-v1.1-evaluation-report/vyzovitis2020.pdf) (see also [here](https://gist.github.com/jsoares/9ce4c0ba6ebcfd2afa8f8993890e2d98)), we expect that almost all participants will reach sent messages within $Δ=3s$, with a huge majority receiving them even after $Δ=2s$. However, if several participants start the instance $Δ + ε$ after some other participants, termination is not guaranteed for the selected timeouts of $2*Δ$. Thus, we do not rely on an explicit synchrony bound for correctness. Instead, we increase the estimate of Δ locally within an instance as rounds progress without decision. The synchronization of participants is performed in the call to $\texttt{updateTimeout(timeout, round)}$ (line 47), and works as follows: * Participants start an instance with $Δ=2s$. * Participants set their timeout for the current round to $Δ*1.3^{r}$ where $r$ is the round number ($r=0$ for the first round). -Additionally, as an optimization, participants could continue to the subsequent step once the execution of the current step has been determined, without waiting for the timeout. For example, if a participant receives QUALITY messages from all participants, it can proceed to the next step without waiting for the timeout. More generally, if the remaining valid messages to be received cannot change the execution of the step, regardless of the values contained in the messages, then a participant should continue to the next step. +Additionally, as an optimization, participants may continue to the subsequent step once the execution of the current step has been determined, without waiting for the timeout. For example, if a participant receives QUALITY messages from all participants, it can proceed to the next step without waiting for the timeout. More generally, if the remaining valid messages to be received cannot change the execution of the step, regardless of the values contained in the messages, then a participant may continue to the next step. ### Synchronization of Participants across Instances From 6b25bc610d2e91fc2c040ab3ee8f6bbf0f233ba5 Mon Sep 17 00:00:00 2001 From: Alex North <445306+anorth@users.noreply.github.com> Date: Tue, 26 Mar 2024 12:40:24 +1300 Subject: [PATCH 02/19] Removed weak quorum --- FIPS/fip-0086.md | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 7483a20b..b973217b 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -319,14 +319,6 @@ A set of messages $M$ that does not contain equivocating messages is called _cle ``` * `StrongQuorumValue(M)` * Returns $v$ if $\texttt{HasStrongQuorumValue}(M)$ holds, $nil$ otherwise. -* `HasWeakQuorumValue(M)` - * Where $M$ is a clean set of messages of the same type and the same round - * The predicate returns True iff there is a value $v$, such that there is a set $P$ of participants who are senders of messages in $M$ such that their message value is exactly $v$ and $\texttt{Power}(P)>1/3$. More precisely: - ``` - HasWeakQuorumValue(M) = ∃ v: Power({p : ∃ m∈ M: m.sender=p AND m.value=v})>1/3 - ``` -* `WeakQuorumValue(M)` - * Returns $v$ if $\texttt{HasWeakQuorumValue}(M)$ holds, $nil$ otherwise. * `LowestTicketProposal(M)` * Let $M$ be a clean set of CONVERGE messages for the same round. * If $M = ∅$, the predicate returns $baseChain$. @@ -453,7 +445,7 @@ If m.step ∈ {CONVERGE, COMMIT, DECIDE} AND | CONVERGE, COMMIT, DECIDE return True ``` -The $\texttt{ValidEvidence}()$ predicate is defined below. Note that QUALITY, PREPARE and DECIDE messages do not need evidence. In fact, DECIDE does not need any protocol-specific validation, since a weak quorum of DECIDE with the same value is required to trigger any execution of the protocol. +The $\texttt{ValidEvidence}()$ predicate is defined below. Note that QUALITY and PREPARE messages do not need evidence. ``` ValidEvidence(m): From eb13a13b93ad5fc4ca6a0692d5679e260d634251 Mon Sep 17 00:00:00 2001 From: Alex North <445306+anorth@users.noreply.github.com> Date: Wed, 27 Mar 2024 10:11:54 +1300 Subject: [PATCH 03/19] Review responses. --- FIPS/fip-0086.md | 56 +++++++++++++++++++++++++----------------------- 1 file changed, 29 insertions(+), 27 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index b973217b..bf9adfda 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -225,16 +225,16 @@ GossiPBFT was designed with the Filecoin network in mind and presents a set of f #### Message format, signatures, and equivocation -Messages include the following fields: $\langle Sender, Signature, MsgType, Value, Instance, [Round, Justification, Ticket] \rangle$. As $Round$, Justification, and $Ticket$ are fields that not all message types require, when not required by a message type, their default value is used (i.e. $0$, $nil$, and $[] byte \lbrace\rbrace$, respectively). We refer to a _field_ of message $m$, with $m.field$: +Messages include the following fields: $\langle Sender, Signature, MsgType, Value, Instance, [Round, Evidence, Ticket] \rangle$. As $Round$, $Evidence$, and $Ticket$ are fields that not all message types require, when not required by a message type, their default value is used (i.e. $0$, $nil$, and $[] byte \lbrace\rbrace$, respectively). We refer to a _field_ of message $m$, with $m.field$: ``` -// A message in the Granite protocol. +// A message in the GossiPBFT protocol. // The same message structure is used for all rounds and phases. // Note that the message is self-attesting so no separate envelope or signature is needed. // - The signature field fixes the included sender ID via the implied public key; // - The signature payload includes all fields a sender can freely choose; // - The ticket field is a signature of the same public key, so also self-attesting. -type GMessage struct { +type GossiPBFTMessage struct { // ID of the sender/signer of this message (a miner actor ID). Sender ActorID // Vote is the payload that is signed by the signature. @@ -243,11 +243,11 @@ type GMessage struct { Signature []byte // VRF ticket for CONVERGE messages (otherwise empty byte array). Ticket Ticket - // Justification for this message, or nil. - Justification *Justification + // Evidence that justifies this message, or nil. + Evidence *Evidence } -type Justification struct { +type Evidence struct { // Vote is the payload that is signed by the signature. Vote Payload // RLE+ serialization of the indexes in the base power table of the signers. @@ -340,14 +340,14 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: \*participants is implicitly used to calculate quorums 1: round ← 0; -2: terminated ← False; +2: decideSent ← False; 3: proposal ← inputChain; \* holds what the participant locally believes should be a decision 4: timeout ← 2*Δ 5: ECCompatibleChains ← all prefixes of proposal, not lighter than baseChain 6: value ← proposal \* used to communicate the voted value to others (proposal or 丄) 7: evidence ← nil \* used to communicate optional evidence for the voted value -8: while (not terminated) { +8: while (not decideSent) { 9: if (round = 0) 10: BEBroadcast ; trigger (timeout) 11: collect a clean set M of valid QUALITY messages @@ -388,8 +388,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 38: if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) \* decide 39: evidence ← Aggregate(M) 39: BEBroadcast -40: terminated ← True - return (StrongQuorumValue(M), Aggregate(M)) +40: decideSent ← True \* break loop, wait for other DECIDE messages 41: if (∃ m ∈ M: m.value ≠ 丄) \* m.value was possibly decided by others 42: proposal ← m.value; \* sway local proposal to possibly decided value 43: evidence ← m.evidence \* strong PREPARE quorum is inherited evidence @@ -400,11 +399,12 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 48: } \*end while 49: collect a clean set M of valid DECIDE messages - until (HasStrongQuorumValue(M)) \* Collect a strong quorum of decide outside the round loop -50: terminated ← True - return (StrongQuorumValue(M), Aggregate(M)) + until (HasStrongQuorumValue(M)) \* collect a strong quorum of decide outside the round loop +50: return (StrongQuorumValue(M), Aggregate(M)) \* terminate the algorithm with a decision ``` -Note that the selection of the heaviest prefix in line 16 need not read the tipsets' weights, as only prefixes that extend each other can gather a strong quorum in QUALITY. In other words: if there are two tipsets $t_1, t_2$ that gather a strong quorum of QUALITY, then either the corresponding chain that has $t_1$ as head tipset is a prefix of the analogous chain that has $t_2$ as head, or viceversa (since the adversary controls < ⅓ of the QAP). As a result, selecting the heaviest prefix is as simple as selecting the highest blockheight, while ensuring all proposed prefixes that gather a strong quorum in QUALITY extend each other as a sanity check. +Note that the selection of the heaviest prefix in line 16 does not need access to the tipsets' EC weights, as only prefixes that extend each other can gather a strong quorum in QUALITY. In other words: if there are two tipsets $t_1, t_2$ that gather a strong quorum of QUALITY, then either the corresponding chain that has $t_1$ as head tipset is a prefix of the analogous chain that has $t_2$ as head, or viceversa (since the adversary controls < ⅓ of the QAP). As a result, selecting the heaviest prefix is as simple as selecting the highest blockheight, while ensuring all proposed prefixes that gather a strong quorum in QUALITY extend each other as a sanity check. + +Implementations may optimise this algorithm to treat the reception of an aggregated signature over some (MsgType, Instance, Round, Value) as evidence of a message as if it had received the same tuple of values directly from each participant in the aggregate. This may be used to effectively skip a partially-complete step. In the particular case of a DECIDE message, which carries evidence of a strong quorum of COMMITs for the same round and value, a participant may immediately send its own DECIDE for the same value (copying the evidence) and exit the loop at line 8. Also, concurrently, we expect that the participant feeds to GossiPBFT chains that are incentive-compatible with EC. To this end, GossiPBFT has a separate invocation called $\texttt{ECUpdate}()$, which is called by an external process at a participant once EC delivers a $chain$ such that $inputChain$ is a prefix of $chain$ (i.e., EC at a participant delivers an extension of $inputChain$). This part is critical to ensuring the progress property in conjunction with lines 24-25. @@ -455,29 +455,28 @@ AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a stro AND ((∀ m' ∈ M: m'.step = COMMIT AND m'.value = 丄) | of COMMIT msgs for 丄 OR (∀ m' ∈ M: m'.step = PREPARE AND | or PREPARE msgs for m'.value = m.value)) | CONVERGE value - AND (∀ m' ∈ M: m'.round = m.round-1) | from previous round - AND (∀ m' ∈ M: m'.instance = m.instance))) | from the same instance + AND (∀ m' ∈ M: m'.round = m.round-1) | from previous round to CONVERGE + AND (∀ m' ∈ M: m'.instance = m.instance))) | from the same instance as CONVERGE OR (m = | valid COMMIT AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a strong quorum AND ∀ m' ∈ M: m'.step = PREPARE | of PREPARE messages - AND ∀ m' ∈ M: m'.round = m.round | from the same round - AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance - AND ∀ m' ∈ M: m'.value = m.value) | for the same value, or - OR (m.value = 丄)) | COMMIT is for 丄 with - | no evidence + AND ∀ m' ∈ M: m'.round = m.round | from the same round as COMMIT + AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance as COMMIT + AND ∀ m' ∈ M: m'.value = m.value) | for the same value as COMMIT, or + OR (m.value = 丄) AND m.evidence=nil) | COMMIT is for 丄 with no evidence OR (m = | valid DECIDE AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a strong quorum - AND ∀ m' ∈ M: m'.step = COMMIT | of PREPARE messages - AND all the same round (!= m.round) | from some (all the same) round - AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance - AND ∀ m' ∈ M: m'.value = m.value) | for the same value + AND ∀ m' ∈ M: m'.step = COMMIT | of COMMIT messages + AND ∀ m', m'' ∈ M: m'.round = m''.round | from some the same round as each other + AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance as DECIDE + AND ∀ m' ∈ M: m'.value = m.value) | for the same value as DECIDE ``` ### Evidence verification complexity -Note that during the validation of each CONVERGE, COMMIT and DECIDE message, two signatures need to be verified: (1) the signature of the message contents, produced by the sender of the message (first check above) and (2) the aggregate signature in $m.evidence$ ($\texttt{ValidEvidence}(m)$ above). The former can be verified using the sender's public key (stored in the power table). The latter, being an aggregated signature, requires aggregating public keys of all the participants whose signatures it combines. Notice that the evidence of each message can be signed by a different set of participants, which requires aggregating a linear number of public BLS keys (in system size) per evidence verification. +Note that during the validation of each CONVERGE, COMMIT, and DECIDE message, two signatures need to be verified: (1) the signature of the message contents, produced by the sender of the message (first check above) and (2) the aggregate signature in $m.evidence$ ($\texttt{ValidEvidence}(m)$ above). The former can be verified using the sender's public key (stored in the power table). The latter, being an aggregated signature, requires aggregating public keys of all the participants whose signatures it combines. Notice that the evidence of each message can be signed by a different set of participants, which requires aggregating a linear number of public BLS keys (in system size) per evidence verification. However, a participant only needs to verify the evidence once for each *unique* message (in terms of (step, round, value)) received. Moreover, verification can further be reduced to those messages a participant uses to make progress (such as advancing to the next step or deciding), ignoring the rest as they are not needed for progress. This reduces the number of evidence verifications in each step to at most one. @@ -490,7 +489,7 @@ An instance of GossiPBFT requires a seed σ that must be common among all partic GossiPBFT ensures termination provided that (i) all participants start the instance at most $\Delta$ apart, and (ii) the estimate on Δ is large enough for $\Delta$-synchrony in some round (either because of the real network delay recovering from asynchrony or because of the estimate increasing). -[Given prior tests performed on GossipSub](https://research.protocol.ai/publications/gossipsub-v1.1-evaluation-report/vyzovitis2020.pdf) (see also [here](https://gist.github.com/jsoares/9ce4c0ba6ebcfd2afa8f8993890e2d98)), we expect that almost all participants will reach sent messages within $Δ=3s$, with a huge majority receiving them even after $Δ=2s$. However, if several participants start the instance $Δ + ε$ after some other participants, termination is not guaranteed for the selected timeouts of $2*Δ$. Thus, we do not rely on an explicit synchrony bound for correctness. Instead, we increase the estimate of Δ locally within an instance as rounds progress without decision. +[Given prior tests performed on GossipSub](https://research.protocol.ai/publications/gossipsub-v1.1-evaluation-report/vyzovitis2020.pdf) (see also [here](https://gist.github.com/jsoares/9ce4c0ba6ebcfd2afa8f8993890e2d98)), we expect that sent messages will reach almost all participants within $Δ=3s$, with a majority receiving them even after $Δ=2s$. However, if several participants start the instance $Δ + ε$ after some other participants, termination is not guaranteed for the selected timeouts of $2*Δ$. Thus, we do not rely on an explicit synchrony bound for correctness. Instead, we increase the estimate of Δ locally within an instance as rounds progress without decision. The synchronization of participants is performed in the call to $\texttt{updateTimeout(timeout, round)}$ (line 47), and works as follows: @@ -749,6 +748,9 @@ We refer to the stand-alone implementation in a simulated environment in the [go - [x] Complete benchmarking around message complexity and computational/networking requirements. - [x] Decide between implicit and explicit evidence, taking into account benchmark results. +- [ ] Specify power table delay mechanism, local message queue, bounds, etc +- [ ] Re-specify timing of new instances after EC epochs +- [ ] Specify power table commitment - [ ] Finalize and incorporate the WIP finality exchange protocol. - [ ] Update and move proofs of correctness and other supplemental documentation into `resources` From f3e8733853ef9a2e5a3367af1bad914965501df4 Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Thu, 28 Mar 2024 12:03:40 +0100 Subject: [PATCH 04/19] Update valid(m) function --- FIPS/fip-0086.md | 52 ++++++++++++++++++++++++++++-------------------- 1 file changed, 30 insertions(+), 22 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index bf9adfda..ef20d3b4 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -420,29 +420,37 @@ ECupdate(chain): The $\texttt{Valid}()$ predicate (referred to in lines 11, 22, 29, and 37) is defined below. ``` -Valid(m): | For a message m to be valid, - -If m is not properly signed: | m must be properly signed. - return False -if m.instance != instance | m must match the instance ID - return False -If not (IsPrefix(baseChain, m.value) | A value must be bottom - or m.value = 丄) | or start with baseChain. - return False -If m.step = QUALITY AND | A QUALITY message - m.round != 0 | must be for round 0 - return false -If m.step = DECIDE AND | A DECIDE message - m.round != 0 | must specify round = 0 - return false -If m.step = CONVERGE AND | A CONVERGE message - (m.ticket does not pass VRF validation | must have a valid VRF ticket - OR m.round = 0) | and round > 0. +Valid(m): | For a message m to be valid, + + If m.signature does not verify | m must be properly signed. + return False + If m.instance != instance | m must match the instance ID. + return False + If m.step = QUALITY AND | A QUALITY message must + NOT IsPrefix(baseChain, m.proposal) | contain a proposal prefixed + return False | with baseChain. + If m.sender has zero power or is unknown: | The sender must have power and be known. return False -If m.step ∈ {CONVERGE, COMMIT, DECIDE} AND | CONVERGE, COMMIT, DECIDE - not ValidEvidence(m) | must contain valid evidence. - return False -return True + If NOT (m.value = 丄 | m's value must extend baseChain + OR baseChain.isPrefix(m.value)) | or be 丄 + return False + If m.step = QUALITY AND | A QUALITY message must + (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. + return False | + If m.step = CONVERGE AND | A CONVERGE message must + (m.round = 0 OR m.value = 丄 OR | have non-zero round, non-丄 value, + m.ticket does not pass VRF validation) | and a valid ticket. + return False | + If m.step = DECIDE AND | A DECIDE message must + (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. + return False | + If m.step IN {QUALITY, PREPARE} | If the step never requires evidence + | (QUALITY, PREPARE), + If m.evidence != nil: | evidence should not be present. + return False | + Else + return ValidEvidence(m) | + return True | ``` The $\texttt{ValidEvidence}()$ predicate is defined below. Note that QUALITY and PREPARE messages do not need evidence. From 7de7bba036a40e2a1c03f647da856d55029b0c97 Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Tue, 2 Apr 2024 13:32:43 +0200 Subject: [PATCH 05/19] Update fip-0086.md Remove redundant clause --- FIPS/fip-0086.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index ef20d3b4..ecf31893 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -426,9 +426,6 @@ Valid(m): | For a message m to be valid, return False If m.instance != instance | m must match the instance ID. return False - If m.step = QUALITY AND | A QUALITY message must - NOT IsPrefix(baseChain, m.proposal) | contain a proposal prefixed - return False | with baseChain. If m.sender has zero power or is unknown: | The sender must have power and be known. return False If NOT (m.value = 丄 | m's value must extend baseChain From d91afebaeb06d24652d3bc8108c17ed5b2471c1d Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Mon, 8 Apr 2024 18:35:52 +0200 Subject: [PATCH 06/19] First round of changes from Guy's first Audit --- FIPS/fip-0086.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index ecf31893..20807039 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -26,7 +26,7 @@ We specify a mechanism for fast finality with the F3 component. F3 is expected t ## Change Motivation * The long time to finality on Filecoin mainnet restricts or severely affects applications built on Filecoin (e.g., IPC, Axelar, Wormhole, Glif, …). -* Even though applications on Filecoin can set a lower finalization time than the built-in 900 epochs, delayed finalization for important transactions will require tens of minutes with a longest-chain protocol like Filecoin's Expected Consensus (EC). +* Even though applications on Filecoin can set a lower finalization time than the built-in 900 epochs, delayed finalization for important transactions will require multiple epochs with Filecoin's Expected Consensus (EC). * Long finalization times also affect exchanges, by imposing a long confirmation period (often more than 1 hour) for users managing their FIL assets, and bridges, which face extended wait times for asset transfers. * Bridging to other systems is not currently fast, safe, and verifiable. @@ -40,7 +40,7 @@ We specify a mechanism for fast finality with the F3 component. F3 is expected t ![](../resources/fip-0086/chain.png) -Two or more tipsets of the same epoch with different parent tipsets (like tipsets $C$ and $C'$ above) form a _fork_ in the chain. Forks are resolved using a _fork choice rule_, a deterministic algorithm that, given a blockchain data structure, returns the heaviest tipset, called the _head_. We refer to the path from genesis to the head as the _canonical chain_. Participants may have different views of the blockchain, resulting in other canonical chains. For example, if a participant $p_1$ is not (yet) aware of tipset $D$, it would consider $C$ the heaviest tipset with the canonical chain $[G A B C]$. Another participant $p_2$ aware of tipset $D$ will consider $[G A C' D]$ to be the canonical chain. Once $p_1$ becomes aware of tipset $D$, it will update its canonical chain to $[G A C' D]$ - this is called _reorganization_. We say a tipset is _finalized_ when a reorganization involving that tipset is impossible, i.e., when a different path that does not contain the tipset cannot become the canonical chain. +Two or more tipsets of the same epoch with different ancestor tipsets (like tipsets $C$ and $C'$ above) form a _fork_ in the chain. Forks are resolved using a _fork choice rule_, a deterministic algorithm that, given a blockchain data structure, returns the heaviest tipset, called the _head_. We refer to the path from genesis to the head as the _canonical chain_. Participants may have different views of the blockchain, resulting in other canonical chains. For example, if a participant $p_1$ is not (yet) aware of tipset $D$, it would consider $C$ the heaviest tipset with the canonical chain $[G A B C]$. Another participant $p_2$ aware of tipset $D$ will consider $[G A C' D]$ to be the canonical chain. Once $p_1$ becomes aware of tipset $D$, it will update its canonical chain to $[G A C' D]$ - this is called _reorganization_. We say a tipset is _finalized_ when a reorganization involving that tipset is impossible, i.e., when a different path that does not contain the tipset cannot become the canonical chain. In EC and, generally, longest-chain protocols, the probability of a path from some tipset $h$ to the genesis tipset becoming finalized increases with the number of descendant tipsets of $h$. This happens because the weight of the heaviest chain increases the fastest, as the tipsets with the most new blocks are appended to it (assuming that honest participants form a majority). In the particular case of EC, in each epoch, most created blocks are expected to come from honest participants and thus extend the heaviest chain. Consequently, it becomes progressively harder for a different path to overcome that weight. Over time, the probability of a tipset never undergoing a reorganization becomes high enough that the tipset is considered final for all practical purposes. In the Filecoin network, a tipset that is part of the heaviest chain is considered final after 900 epochs (or, equivalently, 7.5 hours) from its proposal. @@ -188,9 +188,9 @@ EC needs to be modified to accommodate the finalization of tipsets by F3. **This The current EC fork-choice rule selects, from all the known tipsets, the tipset backed by the most weight. As the F3 component finalizes tipsets, the fork-choice rule must ensure that the heaviest finalized chain is always a prefix of the heaviest chain, preventing reorganizations of the already finalized chain. -We achieve this by adjusting the definition of weight for a finalized prefix: the heaviest finalized chain is the one that **matches exactly the tipsets finalized by F3**, in that a tipset $t'$ that is a superset of finalized tipset $t$ in the same epoch is not heavier than $t$ itself, despite it being backed by more EC power. +We achieve this by adjusting the fork choice rule in the presence of a finalized prefix: the fork choice rule selects the heaviest chain out of all chians with a prefix that **matches exactly all tipsets finalized by F3**, in that a tipset $t'$ that is a superset of finalized tipset $t$ in the same epoch is not heavier than $t$ itself, despite it being backed by more EC power. -This redefinition of the heaviest chain is consistent with the abstract notion of the heaviest chain being backed by the most power because a finalized tipset has been backed by a super-majority of participants in GossiPBFT. In contrast, any non-finalized block in the same epoch is only backed in that epoch by the EC proposer. +This redefinition of the fork choice rule is consistent with the abstract notion of the heaviest chain being backed by the most power because a finalized tipset has been backed by a super-majority of participants in GossiPBFT. In contrast, any non-finalized block in the same epoch is only backed in that epoch by the EC proposer. We illustrate the updated rule in the following figure, where blocks in blue are finalized blocks, and all blocks are assumed to be proposed by a proposer holding only one EC ticket (the weight of a chain is the number of blocks): @@ -663,9 +663,9 @@ Because of changes to the EC fork choice rule, this FIP requires a network upgra - EB: Successful catch-up to currently executed instance and decision in it. Make sure new participants catch up timely with the rest (as progress will happen while they catch up). * Significant network delays: - Participants holding ½ QAP start the instance 10 seconds after the other half. - - EB: After round 5, participants are synchronized by drand and decide in this round. + - EB: Participants eventually decide. - All messages are delayed by 10 seconds. - - EB: After some round >5, participants can decide. + - EB: Participants eventually decide. * Tests on message validity: - Invalid messages should be discarded; this includes: * Old/decided instance From 61d48e51280a231032dc4fb6315949b0af9e02bb Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Tue, 9 Apr 2024 14:09:11 +0200 Subject: [PATCH 07/19] Update GossiPBFT Pseudocode (TODO still update line numbering and other pseudocodes) --- FIPS/fip-0086.md | 118 +++++++++++++++++++++++++++++------------------ 1 file changed, 72 insertions(+), 46 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index dba96cdb..9a034723 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -322,7 +322,8 @@ A set of messages $M$ that does not contain equivocating messages is called _cle * `LowestTicketProposal(M)` * Let $M$ be a clean set of CONVERGE messages for the same round. * If $M = ∅$, the predicate returns $baseChain$. - * If $M \ne ∅$, the predicate returns $m.value$, such that $m$ is the message in $M$ with the lowest ticket ($m.ticket$). + * If $M \ne ∅$, the predicate returns $m.value$ and $m.evidence$, such that $m$ is the message in $M$ with the lowest ticket ($m.ticket$). M will never be empty as the participant must at least deliver its own CONVERGE message. + * `Aggregate(M)` * Where $M$ is a clean set of messages of the same type $T$, round $r$, and instance $i$, with $v=\texttt{StrongQuorumValue}(M)≠nil$. ``` @@ -343,17 +344,17 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 2: decideSent ← False; 3: proposal ← inputChain; \* holds what the participant locally believes should be a decision 4: timeout ← 2*Δ -5: ECCompatibleChains ← all prefixes of proposal, not lighter than baseChain -6: value ← proposal \* used to communicate the voted value to others (proposal or 丄) -7: evidence ← nil \* used to communicate optional evidence for the voted value - -8: while (not decideSent) { -9: if (round = 0) -10: BEBroadcast ; trigger (timeout) -11: collect a clean set M of valid QUALITY messages +5: value ← proposal \* used to communicate the voted value to others (proposal or 丄) +6: evidence ← nil \* used to communicate optional evidence for the voted value + +7: while (not decideSent) { +8: if (round = 0) +9: BEBroadcast ; trigger (timeout) +10: collect a clean set M of valid QUALITY messages from this instance until HasStrongQuorum(proposal, M) OR timeout expires -12: let C={prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)} -13: if (C = ∅) +11: let C={prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)} +12: if (C = ∅) +13: C ← {baseChain} 14: proposal ← baseChain \* no proposals of high-enough quality 15: else 16: proposal ← heaviest prefix ∈ C \* this becomes baseChain or sth heavier @@ -363,44 +364,69 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 19: ticket ← VRF(Randomness(baseChain) || instance || round) 20: value ← proposal \* set local proposal as value in CONVERGE message 21: BEBroadcast ; trigger(timeout) -22: collect a clean set M of valid CONVERGE msgs from this round +22: collect a clean set M of valid CONVERGE msgs from this round and instance until timeout expires -23: value ← LowestTicketProposal(M) \* leader election -24: if value ∈ ECCompatibleChains \* see also lines 55-56 -25: proposal ← value \* we sway proposal if the value is EC compatible -26: else -27: value ← 丄 \* vote for not deciding in this round - -28: BEBroadcast ; trigger(timeout) -29: collect a clean set M of valid msgs \* match PREPARE value against local proposal - until Power(M) > ⅔ OR timeout expires -30: if (Power(M) > ⅔) \* strong quorum of PREPAREs for local proposal -31: value ← proposal \* vote for deciding proposal (COMMIT) -32: evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence -33: else -34: value ← 丄 \* vote for not deciding in this round -35: evidence ← nil - -36: BEBroadcast ; trigger(timeout) -37: collect a clean set M of valid COMMIT messages from this round +23: prepareReadyToSend ← False +24: while (!prepareReadyToSend){ +25: value, evidence ← LowestTicketProposal(M) \* leader election +26: if (evidence is a strong quorum of PREPAREs AND mightHaveBeenDecided(value, r-1)): +27: C ← C ∪ {value} +28: if (value ∈ C) +29: proposal ←value \* we sway proposal if the value is incentive compatible (i.e., in C) +30: prepareReadyToSend ← True \* Exit loop +31: else +32: M = {m ∈ M | m.value != value AND m.evidence.value != evidence.value} \* Update M for next iteration } + +33: BEBroadcast ; trigger(timeout) +34: collect a clean set M of valid PREPARE messages from this round and instance + until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) = proposal) + OR (timeout expires AND Power(M)>2/3) +35: If (HasStrongQuorumValue AND StrongQuorumValue(M) = proposal) \* strong quorum of PREPAREs for local proposal +36: value ← proposal \* vote for deciding proposal (COMMIT) +37: evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence +38: else +39: value ← 丄 \* vote for not deciding in this round +40: evidence ← nil + +41: BEBroadcast ; trigger(timeout) +42: collect a clean set M of valid COMMIT messages from this round and instance until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) OR (timeout expires AND Power(M)>2/3) -38: if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) \* decide -39: evidence ← Aggregate(M) -39: BEBroadcast -40: decideSent ← True \* break loop, wait for other DECIDE messages -41: if (∃ m ∈ M: m.value ≠ 丄) \* m.value was possibly decided by others -42: proposal ← m.value; \* sway local proposal to possibly decided value -43: evidence ← m.evidence \* strong PREPARE quorum is inherited evidence -44: else \* no participant decided in this round -45: evidence ← Aggregate(M) \* strong quorum of COMMITs for 丄 is evidence -46: round ← round + 1; -47: timeout ← updateTimeout(timeout, round) -48: } \*end while - -49: collect a clean set M of valid DECIDE messages +43: if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) \* decide +44: evidence ← Aggregate(M) +45: BEBroadcast +46: decideSent ← True \* break loop, wait for other DECIDE messages +47: if (∃ m ∈ M: m.value ≠ 丄 s.t. mightHaveBeenDecided(m.value, r)) \* m.value was possibly decided by others +48: C ← C ∪ {m.value} \* add to candidate values if not there +49: proposal ← m.value; \* sway local proposal to possibly decided value +50: evidence ← m.evidence \* strong PREPARE quorum is inherited evidence +51: else \* no participant decided in this round +52: evidence ← Aggregate(M) \* strong quorum of COMMITs for 丄 is evidence +53: round ← round + 1; +54: timeout ← updateTimeout(timeout, round) +55: } \*end while + +56: collect a clean set M of valid DECIDE messages until (HasStrongQuorumValue(M)) \* collect a strong quorum of decide outside the round loop -50: return (StrongQuorumValue(M), Aggregate(M)) \* terminate the algorithm with a decision +57: return (StrongQuorumValue(M), Aggregate(M)) \* terminate the algorithm with a decision +``` +``` +\* decide anytime +58: upon reception of a valid AND not decideSent +59: decideSent ← TRUE +60: BEBroadcast Date: Tue, 9 Apr 2024 16:46:10 +0200 Subject: [PATCH 08/19] Update references to line numbers --- FIPS/fip-0086.md | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 9a034723..af678a3a 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -428,22 +428,16 @@ The helper function mightHaveBeenDecided returns False if, given the already del 66: return False 67: return True ``` -Note that the selection of the heaviest prefix in line 16 does not need access to the tipsets' EC weights, as only prefixes that extend each other can gather a strong quorum in QUALITY. In other words: if there are two tipsets $t_1, t_2$ that gather a strong quorum of QUALITY, then either the corresponding chain that has $t_1$ as head tipset is a prefix of the analogous chain that has $t_2$ as head, or viceversa (since the adversary controls < ⅓ of the QAP). As a result, selecting the heaviest prefix is as simple as selecting the highest blockheight, while ensuring all proposed prefixes that gather a strong quorum in QUALITY extend each other as a sanity check. +Note that the selection of the heaviest prefix in line 16 does not need access to the tipsets' EC weights, as only prefixes that extend each other can gather a strong quorum in QUALITY. In other words: if there are two tipsets $t_1, t_2$ that gather a strong quorum of QUALITY, then either the corresponding chain that has $t_1$ as head tipset is a prefix of the analogous chain that has $t_2$ as head, or viceversa (since the adversary controls < ⅓ of the QAP). As a result, selecting the heaviest prefix is as simple as selecting the highest blockheight (greatest number of blocks), while ensuring all proposed prefixes that gather a strong quorum in QUALITY extend each other as a sanity check. -Implementations may optimise this algorithm to treat the reception of an aggregated signature over some (MsgType, Instance, Round, Value) as evidence of a message as if it had received the same tuple of values directly from each participant in the aggregate. This may be used to effectively skip a partially-complete step. In the particular case of a DECIDE message, which carries evidence of a strong quorum of COMMITs for the same round and value, a participant may immediately send its own DECIDE for the same value (copying the evidence) and exit the loop at line 8. +Implementations may optimise this algorithm to treat the reception of an aggregated signature over some (MsgType, Instance, Round, Value) as evidence of a message as if it had received the same tuple of values directly from each participant in the aggregate. This may be used to effectively skip a partially-complete step. In the particular case of a DECIDE message, which carries evidence of a strong quorum of COMMITs for the same round and value, a participant immediately sends its own DECIDE for the same value (copying the evidence) and exits the loop at line 7. -Also, concurrently, we expect that the participant feeds to GossiPBFT chains that are incentive-compatible with EC. To this end, GossiPBFT has a separate invocation called $\texttt{ECUpdate}()$, which is called by an external process at a participant once EC delivers a $chain$ such that $inputChain$ is a prefix of $chain$ (i.e., EC at a participant delivers an extension of $inputChain$). This part is critical to ensuring the progress property in conjunction with lines 24-25. +Also, concurrently, we expect that the participant feeds to GossiPBFT chains that are incentive-compatible with EC. To this end, we restrict the set C of candidate values that the participant contributes to deciding to only values that either (i) pass the QUALITY step or (ii) may have been decided by other participants (hence the functin `mightHaveBeenDecided`). -``` -ECupdate(chain): - -55: If (IsPrefix(proposal, chain)) \* sanity check -56: ECCompatibleChains ← ECCompatibleChains ∪ all prefixes of chain, not lighter than baseChain -``` #### Valid messages and evidence -The $\texttt{Valid}()$ predicate (referred to in lines 11, 22, 29, and 37) is defined below. +The $\texttt{Valid}()$ predicate (referred to in lines 10, 22, 34, and 42, and 56) is defined below. ``` Valid(m): | For a message m to be valid, @@ -521,7 +515,7 @@ GossiPBFT ensures termination provided that (i) all participants start the insta [Given prior tests performed on GossipSub](https://research.protocol.ai/publications/gossipsub-v1.1-evaluation-report/vyzovitis2020.pdf) (see also [here](https://gist.github.com/jsoares/9ce4c0ba6ebcfd2afa8f8993890e2d98)), we expect that sent messages will reach almost all participants within $Δ=3s$, with a majority receiving them even after $Δ=2s$. However, if several participants start the instance $Δ + ε$ after some other participants, termination is not guaranteed for the selected timeouts of $2*Δ$. Thus, we do not rely on an explicit synchrony bound for correctness. Instead, we increase the estimate of Δ locally within an instance as rounds progress without decision. -The synchronization of participants is performed in the call to $\texttt{updateTimeout(timeout, round)}$ (line 47), and works as follows: +The synchronization of participants is performed in the call to $\texttt{updateTimeout(timeout, round)}$ (line 54), and works as follows: * Participants start an instance with $Δ=2s$. * Participants set their timeout for the current round to $Δ*1.3^{r}$ where $r$ is the round number ($r=0$ for the first round). From 24f6327ac6fd752a80dd8ec7a2a46571fd57123e Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Tue, 9 Apr 2024 16:50:34 +0200 Subject: [PATCH 09/19] Fix typos (code statements, indenting) --- FIPS/fip-0086.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index af678a3a..198b6e2d 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -354,7 +354,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: until HasStrongQuorum(proposal, M) OR timeout expires 11: let C={prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)} 12: if (C = ∅) -13: C ← {baseChain} +13: C ← {baseChain} 14: proposal ← baseChain \* no proposals of high-enough quality 15: else 16: proposal ← heaviest prefix ∈ C \* this becomes baseChain or sth heavier @@ -381,7 +381,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 34: collect a clean set M of valid PREPARE messages from this round and instance until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) = proposal) OR (timeout expires AND Power(M)>2/3) -35: If (HasStrongQuorumValue AND StrongQuorumValue(M) = proposal) \* strong quorum of PREPAREs for local proposal +35: if (HasStrongQuorumValue AND StrongQuorumValue(M) = proposal) \* strong quorum of PREPAREs for local proposal 36: value ← proposal \* vote for deciding proposal (COMMIT) 37: evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence 38: else @@ -441,30 +441,30 @@ The $\texttt{Valid}()$ predicate (referred to in lines 10, 22, 34, and 42, and 5 ``` Valid(m): | For a message m to be valid, - If m.signature does not verify | m must be properly signed. + if m.signature does not verify | m must be properly signed. return False - If m.instance != instance | m must match the instance ID. + if m.instance != instance | m must match the instance ID. return False - If m.sender has zero power or is unknown: | The sender must have power and be known. + if m.sender has zero power or is unknown: | The sender must have power and be known. return False - If NOT (m.value = 丄 | m's value must extend baseChain + if NOT (m.value = 丄 | m's value must extend baseChain OR baseChain.isPrefix(m.value)) | or be 丄 return False - If m.step = QUALITY AND | A QUALITY message must + if m.step = QUALITY AND | A QUALITY message must (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. return False | - If m.step = CONVERGE AND | A CONVERGE message must + if m.step = CONVERGE AND | A CONVERGE message must (m.round = 0 OR m.value = 丄 OR | have non-zero round, non-丄 value, m.ticket does not pass VRF validation) | and a valid ticket. return False | - If m.step = DECIDE AND | A DECIDE message must + if m.step = DECIDE AND | A DECIDE message must (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. return False | - If m.step IN {QUALITY} | If the step never requires evidence + if m.step IN {QUALITY} | If the step never requires evidence | (QUALITY, PREPARE), - If m.evidence != nil: | evidence should not be present. + if m.evidence != nil: | evidence should not be present. return False | - Else + else return ValidEvidence(m) | return True | ``` From 56c81061456866eb19305dde0839a7e61e8a8863 Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Tue, 9 Apr 2024 17:09:11 +0200 Subject: [PATCH 10/19] Fix valid(m) and validEvidence(m) --- FIPS/fip-0086.md | 71 ++++++++++++++++++++++++++++-------------------- 1 file changed, 41 insertions(+), 30 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 198b6e2d..15f43b75 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -449,7 +449,9 @@ Valid(m): | For a message m to be valid, return False if NOT (m.value = 丄 | m's value must extend baseChain OR baseChain.isPrefix(m.value)) | or be 丄 - return False + return False + if m.step != CONVERGE AND m.ticket != nil | ticket must be nil if not CONVERGE + return False if m.step = QUALITY AND | A QUALITY message must (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. return False | @@ -461,42 +463,51 @@ Valid(m): | For a message m to be valid, (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. return False | if m.step IN {QUALITY} | If the step never requires evidence - | (QUALITY, PREPARE), - if m.evidence != nil: | evidence should not be present. - return False | + if m.evidence != nil: | (QUALITY), evidence should not be present. + return False | else return ValidEvidence(m) | return True | ``` -The $\texttt{ValidEvidence}()$ predicate is defined below. Note that QUALITY and PREPARE messages do not need evidence. +The $\texttt{ValidEvidence}()$ predicate is defined below. Note that QUALITY messages do not need evidence. ``` -ValidEvidence(m): - -(m = | valid CONVERGE -AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a strong quorum - AND ((∀ m' ∈ M: m'.step = COMMIT AND m'.value = 丄) | of COMMIT msgs for 丄 - OR (∀ m' ∈ M: m'.step = PREPARE AND | or PREPARE msgs for - m'.value = m.value)) | CONVERGE value - AND (∀ m' ∈ M: m'.round = m.round-1) | from previous round to CONVERGE - AND (∀ m' ∈ M: m'.instance = m.instance))) | from the same instance as CONVERGE - - -OR (m = | valid COMMIT - AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a strong quorum - AND ∀ m' ∈ M: m'.step = PREPARE | of PREPARE messages - AND ∀ m' ∈ M: m'.round = m.round | from the same round as COMMIT - AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance as COMMIT - AND ∀ m' ∈ M: m'.value = m.value) | for the same value as COMMIT, or - OR (m.value = 丄) AND m.evidence=nil) | COMMIT is for 丄 with no evidence - -OR (m = | valid DECIDE - AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a strong quorum - AND ∀ m' ∈ M: m'.step = COMMIT | of COMMIT messages - AND ∀ m', m'' ∈ M: m'.round = m''.round | from the same round as each other - AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance as DECIDE - AND ∀ m' ∈ M: m'.value = m.value) | for the same value as DECIDE +ValidEvidence(m= ): + +if ( step = PREPARE and round = 0) | in the first round, + AND (evidence = nil) | evidence for PREPARE + return True | is nil + +if (step = COMMIT and value = 丄) | a COMMIT for 丄 carries no evidence + AND (evidence = nil) + return True + +If (evidence.instance != instance) | the instance of the evidence must be the + return False | same as that of the message + + | valid evidences for +return (step = CONVERGE OR (step = PREPARE AND round>0) | CONVERGE and PREPARE in + AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | round>0 is strong quorum + AND ((∀ m’ ∈ M: m’.step = COMMIT AND m’.value = 丄) | of COMMIT msgs for 丄 + OR (∀ m’ ∈ M: m’.step = PREPARE AND | or PREPARE msgs for + m’.value = value)) | CONVERGE value + AND (∀ m’ ∈ M: m’.round = round-1))) | from previous round + + +OR (step=COMMIT | valid COMMIT evidence + AND ((∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | is a strong quorum + AND ∀ m’ ∈ M: m’.step = PREPARE | of PREPARE messages + AND ∀ m’ ∈ M: m’.round = round | from the same round + AND ∀ m’ ∈ M: m’.value = value) | for the same value, or + OR (value = 丄)) | COMMIT is for 丄 with + | no evidence + +OR (step = DECIDE | valid DECIDE evidence + AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | is a strong quorum + AND ∀ m’ ∈ M: m’.step = COMMIT | of COMMIT messages + AND ∀ m’ ∈ M: m’.round = round | from the same round + AND ∀ m’ ∈ M: m’.value = value)) | for the same value ``` ### Evidence verification complexity From c6e32b41ade9cf311c43af1a349294f0376d230f Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Tue, 9 Apr 2024 17:19:38 +0200 Subject: [PATCH 11/19] Fix DECIDE format --- FIPS/fip-0086.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 15f43b75..2b3aa1e0 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -394,7 +394,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: OR (timeout expires AND Power(M)>2/3) 43: if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) \* decide 44: evidence ← Aggregate(M) -45: BEBroadcast +45: BEBroadcast 46: decideSent ← True \* break loop, wait for other DECIDE messages 47: if (∃ m ∈ M: m.value ≠ 丄 s.t. mightHaveBeenDecided(m.value, r)) \* m.value was possibly decided by others 48: C ← C ∪ {m.value} \* add to candidate values if not there @@ -414,7 +414,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: \* decide anytime 58: upon reception of a valid AND not decideSent 59: decideSent ← TRUE -60: BEBroadcast ): +ValidEvidence(m= ): if ( step = PREPARE and round = 0) | in the first round, AND (evidence = nil) | evidence for PREPARE From 2974f70bf2effc96bcc86d380693836c97ed6e43 Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Tue, 9 Apr 2024 17:30:52 +0200 Subject: [PATCH 12/19] Update fip-0086.md --- FIPS/fip-0086.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 2b3aa1e0..54b0bb66 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -755,7 +755,7 @@ The modifications proposed in this FIP have far-reaching implications for the se * **Censorship.** F3 and GossiPBFT are designed with censorship resistance in mind. The updated fork choice rule means that an adversary controlling at least more than ⅓ QAP can try to perform a censorship attack if honest participants start an instance of GossiPBFT proposing at least two distinct inputs. While this attack is theoretically possible, it is notably hard to perform on F3 given the QUALITY step of GossiPBFT and other mitigation strategies specifically put in place to protect against this. We strongly believe that, even against a majority adversary, the mitigations designed will prevent such an attack. * **Liveness.** Implementing F3 introduces the risk that an adversary controlling at least ⅓ QAP prevents termination of a GossiPBFT instance. In that case, the F3 component would halt, not finalizing any tipset anymore. At the same time, EC would still operate, outputting tipsets and considering them final after 900 epochs. The liveness of the system is thus not affected by attacks on the liveness of F3. -* **Safety.** Implementing F3 ensures the safety of finalized outputs during regular or even congested networks against a Byzantine adversary controlling less than ⅓ QAP. For stronger adversaries, F3 provides mitigations to prevent censorship attacks, as outlined above. If deemed necessary, the punishment and recovery from coalitions in the event of an attempted attack on safety can be explored in future FIPs. Note that safety is already significantly improved by F3 compared to the status quo: F3 provides safety of finalized outputs two orders of magnitude faster than the current estimate of 900 epochs during regular network operation. +* **Safety.** Implementing F3 ensures the safety of finalized outputs during regular or even congested networks against a Byzantine adversary controlling less than ⅓ QAP. For stronger adversaries, F3 provides mitigations to prevent censorship attacks, as outlined above. If deemed necessary, the punishment and recovery from coalitions in the event of an attempted attack on safety can be explored in future FIPs. Note that (safe) finality time is already significantly improved by F3 compared to the status quo: F3 provides safety of finalized outputs two orders of magnitude faster than the current estimate of 900 epochs during regular network operation. * **Denial-of-service (DoS).** The implementation of the F3 preserves resistance against DoS attacks currently ensured by Filecoin, thanks to the fully leaderless nature of GossiPBFT and to the use of a VRF to self-assign tickets during the CONVERGE step. * **Committees.** This FIP proposes to have all participants run all instances of GossiPBFT. While this ensures optimal resilience against a Byzantine adversary, it can render the system unusable if the number of participants grows too large. While we are still evaluating the maximum practical number of participants in F3, it is expected to be at least one order of magnitude greater than the current number of participants in Filecoin. This introduces an attack vector: if the scalability limit is 100,000 participants, a participant holding as little as 3% of the current QAP can perform a Sybil attack to render the system unusable, with the minimum QAP required per identity. As a result, the implementation should favor the messages of the more powerful participants if the number of participants grows too large. Given that favoring more powerful participants discriminates against the rest, affecting decentralization, amending F3 to use committees in the event of the number of participants exceeding the practical limit will be the topic of a future FIP, as well as the analysis of optimized message aggregation in the presence of self-selected committees. From b9c1db2ecb7e5bb79feae24b55133249a2e10f5a Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Thu, 11 Apr 2024 11:48:57 +0200 Subject: [PATCH 13/19] Changes from 2nd audit by Guy --- FIPS/fip-0086.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 54b0bb66..4f6d7576 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -377,7 +377,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 31: else 32: M = {m ∈ M | m.value != value AND m.evidence.value != evidence.value} \* Update M for next iteration } -33: BEBroadcast ; trigger(timeout) +33: BEBroadcast ; trigger(timeout) \* evidence is nil in round=0 34: collect a clean set M of valid PREPARE messages from this round and instance until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) = proposal) OR (timeout expires AND Power(M)>2/3) From 5dab603453cc7b2eb674df93f14219248cfe8a7f Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Thu, 11 Apr 2024 18:03:37 +0200 Subject: [PATCH 14/19] Make C a globally scoped variable and update line numbering --- FIPS/fip-0086.md | 141 +++++++++++++++++++++++------------------------ 1 file changed, 69 insertions(+), 72 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 4f6d7576..d22a9ba8 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -340,104 +340,101 @@ We illustrate the pseudocode for GossiPBFT below, consisting of 3 steps per roun GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: \*participants is implicitly used to calculate quorums -1: round ← 0; -2: decideSent ← False; -3: proposal ← inputChain; \* holds what the participant locally believes should be a decision +1: round ← 0 +2: decideSent ← False +3: proposal ← inputChain \* holds what the participant locally believes should be a decision 4: timeout ← 2*Δ 5: value ← proposal \* used to communicate the voted value to others (proposal or 丄) 6: evidence ← nil \* used to communicate optional evidence for the voted value +7: C ← {baseChain} -7: while (not decideSent) { -8: if (round = 0) -9: BEBroadcast ; trigger (timeout) -10: collect a clean set M of valid QUALITY messages from this instance +8: while (not decideSent) { +9: if (round = 0) +10: BEBroadcast ; trigger (timeout) +11: collect a clean set M of valid QUALITY messages from this instance until HasStrongQuorum(proposal, M) OR timeout expires -11: let C={prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)} -12: if (C = ∅) -13: C ← {baseChain} -14: proposal ← baseChain \* no proposals of high-enough quality -15: else -16: proposal ← heaviest prefix ∈ C \* this becomes baseChain or sth heavier -17: value ← proposal - -18: if (round > 0) \* CONVERGE -19: ticket ← VRF(Randomness(baseChain) || instance || round) -20: value ← proposal \* set local proposal as value in CONVERGE message -21: BEBroadcast ; trigger(timeout) -22: collect a clean set M of valid CONVERGE msgs from this round and instance +12: C ← {prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)} +13: proposal ← heaviest prefix ∈ C \* this becomes baseChain or sth heavier +14: value ← proposal + +15: if (round > 0) \* CONVERGE +16: ticket ← VRF(Randomness(baseChain) || instance || round) +17: value ← proposal \* set local proposal as value in CONVERGE message +18: BEBroadcast ; trigger(timeout) +19: collect a clean set M of valid CONVERGE msgs from this round and instance until timeout expires -23: prepareReadyToSend ← False -24: while (!prepareReadyToSend){ -25: value, evidence ← LowestTicketProposal(M) \* leader election -26: if (evidence is a strong quorum of PREPAREs AND mightHaveBeenDecided(value, r-1)): -27: C ← C ∪ {value} -28: if (value ∈ C) -29: proposal ←value \* we sway proposal if the value is incentive compatible (i.e., in C) -30: prepareReadyToSend ← True \* Exit loop -31: else -32: M = {m ∈ M | m.value != value AND m.evidence.value != evidence.value} \* Update M for next iteration } - -33: BEBroadcast ; trigger(timeout) \* evidence is nil in round=0 -34: collect a clean set M of valid PREPARE messages from this round and instance +20: prepareReadyToSend ← False +21: while (not prepareReadyToSend){ +22: value, evidence ← LowestTicketProposal(M) \* leader election +23: if (evidence is a strong quorum of PREPAREs AND mightHaveBeenDecided(value, r-1)): +24: C ← C ∪ {value} +25: if (value ∈ C) +26: proposal ←value \* we sway proposal if the value is incentive compatible (i.e., in C) +27: prepareReadyToSend ← True \* Exit loop +28: else +29: M = {m ∈ M | m.value != value AND m.evidence.value != evidence.value} \* Update M for next iteration } + +30: BEBroadcast ; trigger(timeout) \* evidence is nil in round=0 +31: collect a clean set M of valid PREPARE messages from this round and instance until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) = proposal) OR (timeout expires AND Power(M)>2/3) -35: if (HasStrongQuorumValue AND StrongQuorumValue(M) = proposal) \* strong quorum of PREPAREs for local proposal -36: value ← proposal \* vote for deciding proposal (COMMIT) -37: evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence -38: else -39: value ← 丄 \* vote for not deciding in this round -40: evidence ← nil - -41: BEBroadcast ; trigger(timeout) -42: collect a clean set M of valid COMMIT messages from this round and instance +32: if (HasStrongQuorumValue AND StrongQuorumValue(M) = proposal) \* strong quorum of PREPAREs for local proposal +33: value ← proposal \* vote for deciding proposal (COMMIT) +34: evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence +35: else +36: value ← 丄 \* vote for not deciding in this round +37: evidence ← nil + +38: BEBroadcast ; trigger(timeout) +39: collect a clean set M of valid COMMIT messages from this round and instance until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) OR (timeout expires AND Power(M)>2/3) -43: if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) \* decide -44: evidence ← Aggregate(M) -45: BEBroadcast -46: decideSent ← True \* break loop, wait for other DECIDE messages -47: if (∃ m ∈ M: m.value ≠ 丄 s.t. mightHaveBeenDecided(m.value, r)) \* m.value was possibly decided by others -48: C ← C ∪ {m.value} \* add to candidate values if not there -49: proposal ← m.value; \* sway local proposal to possibly decided value -50: evidence ← m.evidence \* strong PREPARE quorum is inherited evidence -51: else \* no participant decided in this round -52: evidence ← Aggregate(M) \* strong quorum of COMMITs for 丄 is evidence -53: round ← round + 1; -54: timeout ← updateTimeout(timeout, round) -55: } \*end while - -56: collect a clean set M of valid DECIDE messages +40: if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) \* decide +41: evidence ← Aggregate(M) +42: BEBroadcast +43: decideSent ← True \* break loop, wait for other DECIDE messages +44: if (∃ m ∈ M: m.value ≠ 丄 s.t. mightHaveBeenDecided(m.value, r)) \* m.value was possibly decided by others +45: C ← C ∪ {m.value} \* add to candidate values if not there +46: proposal ← m.value; \* sway local proposal to possibly decided value +47: evidence ← m.evidence \* strong PREPARE quorum is inherited evidence +48: else \* no participant decided in this round +49: evidence ← Aggregate(M) \* strong quorum of COMMITs for 丄 is evidence +50: round ← round + 1; +51: timeout ← updateTimeout(timeout, round) +52: } \*end while + +53: collect a clean set M of valid DECIDE messages until (HasStrongQuorumValue(M)) \* collect a strong quorum of decide outside the round loop -57: return (StrongQuorumValue(M), Aggregate(M)) \* terminate the algorithm with a decision +54: return (StrongQuorumValue(M), Aggregate(M)) \* terminate the algorithm with a decision ``` ``` \* decide anytime -58: upon reception of a valid AND not decideSent -59: decideSent ← TRUE -60: BEBroadcast AND not decideSent +56: decideSent ← True +57: BEBroadcast Date: Thu, 11 Apr 2024 18:20:21 +0200 Subject: [PATCH 15/19] Small fix --- FIPS/fip-0086.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index d22a9ba8..f3da0d8c 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -353,7 +353,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 10: BEBroadcast ; trigger (timeout) 11: collect a clean set M of valid QUALITY messages from this instance until HasStrongQuorum(proposal, M) OR timeout expires -12: C ← {prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)} +12: C ← C ∪ {prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)} 13: proposal ← heaviest prefix ∈ C \* this becomes baseChain or sth heavier 14: value ← proposal From 1fcce20dff9438d488ea520bb85d7ceae6661320 Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Fri, 12 Apr 2024 11:24:28 +0200 Subject: [PATCH 16/19] Fix couple comments --- FIPS/fip-0086.md | 44 +++++++++++++++++++++----------------------- 1 file changed, 21 insertions(+), 23 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index f3da0d8c..f9787e09 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -472,39 +472,37 @@ The $\texttt{ValidEvidence}()$ predicate is defined below. Note that QUALITY mes ``` ValidEvidence(m= ): -if ( step = PREPARE and round = 0) | in the first round, - AND (evidence = nil) | evidence for PREPARE - return True | is nil +if ( step = PREPARE and round = 0) | in the first round, + AND (evidence = nil) | evidence for PREPARE + return True | is nil if (step = COMMIT and value = 丄) | a COMMIT for 丄 carries no evidence AND (evidence = nil) return True -If (evidence.instance != instance) | the instance of the evidence must be the - return False | same as that of the message +If (evidence.instance != instance) | the instance of the evidence must be the + return False | same as that of the message | valid evidences for return (step = CONVERGE OR (step = PREPARE AND round>0) | CONVERGE and PREPARE in - AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | round>0 is strong quorum - AND ((∀ m’ ∈ M: m’.step = COMMIT AND m’.value = 丄) | of COMMIT msgs for 丄 - OR (∀ m’ ∈ M: m’.step = PREPARE AND | or PREPARE msgs for - m’.value = value)) | CONVERGE value - AND (∀ m’ ∈ M: m’.round = round-1))) | from previous round + AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | round>0 is strong quorum + AND ((∀ m’ ∈ M: m’.step = COMMIT AND m’.value = 丄) | of COMMIT msgs for 丄 + OR (∀ m’ ∈ M: m’.step = PREPARE AND | or PREPARE msgs for + m’.value = value)) | CONVERGE value + AND (∀ m’ ∈ M: m’.round = round-1))) | from previous round -OR (step=COMMIT | valid COMMIT evidence - AND ((∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | is a strong quorum - AND ∀ m’ ∈ M: m’.step = PREPARE | of PREPARE messages - AND ∀ m’ ∈ M: m’.round = round | from the same round - AND ∀ m’ ∈ M: m’.value = value) | for the same value, or - OR (value = 丄)) | COMMIT is for 丄 with - | no evidence - -OR (step = DECIDE | valid DECIDE evidence - AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | is a strong quorum - AND ∀ m’ ∈ M: m’.step = COMMIT | of COMMIT messages - AND ∀ m’ ∈ M: m’.round = round | from the same round - AND ∀ m’ ∈ M: m’.value = value)) | for the same value +OR (step=COMMIT | valid COMMIT evidence + AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | is a strong quorum + AND ∀ m’ ∈ M: m’.step = PREPARE | of PREPARE messages + AND ∀ m’ ∈ M: m’.round = round | from the same round + AND ∀ m’ ∈ M: m’.value = value)) | for the same value, or + +OR (step = DECIDE | valid DECIDE evidence + AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | is a strong quorum + AND ∀ m’ ∈ M: m’.step = COMMIT | of COMMIT messages + AND ∀ m’ ∈ M: m’.round = round | from the same round + AND ∀ m’ ∈ M: m’.value = value)) | for the same value ``` ### Evidence verification complexity From daccc3f5a3fe65e755c091648be4b4eab56729a8 Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Mon, 15 Apr 2024 10:42:53 +0200 Subject: [PATCH 17/19] Typos and indentation fixes --- FIPS/fip-0086.md | 45 ++++++++++++++++++++++----------------------- 1 file changed, 22 insertions(+), 23 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index b3970daa..9d06f8df 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -352,7 +352,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 6: evidence ← nil \* used to communicate optional evidence for the voted value 7: C ← {baseChain} -8: while (not decideSent) { +8: while (NOT decideSent) { 9: if (round = 0) 10: BEBroadcast ; trigger (timeout) 11: collect a clean set M of valid QUALITY messages from this instance @@ -381,7 +381,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: 30: BEBroadcast ; trigger(timeout) \* evidence is nil in round=0 31: collect a clean set M of valid PREPARE messages from this round and instance until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) = proposal) - OR (timeout expires AND Power(M)>2/3) + OR (timeout expires AND Power(M)>2/3) 32: if (HasStrongQuorumValue AND StrongQuorumValue(M) = proposal) \* strong quorum of PREPAREs for local proposal 33: value ← proposal \* vote for deciding proposal (COMMIT) 34: evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence @@ -424,10 +424,10 @@ The helper function mightHaveBeenDecided returns False if, given the already del ``` 59: mightHaveBeenDecided(value, round): 60: M ← { m | m.step = COMMIT AND m.round = round AND m is valid} -61: M' ← { m | m ∈ M AND m.value = value } -62: if Power(M') + (1-Power(M)) < ⅓ : \* value cannot have been decided -63: return False -64: return True +61: M' ← { m | m ∈ M AND m.value = value } +62: f Power(M') + (1-Power(M)) < ⅓ : \* value cannot have been decided +63: return False +64: return True ``` Note that the selection of the heaviest prefix in line 13 does not need access to the tipsets' EC weights, as only prefixes that extend each other can gather a strong quorum in QUALITY. In other words: if there are two tipsets $t_1, t_2$ that gather a strong quorum of QUALITY, then either the corresponding chain that has $t_1$ as head tipset is a prefix of the analogous chain that has $t_2$ as head, or viceversa (since the adversary controls < ⅓ of the QAP). As a result, selecting the heaviest prefix is as simple as selecting the highest blockheight (greatest number of blocks), while ensuring all proposed prefixes that gather a strong quorum in QUALITY extend each other as a sanity check. @@ -439,35 +439,34 @@ Also, concurrently, we expect that the participant feeds to GossiPBFT chains tha #### Valid messages and evidence The $\texttt{Valid}()$ predicate (referred to in lines 11, 19, 31, and 39, 53, 55) is defined below. - ``` Valid(m): | For a message m to be valid, if m.signature does not verify | m must be properly signed. - return False + return False | if m.instance != instance | m must match the instance ID. - return False + return False | if m.sender has zero power or is unknown: | The sender must have power and be known. - return False - if NOT (m.value = 丄 | m's value must extend baseChain + return False | + if NOT (m.value = 丄 | m's value must extend baseChain OR baseChain.isPrefix(m.value)) | or be 丄 - return False - if m.step != CONVERGE AND m.ticket != nil | ticket must be nil if not CONVERGE - return False + return False | + if m.step != CONVERGE AND m.ticket != nil | ticket must be nil if not CONVERGE + return False | if m.step = QUALITY AND | A QUALITY message must - (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. - return False | + (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. + return False | if m.step = CONVERGE AND | A CONVERGE message must - (m.round = 0 OR m.value = 丄 OR | have non-zero round, non-丄 value, + (m.round = 0 OR m.value = 丄 OR | have non-zero round, non-丄 value, m.ticket does not pass VRF validation) | and a valid ticket. - return False | + return False | if m.step = DECIDE AND | A DECIDE message must - (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. + (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. return False | if m.step IN {QUALITY} | If the step never requires evidence if m.evidence != nil: | (QUALITY), evidence should not be present. - return False | - else - return ValidEvidence(m) | + return False | + else | + return ValidEvidence(m) | return True | ``` @@ -754,7 +753,7 @@ The modifications proposed in this FIP have far-reaching implications for the se * **Censorship.** F3 and GossiPBFT are designed with censorship resistance in mind. The updated fork choice rule means that an adversary controlling at least more than ⅓ QAP can try to perform a censorship attack if honest participants start an instance of GossiPBFT proposing at least two distinct inputs. While this attack is theoretically possible, it is notably hard to perform on F3 given the QUALITY step of GossiPBFT and other mitigation strategies specifically put in place to protect against this. We strongly believe that, even against a majority adversary, the mitigations designed will prevent such an attack. * **Liveness.** Implementing F3 introduces the risk that an adversary controlling at least ⅓ QAP prevents termination of a GossiPBFT instance. In that case, the F3 component would halt, not finalizing any tipset anymore. At the same time, EC would still operate, outputting tipsets and considering them final after 900 epochs. The liveness of the system is thus not affected by attacks on the liveness of F3. -* **Safety.** Implementing F3 ensures the safety of finalized outputs during regular or even congested networks against a Byzantine adversary controlling less than ⅓ QAP. For stronger adversaries, F3 provides mitigations to prevent censorship attacks, as outlined above. If deemed necessary, the punishment and recovery from coalitions in the event of an attempted attack on safety can be explored in future FIPs. Note that (safe) finality time is already significantly improved by F3 compared to the status quo: F3 provides safety of finalized outputs two orders of magnitude faster than the current estimate of 900 epochs during regular network operation. +* **Safety.** Implementing F3 ensures the safety of finalized outputs during regular or even congested networks against a Byzantine adversary controlling less than ⅓ QAP. For stronger adversaries, F3 provides mitigations to prevent censorship attacks, as outlined above. If deemed necessary, the punishment and recovery from coalitions in the event of an attempted attack on safety can be explored in future FIPs. Note that the (safe) finality time is already significantly improved by F3 compared to the status quo: F3 provides safety of finalized outputs two orders of magnitude faster than the current parameter of 900 epochs during regular network operation. * **Denial-of-service (DoS).** The implementation of the F3 preserves resistance against DoS attacks currently ensured by Filecoin, thanks to the fully leaderless nature of GossiPBFT and to the use of a VRF to self-assign tickets during the CONVERGE step. * **Committees.** This FIP proposes to have all participants run all instances of GossiPBFT. While this ensures optimal resilience against a Byzantine adversary, it can render the system unusable if the number of participants grows too large. While we are still evaluating the maximum practical number of participants in F3, it is expected to be at least one order of magnitude greater than the current number of participants in Filecoin. This introduces an attack vector: if the scalability limit is 100,000 participants, a participant holding as little as 3% of the current QAP can perform a Sybil attack to render the system unusable, with the minimum QAP required per identity. As a result, the implementation should favor the messages of the more powerful participants if the number of participants grows too large. Given that favoring more powerful participants discriminates against the rest, affecting decentralization, amending F3 to use committees in the event of the number of participants exceeding the practical limit will be the topic of a future FIP, as well as the analysis of optimized message aggregation in the presence of self-selected committees. From 417e229d553575c40d4a8a253964b2ae65c94bc4 Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Thu, 11 Apr 2024 11:57:07 +0200 Subject: [PATCH 18/19] Update to use greatest ticket and adjust by power --- FIPS/fip-0086.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 9d06f8df..2387947e 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -323,10 +323,10 @@ A set of messages $M$ that does not contain equivocating messages is called _cle ``` * `StrongQuorumValue(M)` * Returns $v$ if $\texttt{HasStrongQuorumValue}(M)$ holds, $nil$ otherwise. -* `LowestTicketProposal(M)` +* `GreatestTicketProposal(M)` * Let $M$ be a clean set of CONVERGE messages for the same round. * If $M = ∅$, the predicate returns $baseChain$. - * If $M \ne ∅$, the predicate returns $m.value$ and $m.evidence$, such that $m$ is the message in $M$ with the lowest ticket ($m.ticket$). M will never be empty as the participant must at least deliver its own CONVERGE message. + * If $M \ne ∅$, the predicate returns $m.value$ and $m.evidence$, such that $m$ is the message in $M$ with the greatest ticket after adjusting for the power of the sender ($m.ticket*m.sender.power$). M will never be empty as the participant must at least deliver its own CONVERGE message. * `Aggregate(M)` * Where $M$ is a clean set of messages of the same type $T$, round $r$, and instance $i$, with $v=\texttt{StrongQuorumValue}(M)≠nil$. @@ -369,7 +369,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: until timeout expires 20: prepareReadyToSend ← False 21: while (not prepareReadyToSend){ -22: value, evidence ← LowestTicketProposal(M) \* leader election +22: value, evidence ← GreatestTicketProposal(M) \* leader election 23: if (evidence is a strong quorum of PREPAREs AND mightHaveBeenDecided(value, r-1)): 24: C ← C ∪ {value} 25: if (value ∈ C) @@ -713,7 +713,7 @@ Because of changes to the EC fork choice rule, this FIP requires a network upgra - EB: the common input is decided in the first round. - \>⅔ QAP send QUALITY messages for some chain $c$, while the rest for some chain $c'$ ($c$ and $c'$ only share $baseChain$ as common prefix). After sending QUALITY messages, participants that sent $c$ and that hold <⅓ QAP crash. - EB: $c$ is decided (participants that sent $c'$ swayed to $c$) in the first round. - - Same setup as the test with [three different partitions](#three-partitions), but participants holding less than ⅓ QAP in Q crash after sending QUALITY. One more participant (still in total <⅓ QAP), holding the lowest ticket, crashes in the second round right after sending its CONVERGE. + - Same setup as the test with [three different partitions](#three-partitions), but participants holding less than ⅓ QAP in Q crash after sending QUALITY. One more participant (still in total <⅓ QAP), holding the greatest ticket, crashes in the second round right after sending its CONVERGE. - EB: the chain voted by the crashed participant (i.e., $c'$) is decided. * Crash-recovery: - Repeat tests and their EB when, at a given moment, all participants crash and recover (can be done on smaller scales) @@ -722,7 +722,7 @@ Because of changes to the EC fork choice rule, this FIP requires a network upgra - Three partitions, $F$ holding <⅓ QAP, $P$ and $Q$ holding the rest of QAP (with $P$ holding more QAP than $Q$). Participants in $P$ do not receive messages from $Q$ timely, and vice versa, in the first round. Participants in $F$ send QUALITY for $c$ to $P$ and QUALITY for $c'$ to _P'_. They do the same with PREPARE, PROPOSE, COMMIT. Synchrony is restored in round 2. - EB: in the first round, participants in $P$ decide $c$. Participants in $Q$ go to round 2, where they also decide $c$. Participants in $F$ are detected as equivocating by $p$ and $Q$ eventually. - Same setup as the test with [three different partitions](#three-partitions), but participants holding just less than ⅓ QAP in $Q$ equivocate after sending QUALITY by sending PREPARE and PROPOSE for $c$ to $P$ and for $c'$ to honest participants in $Q$ and $T$. - - EB: honest participants in $Q$ and $T$ decide $c'$ in the first round. Once synchrony is restored in the second round, participants in $P$ decide $c'$ too (perhaps subject to the lower ticket being held by non-Byzantine). + - EB: honest participants in $Q$ and $T$ decide $c'$ in the first round. Once synchrony is restored in the second round, participants in $P$ decide $c'$ too (perhaps subject to the greatest ticket being held by non-Byzantine). - Flooding messages for future instances/rounds - Participants holding <⅓ QAP keep sending QUALITY and PREPARE messages for future rounds/instances (as they do not require evidence), intending to flood memory. - EB: the system can handle buffering a large load of future messages. From e03abda574ad8756ed7afb791e66d19d3405c2f6 Mon Sep 17 00:00:00 2001 From: Alejandro Ranchal-Pedrosa Date: Thu, 11 Apr 2024 12:03:51 +0200 Subject: [PATCH 19/19] Specify no need to store equivocating messages. --- FIPS/fip-0086.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 2387947e..f05f2bd8 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -294,7 +294,7 @@ The receiver of a message only considers messages with valid signatures and disc Two (or more) messages $m1$ and $m2$ are called _equivocating messages_ if $m1.Sender=m2.Sender \land m1.Instance=m2.Instance \land m1.Value ≠ m2.Value \land m1.MsgType=m2.MsgType \land \texttt(if applicable)\ m1.Round=m2.Round$. We call $m1.Sender$ an _equivocating sender_. -A set of messages $M$ that does not contain equivocating messages is called _clean_. Participants discard all equivocating messages when forming clean sets. +A set of messages $M$ that does not contain equivocating messages is called _clean_. Participants discard all equivocating messages when forming clean sets. In fact, in the proposed version of GossiPBFT in this document, only one of the equivocating messages needs to be stored (thanks to evidences explicitly validating a message). #### Predicates and functions used in the protocol