diff --git a/Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex b/Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex index 6275f04..bd56323 100644 --- a/Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex +++ b/Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex @@ -66,6 +66,10 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB } \end{algorithm} + +\paragraph{Algorithm intuition.} +The crash-tolerant algorithm is organized around round closure and winner extraction. By \Cref{def:closed-round,def:first-append,lem:closure-view,lem:winners}, once a round is closed, every correct process eventually reads the same winner set $\Winners_r$. By \Cref{lem:nonempty}, this set is never empty, and by \Cref{lem:winners-propose} every winner has necessarily sent its proposal to all processes before becoming a winner, exactly because sending precedes $\PROVE(r)$ and $\APPEND(r)$ at line~\ref{code:submit-proposition}. Under reliable channels, these winner proposals are eventually received by every correct process, so the waiting condition at line~\ref{code:check-winners-ack} eventually becomes true, which is formalized by \Cref{lem:eventual-closure}. Then, by \Cref{lem:convergence}, all correct processes compute the same set $M$ at line~\ref{code:Mcompute-dl}, and because line~\ref{code:next-msg-extraction} applies the same deterministic ordering function, they append messages in the same order; this is exactly the core mechanism later used in \Cref{lem:validity,lem:no-duplication,lem:total-order}. + \subsection{Correctness} \begin{definition}[First APPEND]\label{def:first-append} diff --git a/Recherche/BFT-ARBover/5_BFT_ARB/index.tex b/Recherche/BFT-ARBover/5_BFT_ARB/index.tex index 5569516..a2c17b4 100644 --- a/Recherche/BFT-ARBover/5_BFT_ARB/index.tex +++ b/Recherche/BFT-ARBover/5_BFT_ARB/index.tex @@ -1,15 +1,15 @@ \subsection{Model extension} -We consider a static set $\Pi$ of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable. At most $f$ processes may be Byzantine, and we assume $n > 3f$. +We extend the crash model of Section 1 (same process universe, asynchronous setting, uniquely identifiable messages, and reliable point-to-point channels) with Byzantine faults and Byzantine-resilient dissemination primitives. -\paragraph{Synchrony.} The network is asynchronous. +\paragraph{Failure threshold.} At most $t$ processes may be Byzantine, and we assume $n > 3t$. -\paragraph{Communication.} Processes can exchange through a Reliable Broadcast ($\RB$) primitive (defined below) which is invoked with the functions $\RBcast(m)$ and $m = \rbreceived()$. The Reliable Broadcast is a Byzantine fault-tolerant primitive following Bracha's specification \cite{Bracha1987}: for any message $m$ broadcast by a process $p_j$, every correct process either receives the message $m$ or none at all; moreover, all correct processes that receive a broadcast from $p_j$ for a given sequence number or round receive exactly the same message. This ensures that Byzantine processes cannot send different messages to different correct processes for the same broadcast instance. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$. +\paragraph{Additional communication primitive.} In addition to reliable point-to-point channels, processes use Reliable Broadcast ($\RB$) with operations $\RBcast(m)$ and $m=\rdeliver()$. We use Bracha's Byzantine RB specification (1987): for a fixed sender and broadcast instance, all correct processes that deliver, deliver the same payload, and Byzantine equivocation on that instance is prevented. \paragraph{Byzantine behaviour} -A process is said to exhibit Byzantine behaviour if it deviates arbitrarily from the prescribed algorithm. Such deviations may, for instance, consist in invoking primitives ($\RBcast$, $\APPEND$, $\PROVE$, etc.) with invalid inputs or inputs crafted maliciously, colluding with other Byzantine processes in an attempt to manipulate the system state or violate its guarantees, deliberately delaying or accelerating the delivery of messages to selected nodes so as to disrupt the expected timing of operations, or withholding messages and responses in order to induce inconsistencies in the system state. +A Byzantine process may deviate arbitrarily from the algorithm (malformed inputs, selective omission, collusion, inconsistent timing, etc.). -Byzantine processes are constrained by the following. They cannot forge valid cryptographic signatures or threshold shares without access to the corresponding private keys. They cannot violate the termination, validity, or anti-flickering properties of the $\DL$ object. They also cannot break the integrity, no-duplicates, or validity properties of the $\RB$ primitive. +Byzantine processes are still constrained by the assumed primitives: they cannot violate the safety/liveness guarantees of $\DL$ and cannot break the Integrity, No-duplicates, and Validity guarantees of $\RB$. \paragraph{Notation.} For any indice $k$ we defined by $\DL[k]$ as the $k$-th DenyList object. For a given $\DL[k]$ and any indice $x$ we defined by $\Pi_x^k$ a subset of $\Pi$. Still for a given $k$ we consider $\Pi_M^k \subseteq \Pi$ and $\Pi_V^k \subseteq \Pi$ two authorization subsets for $\DL[k]$. Indice $i \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec_k$ for the $\DL[k]$ linearization: $x \prec_k y$ means that operation $x$ appears strictly before $y$ in the linearized history of $\DL[k]$. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes). @@ -18,6 +18,15 @@ For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked % ------------------------------------------------------------------------------ \subsection{Primitives} +\subsection{Reliable Broadcast (RB)} + +\RB provides the following properties in the model. +\begin{itemize}[leftmargin=*] + \item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ m = \rbreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$. + \item \textbf{No-duplicates}: No message is received more than once at any process. + \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$. +\end{itemize} + \subsubsection{t-BFT-DL} We consider a t-Byzantine Fault Tolerant DenyList (t-$\BFTDL$) with the following properties. @@ -83,6 +92,9 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au } \end{algorithm} +\paragraph{Algorithm intuition.} +In the Byzantine setting, a process identifier $j$ is selected in $\winners[r]$ only when it accumulates at least $t+1$ proofs for round $r$ in $\validated(r)$. A process emits such a proof for $j$ only after receiving $j$'s $\texttt{PROP}$ payload (handler $\rdeliver(\texttt{PROP},\cdot)$). Therefore, if $j$ is a winner, at least one correct process has received $j$'s proposal. By RB agreement/validity, once one correct process receives that proposal for the instance, all correct processes eventually receive the same payload, so winner proposals eventually become available everywhere and can be merged consistently. + \begin{lemma}[BFT-PROVE Validity]\label{lem:bft-prove-validity} The invocation of $op = \BFTPROVE(x)$ by a correct process is invalid iff there exist at least $t+1$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$. \end{lemma} @@ -253,6 +265,9 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au \end{algorithm} +\paragraph{Algorithm intuition.} +The Byzantine-tolerant construction combines threshold evidence and RB agreement to make winner selection robust. A sender $j$ appears in $\validated(r)$ only when at least $t+1$ proofs for $\langle j,r\rangle$ are observed through $\BFTREAD()$, and by \Cref{lem:bft-prove-validity} this threshold means that $j$ cannot be certified without broad enough support from the system. Once a round is closed, the winner set becomes stable by \Cref{lem:winners-stability}, so correct processes stop diverging on who contributes to the round outcome. For each stable winner, the associated proposal payload is unique at correct receivers by \Cref{lem:bft-unique-proposal}, which prevents equivocation from creating distinct local values for the same winner identity. Consequently, when correct processes wait for all winner proposals and compute the union at line~\ref{code:Mcompute}, they obtain the same message set by \Cref{lem:message-content-invariance}. Progress is then ensured by \Cref{lem:bft-eventual-closure}, which guarantees that if new messages remain unordered, a new round eventually closes with at least $n-t$ winners. Finally, once rounds are commonly closed, appending $\order(M)$ at each round yields a common delivery sequence, exactly formalized by \Cref{lem:bft-total-order}. + % \textbf{Everything below has to be updated} % \begin{definition}[BFT Closed round for $k$] @@ -422,7 +437,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au By strong induction, if round $r$ is closed, all rounds $r_1 < r$ are closed. \end{proof} -\begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:unique-proposal} +\begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:bft-unique-proposal} For any closed round $r$ and any process $p_j \in \winners[r]$, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process $p_i$ that has received a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly this set $S_j$. \end{lemma} @@ -433,7 +448,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au Since at least $t+1$ distinct processes have performed a valid $\BFTPROVE(\langle j, r \rangle)$, and since $t < n/3$, at least one of these processes is correct. Thus, at least one correct process must have received a reliable broadcast from $p_j$ for round $r$. - Now, by Bracha's Byzantine Reliable Broadcast specification \cite{Bracha1987}, for any message broadcast instance by process $p_j$ in round $r$, all correct processes that deliver this broadcast either receive the identical message or none at all. Formally, for all correct processes $p_i, p_i'$ that received a delivery from $p_j$ for round $r$, we have $S_j^{(i)} = S_j^{(i')}$. + Now, by Bracha's Byzantine Reliable Broadcast specification, for any message broadcast instance by process $p_j$ in round $r$, all correct processes that deliver this broadcast either receive the identical message or none at all. Formally, for all correct processes $p_i, p_i'$ that received a delivery from $p_j$ for round $r$, we have $S_j^{(i)} = S_j^{(i')}$. Therefore, there exists a unique set $S_j$ such that every correct process $p_i$ that receives a reliable delivery from $p_j$ for round $r$ receives exactly $S_j$. \end{proof} @@ -473,7 +488,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au By \cref{lem:winners-stability}, the set $\winners[r]$ is stable once round $r$ is closed. Therefore, both $p_i$ and $p_{i'}$ compute the same set of winners $\winners[r]$. - Now, consider any winner $j \in \winners[r]$. By \cref{lem:unique-proposal}, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process that receives a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly $S_j$. + Now, consider any winner $j \in \winners[r]$. By \cref{lem:bft-unique-proposal}, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process that receives a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly $S_j$. By the algorithm, each correct process stores this received set in its local variable: $\prop^{(i)}[r][j] = S_j$ and $\prop^{(i')}[r][j] = S_j$. @@ -485,7 +500,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au Therefore, all correct processes compute the same set $M$ for any closed round $r$. \end{proof} -\begin{lemma}[Inclusion]\label{lem:inclusion} +\begin{lemma}[Inclusion]\label{lem:bft-inclusion} If a correct process $p_i$ invokes $\ABbroadcast(m)$, then there exist a closed round $r$ and a winner $j \in \winners[r]$ such that $p_j$ invoked $\RBcast(j, \texttt{PROP}, S, r)$ with $m \in S$. \end{lemma} @@ -507,14 +522,38 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au Since $n > 3f$, we have $n - t > t + 1 > f$. By the pigeonhole principle, there eventually exists a round $r$ where at least $n - t$ distinct processes have proposed sets containing $m$. Since more than $2f$ processes have proposed $m$, at least one of them must be correct and be elected as a winner. Therefore, there exist a round $r$ and a winner $j \in \winners[r]$ such that $m \in S_j$ was broadcast by $p_j$. \end{proof} -\begin{lemma}[Eventual Closure]\label{lem:eventual-closure} +\begin{lemma}[Eventual Closure]\label{lem:bft-eventual-closure} For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$. \end{lemma} -\begin{lemma}[Total Order]\label{lem:total-order} +\begin{proof} + Let $p_i$ be a correct process such that $\unordered \setminus \ordered \neq \emptyset$ after round $r$ is the highest closed round it observed. By the main loop of Algorithm~\ref{alg:bft-arb}, $p_i$ eventually enters round $r+1$, computes $S=\unordered\setminus\ordered$, and invokes $\RBcast(\texttt{PROP},S,\langle i,r+1\rangle)$. + + By RB Validity, every correct process eventually $\rdeliver(\texttt{PROP},S,\langle i,r+1\rangle)$. Upon this delivery, each correct process executes $\BFTPROVE(\langle i,r+1\rangle)$. Hence at least $n-t$ correct processes issue a proof for candidate $i$ in round $r+1$, and in particular the threshold $t+1$ used in $\validated(r+1)$ is eventually met for that candidate. + + The same argument applies to each correct process that broadcasts in round $r+1$: once its proposal is RB-delivered, at least $n-t$ correct processes issue the corresponding proofs, so that sender is eventually included in $\validated(r+1)$. Since there are at least $n-t$ correct processes, eventually $|\validated(r+1)| \geq n-t$, and the wait at line~\ref{alg:check-validated} is eventually released for every correct process in that round. + + After this point, each correct process executes the $\BFTAPPEND$ loop (line~\ref{alg:append}) and sends $\texttt{DONE}$ to all processes. By reliability of point-to-point channels, every correct process eventually receives at least $n-t$ DONE messages, so the wait at line~\ref{alg:check-done} is also eventually released. At that moment, the process computes $\winners[r+1] \gets \validated(r+1)$, and by the previous bound we have $|\winners[r+1]| \geq n-t$. + + Therefore round $r+1$ eventually becomes closed with at least $n-t$ winners. +\end{proof} + +\begin{lemma}[Total Order]\label{lem:bft-total-order} For any two correct processes $p_i$ and $p_j$, the sequence $\ordered$ maintained locally by $p_i$ and the sequence maintained by $p_j$ contain the same messages in the same order, provided that both have reached the same set of closed rounds. \end{lemma} +\begin{proof} + We prove the claim by induction on the number of closed rounds completed by both processes. + + \textbf{Base case.} Before any closed round is completed, both local sequences are initialized to $\epsilon$, hence identical. + + \textbf{Induction step.} Assume that after all closed rounds up to $r-1$, processes $p_i$ and $p_j$ have identical $\ordered$ prefixes. Consider round $r$. + + By \Cref{lem:winners-stability}, once round $r$ is closed, both processes use the same stable winner set $\winners[r]$. By \Cref{lem:message-content-invariance}, the set $M$ computed at line~\ref{code:Mcompute} is identical at all correct processes for that round. Both processes then apply the same deterministic ordering function $\order(M)$ and append that same ordered block to their current sequence. + + Since they started round $r$ from identical prefixes and append the same ordered suffix for round $r$, their resulting sequences after round $r$ are identical. The induction concludes that for any common set of closed rounds, both correct processes maintain the same messages in the same order. +\end{proof} + \begin{theorem} The algorithm implements a BFT Atomic Reliable Broadcast. \end{theorem} diff --git a/Recherche/BFT-ARBover/main.pdf b/Recherche/BFT-ARBover/main.pdf index 938b244..2076911 100644 Binary files a/Recherche/BFT-ARBover/main.pdf and b/Recherche/BFT-ARBover/main.pdf differ