From c2f1316977093314eef8e3e830a9154fb052614d Mon Sep 17 00:00:00 2001 From: Jeff Burdges Date: Fri, 9 Nov 2018 16:27:42 +0100 Subject: [PATCH 1/2] Appears to be a missing negation in Theorem 4.1 and .. I replaced an "or such that" with "in either case such that" Also some formatting changes --- pdf/grandpa.tex | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/pdf/grandpa.tex b/pdf/grandpa.tex index 8c8dbee..ed964b5 100644 --- a/pdf/grandpa.tex +++ b/pdf/grandpa.tex @@ -244,32 +244,35 @@ If we receive a valid commit message for $B$ for round $r$, then it contains eno \subsection{ Accountable Safety} -The first thing we want to show is asynchronous safety if we have at most $f$ Byzantine validators: +The first thing we want to show is asynchronous safety, assuming we have at most $f$ Byzantine validators. -\begin{theorem} If the protocol finalises any two blocks $B,B'$ that have valid commit messages sent are on the same chain, then there are at least $f+1$ Byzantine voters who all voted in a particular vote. Furthermore, there is a synchronous procedure to find such a set. +\begin{theorem} If the protocol finalises any two blocks $B,B'$ for which valid commit messages were sent, but which do not lie on the same chain, then there are at least $f+1$ Byzantine voters who all voted in a particular vote. Furthermore, there is a synchronous procedure to find some such of $f+1$ Byzantine voters. \end{theorem} -The challenge procedure works as follows: If $B$ and $B'$ are committed in the same round, then the union of their precommits must contain at least $f$ equivocations, so we are done. Otherwise $B$ was committed in round $r$ and $B'$ in round $r' > r$ say. Then we ask the at least $n-f$ validators who precomitted $\geq B'$ in round $r$ in the commit message, why they precomitted. +The challenge procedure works as follows: If $B$ and $B'$ are committed in the same round, then the union of their precommits must contain at least $f$ equivocations, so we are done. Otherwise, we may assume by symmetry that $B$ was committed in round $r$ and $B'$ in round $r' > r$. There are at least $n-f$ validators who precomitted $\geq B'$ in round $r$ in their commit messages, so we ask them why they precomitted. We ask queries of the following form: - -- Why was $E_{r''-1} \not\geq B$ when you prevoted for or precomitted to $B'' \not\geq B$ in round $r'' > r$? - -Which any honest validator should be able to respond to as is shown in Lemma \ref{lem:honest-answer} below. +\begin{itemize} +\item Why was $E_{r''-1} \not\geq B$ when you prevoted for or precomitted to $B'' \not\geq B$ in round $r'' > r$? +\end{itemize} + +Any honest validator should be able to respond to this, as is shown in Lemma \ref{lem:honest-answer} below. The response is of the following form: +\begin{itemize} +\item A either a set $S$ of prevotes for round $r''-1$, or else a set $S$ of precommits for round $r''-1$, in either case such that it is impossible for $S$ to have a supermajority for $B$. +\end{itemize} -- A either a set $S$ of prevotes for round $r''-1$ or a set $S$ of precommits for round $r''-1$ or such that it is impossible for $S$ to have a supermajority for $B$. +If no validator responds, then we have $n-f$ Byzantine validators. If any do, then if $r'' > r+1$, we can ask the same query for at least $n-f$ validators in round $r''-1$. -If no validator responds, then we have $n-f$ Byzantine validators. If any do, then if $r'' > r+1$, we can ask the same query for $n-f$ validators in round $r''-1$. - -If any responded and $r''=r+1$, then we have either a set $S$ of prevotes or precommits in round $r$ that it is impossible for $S$ to have a supermajority for $B$ in round $r$. +If any responded and $r''=r+1$, then we have either a set $S$ of prevotes or precommits in round $r$ that show it is impossible for $S$ to have a supermajority for $B$ in round $r$. If $S$ is a set of precommits, then if we take the union of $S$ and the set of precommits in the commit message for $B$, then the resulting set of precommits for round $r$ has a supermajority for $B$ and it is impossible for it to have a supermajority for $B$. This is possible if the set is not tolerant and so there must be at least $f+1$ voters who equivocate an so are Byzantine. If we get a set $S$ of prevotes for round $r$ that does not have a supermajority for $B$, then we need to ask a query of the form - -- Which prevotes for round $r$ have you seen? +\begin{itemize} +\item Which prevotes for round $r$ have you seen? +\end{itemize} to all the voters of precommit in the commit message for $B$ who voted for blocks $B'' \geq B$. There must be $n-f$ such validators and a valid response to this query is a set $T$ of prevotes for round $r$ with a supermajority for $B''$ and so a supermajority for $B$. From 9fe0b4adb0e2271de7055f717a40f08b1d0b8980 Mon Sep 17 00:00:00 2001 From: Jeff Burdges Date: Fri, 9 Nov 2018 16:48:35 +0100 Subject: [PATCH 2/2] Add a set X for explicitly finding the Byzantine validators --- pdf/grandpa.tex | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/pdf/grandpa.tex b/pdf/grandpa.tex index ed964b5..49c789b 100644 --- a/pdf/grandpa.tex +++ b/pdf/grandpa.tex @@ -246,7 +246,7 @@ If we receive a valid commit message for $B$ for round $r$, then it contains eno The first thing we want to show is asynchronous safety, assuming we have at most $f$ Byzantine validators. -\begin{theorem} If the protocol finalises any two blocks $B,B'$ for which valid commit messages were sent, but which do not lie on the same chain, then there are at least $f+1$ Byzantine voters who all voted in a particular vote. Furthermore, there is a synchronous procedure to find some such of $f+1$ Byzantine voters. +\begin{theorem} If the protocol finalises any two blocks $B,B'$ for which valid commit messages were sent, but which do not lie on the same chain, then there are at least $f+1$ Byzantine voters who all voted in a particular vote. Furthermore, there is a synchronous procedure to find some such set $X$ of $f+1$ Byzantine voters. \end{theorem} The challenge procedure works as follows: If $B$ and $B'$ are committed in the same round, then the union of their precommits must contain at least $f$ equivocations, so we are done. Otherwise, we may assume by symmetry that $B$ was committed in round $r$ and $B'$ in round $r' > r$. There are at least $n-f$ validators who precomitted $\geq B'$ in round $r$ in their commit messages, so we ask them why they precomitted. @@ -255,17 +255,16 @@ We ask queries of the following form: \begin{itemize} \item Why was $E_{r''-1} \not\geq B$ when you prevoted for or precomitted to $B'' \not\geq B$ in round $r'' > r$? \end{itemize} - -Any honest validator should be able to respond to this, as is shown in Lemma \ref{lem:honest-answer} below. +\noindent Any honest validator should be able to respond to this, as is shown in Lemma \ref{lem:honest-answer} below. The response is of the following form: \begin{itemize} \item A either a set $S$ of prevotes for round $r''-1$, or else a set $S$ of precommits for round $r''-1$, in either case such that it is impossible for $S$ to have a supermajority for $B$. \end{itemize} -If no validator responds, then we have $n-f$ Byzantine validators. If any do, then if $r'' > r+1$, we can ask the same query for at least $n-f$ validators in round $r''-1$. +We consider any non-responsive validator to be Byzantine and add them to the set $X$. In particular, if no validator responds, then we have $n-f$ Byzantine validators. If any do, then if $r'' > r+1$, we can ask the same query for at least $n-(f - |X|)$ validators in round $r''-1$, . -If any responded and $r''=r+1$, then we have either a set $S$ of prevotes or precommits in round $r$ that show it is impossible for $S$ to have a supermajority for $B$ in round $r$. +If any validators respond when $r''=r+1$, then we have either a set $S$ of prevotes or precommits in round $r$ that show it is impossible for $S$ to have a supermajority for $B$ in round $r$. If $S$ is a set of precommits, then if we take the union of $S$ and the set of precommits in the commit message for $B$, then the resulting set of precommits for round $r$ has a supermajority for $B$ and it is impossible for it to have a supermajority for $B$. This is possible if the set is not tolerant and so there must be at least $f+1$ voters who equivocate an so are Byzantine. @@ -273,8 +272,7 @@ If we get a set $S$ of prevotes for round $r$ that does not have a supermajority \begin{itemize} \item Which prevotes for round $r$ have you seen? \end{itemize} - -to all the voters of precommit in the commit message for $B$ who voted for blocks $B'' \geq B$. There must be $n-f$ such validators and a valid response to this query is a set $T$ of prevotes for round $r$ with a supermajority for $B''$ and so a supermajority for $B$. +\noindent to all the voters of precommit in the commit message for $B$ who voted for blocks $B'' \geq B$. There must be $n-f$ such validators and a valid response to this query is a set $T$ of prevotes for round $r$ with a supermajority for $B''$ and so a supermajority for $B$. If any give a valid response, by a similar argument to the above, $S \cup T$ will have $f+1$ equivocations.