FIP-0086: Changes from 1st Audit #985

ranchalp · 2024-04-08T16:36:45Z

Draft for the moment. Track changes here.

Remove redundant clause

…er pseudocodes)

FIPS/fip-0086.md

anorth

Content LGTM

anorth · 2024-04-11T19:26:40Z

FIPS/fip-0086.md

+ValidEvidence(m= <step, value, instance, round, evidence, ticket>):
+
+if ( step = PREPARE and round = 0)				| in the first round,
+  AND (evidence = nil) 						            | evidence for PREPARE


Alignment of | is broken here.

Thanks, addressed.

anorth · 2024-04-11T19:29:08Z

FIPS/fip-0086.md

+      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


This case value = bottom already handled at 480, so should be impossible here (or the message has evidence that it shouldn't)

Thanks, addressed.

ranchalp · 2024-04-12T09:27:27Z

Resolved conflicts

jsoares · 2024-04-12T22:16:09Z

FIPS/fip-0086.md

-7:    evidence ← nil   \* used to communicate optional evidence for the voted value
+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}

 8:    while (not decideSent)  {


Suggested change

8: while (not decideSent) {

8: while (NOT decideSent) {

not and NOT seem to be inconsistently used throughout the pseudocode. Either is fine, I'd probably go with all caps for consistency with other logical operators.

Fixed in the latest commit, rejected here.

jsoares · 2024-04-12T22:24:25Z

FIPS/fip-0086.md

+ValidEvidence(m= <step, value, instance, round, evidence, ticket>):
+
+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 (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 


The alignment is pretty broken when rendered. Likely a consequence of the mix of space- and tab-based indentation; would be best to go all space as in the previous version. Tabs also show elsewhere in the doc, so maybe configure your editor accordingly.

I think you meant in the previous block of pseudocode? My rendered version looks fine here. The fix for the previous block of pseudocode was a combination of indents and whitespaces (as a result of the font not being monospace, due to special symbols like 丄 taking more width). If that is what it was, fixed.

jsoares · 2024-04-12T22:27:42Z

FIPS/fip-0086.md

@@ -729,7 +754,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.


Suggested change

* **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.

Not something you changed now, but I think we should refer to the 900 epochs as a parameter/setting rather than an estimate.

Fixed in the latest commit (in batch with your other comments and suggestions), rejected here.

jennijuju · 2024-04-13T22:40:36Z

editorial review ✅

anorth and others added 7 commits March 26, 2024 12:37

FIP-0086 Propagate some implementation decisions back to the spec.

72e0487

Removed weak quorum

6b25bc6

Review responses.

eb13a13

Update valid(m) function

f3e8733

Update fip-0086.md

7de7bba

Remove redundant clause

First round of changes from Guy's first Audit

d91afeb

Merge branch 'master' into ranchalp-audit-1

e27cfa4

jsoares changed the title ~~Changes from 1st Audit~~ FIP-0086: Changes from 1st Audit Apr 9, 2024

ranchalp added 7 commits April 9, 2024 14:09

Update GossiPBFT Pseudocode (TODO still update line numbering and oth…

61d48e5

…er pseudocodes)

Update references to line numbers

9b26e5e

Fix typos (code statements, indenting)

24f6327

Fix valid(m) and validEvidence(m)

56c8106

Fix DECIDE format

c6e32b4

Update fip-0086.md

2974f70

Changes from 2nd audit by Guy

b9c1db2

ranchalp mentioned this pull request Apr 11, 2024

FIP-0086: Using max ticket #987

Merged

masih reviewed Apr 11, 2024

View reviewed changes

FIPS/fip-0086.md Outdated Show resolved Hide resolved

FIPS/fip-0086.md Outdated Show resolved Hide resolved

FIPS/fip-0086.md Outdated Show resolved Hide resolved

FIPS/fip-0086.md Outdated Show resolved Hide resolved

ranchalp added 2 commits April 11, 2024 18:03

Make C a globally scoped variable and update line numbering

5dab603

Small fix

57f13f8

anorth reviewed Apr 11, 2024

View reviewed changes

ranchalp added 2 commits April 12, 2024 11:24

Fix couple comments

1fcce20

Merge branch 'master' into ranchalp-audit-1

4113980

ranchalp marked this pull request as ready for review April 12, 2024 09:27

ranchalp requested review from momack2, arajasek, jennijuju, kaitlin-beegle, raulk and jsoares as code owners April 12, 2024 09:27

ranchalp requested a review from TippyFlitsUK as a code owner April 12, 2024 09:27

jsoares approved these changes Apr 12, 2024

View reviewed changes

jennijuju approved these changes Apr 13, 2024

View reviewed changes

Typos and indentation fixes

daccc3f

anorth approved these changes Apr 16, 2024

View reviewed changes

anorth merged commit 6aea945 into filecoin-project:master Apr 16, 2024
1 check passed

This was referenced Apr 22, 2024

Implement changes from 1st protocol audit filecoin-project/go-f3#170

Closed

FIP-0086 Audit final changes #996

Merged

ranchalp mentioned this pull request May 7, 2024

FIP-0086 Include message-rebroadcast and skipping rounds #998

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

FIP-0086: Changes from 1st Audit #985

FIP-0086: Changes from 1st Audit #985

ranchalp commented Apr 8, 2024

anorth left a comment

anorth Apr 11, 2024

ranchalp Apr 12, 2024

anorth Apr 11, 2024

ranchalp Apr 12, 2024

ranchalp commented Apr 12, 2024

jsoares Apr 12, 2024

ranchalp Apr 15, 2024

jsoares Apr 12, 2024

ranchalp Apr 15, 2024

jsoares Apr 12, 2024

ranchalp Apr 15, 2024

jennijuju commented Apr 13, 2024

FIP-0086: Changes from 1st Audit #985

FIP-0086: Changes from 1st Audit #985

Conversation

ranchalp commented Apr 8, 2024

anorth left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ranchalp commented Apr 12, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jennijuju commented Apr 13, 2024