Skip to content
A MILP Model for Failures and Attacks on a BFT Blockchain Protocol
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
MILP_BFTConsensus.mod
README.md

README.md

A MILP Model for Failures and Attacks on a BFT Blockchain Protocol

We present a MILP model for failures and attacks on a BFT blockchain protocol.

Parameters

  • [{$i \in R$}:] consensus replica $i$ from set of replicas $R$. $R^{BYZ}$ is byzantine set. $R^{OK}$ is non-byzantine set. $R = R^{OK} \cup R^{BYZ}$, such that $R^{OK} \cap R^{BYZ} = \emptyset$.
  • [$f$:] number of faulty/Byzantine replicas. $f = |R^{BYZ}|$.
  • [$N$:] total number of replicas. $N = |R| = |R^{OK}| + |R^{BYZ}| = 3f + 1$.
  • [$M$:] safety level. $M = 2f + 1$.
  • [{$b \in B$}:] block $b$ from set of possible proposed blocks $B$ (may be understood as block hash). $B = {b_0, b_1, b_2, \cdots }$.
  • [{$h \in H$}:] height $h$ from set of possible heights $H$ (tests may only require two or three heights). $H = {h_0, h_1, h_2}$.
  • [{$v \in V$}:] view $v$ from set of possible views $V$ (number of views may be limited to the number of consensus nodes $N$). $V = {v_0, v_1, \cdots , v_{N-1}}$
  • [{$t \in T$}:] time unit $t$ from set of discrete time units $T$. $T = {t_0, t_1, t_2, \cdots }$.

Variables

  • [{$primary_{i,h,v}$}:] binary variable that indicates if Consensus Node $i$ is primary at height $h$ view $v$.
  • [$initialized^{t}_{i, h, v}$:] binary variable that indicates if replica $i \in R$ is at height $h$ and view $v$, on time $t$
  • [$SendPrepReq^{t}_{i, h, b, v}$:] binary variable that indicates if replica $i \in R$ is sending Prepare Request message (to all nodes) at height $h$ and view $v$, on time $t$, for proposed block $b$. ACTION VARIABLE MUST BE SET ONLY ONCE FOR EVERY REPLICA, HEIGHT AND BLOCK.
  • [$SendPrepResp^{t}_{i, h, b, v}$:] binary variable that indicates if replica $i \in R$ is sending Prepare Response message (to all nodes) at height $h$ and view $v$, on time $t$, for proposed block $b$. ACTION VARIABLE MUST BE SET ONLY ONCE FOR EVERY REPLICA, HEIGHT AND BLOCK.
  • [$RecvPrepReq^{t}_{i, j, h, b, v}$:] binary variable that indicates if replica $i \in R$ received a Prepare Request message from replica $j$ at height $h$ and view $v$, on time $t$, for proposed block $b$. ACTION VARIABLE MUST BE SET ONLY ONCE FOR EVERY REPLICA, HEIGHT AND BLOCK.
  • [$RecvPrepResp^{t}_{i, j, h, b, v}$:] binary variable that indicates if replica $i \in R$ received a Prepare Response message from replica $j$ at height $h$ and view $v$, on time $t$, for proposed block $b$. ACTION VARIABLE MUST BE SET ONLY ONCE FOR EVERY REPLICA, HEIGHT AND BLOCK.
  • [{$BlockRelay^t_{i, h, b}$}:] binary variable that indicates if replica $i$ has relayed block $b$ at height $h$, on time $t$. ACTION VARIABLE MUST BE SET ONLY ONCE FOR EVERY REPLICA, HEIGHT AND BLOCK.
  • [$RecvBlkPersist^{t}_{i, j, h, b}$:] binary variable that indicates if replica $i \in R$ received a Block Relay message from replica $j$ at height $h$ on time $t$, for proposed block $b$. ACTION VARIABLE MUST BE SET ONLY ONCE FOR EVERY REPLICA, HEIGHT AND BLOCK.
  • [$sentPrepReq^{t}_{i, h, b, v}$:] binary variable that indicates if replica $i \in R$ has sent (in past) to all replicas a Prepare Request message at height $h$ and view $v$, on time $t$, for proposed block $b$. Once set to ONE this is carried forever as ONE.
  • [$sentPrepResp^{t}_{i, h, b, v}$:] binary variable that indicates if replica $i \in R$ has sent (in past) to all replicas a Prepare Response message at height $h$ and view $v$, on time $t$, for proposed block $b$. Once set to ONE this is carried forever as ONE.
  • [$recvdPrepReq^{t}_{i, j, h, b, v}$:] binary variable that indicates if replica $i \in R$ has received (in past) from replica $j$ a Prepare Request message at height $h$ and view $v$, on time $t$, for proposed block $b$. Once set to ONE this is carried forever as ONE.
  • [$recvdPrepResp^{t}_{i, j, h, b, v}$:] binary variable that indicates if replica $i \in R$ has received (in past) from replica $j$ a Prepare Response message at height $h$ and view $v$, on time $t$, for proposed block $b$. Once set to ONE this is carried forever as ONE.
  • [$sentBlkPersist^{t}_{i, h, b}$:] binary variable that indicates if replica $i \in R$ has sent (in past) to all replicas a Block Relay message at height $h$, on time $t$, for proposed block $b$. Once set to ONE this is carried forever as ONE. % Nao se assumi que um byzantine poderia dar dois relays diferentes em views distintos?
  • [$recvdBlkPersist^{t}_{i, j, h, b}$:] binary variable that indicates if replica $i \in R$ has received (in past) from replica $j$ a Block Relay message at height $h$, on time $t$, for proposed block $b$. Once set to ONE this is carried forever as ONE.
  • [{$blockRelayed_{b}$}:] binary variable that indicates if block $b$ was relayed (on any time, height or view).

Objective function

maximize: \sum_{b \in B} blockRelayed_{b}

The adversary can control $f$ replicas, but the other $M$ replicas must follow dBFT algorithm. The adversary can choose any delay for any message (up to maximum simulation time $|T|$). If it wants to shutdown the whole network, no blocks will be ever produced and objective will be zero (minimum possible). So, adversary will try to maximize blocks produced by manipulating delays in a clever way. Objective function is bounded to [$0$, $|B|$].

Constraints

Initialization constraints \begin{align} % initializing all good replicas in time zero, height zero, view zero (Byzantine can start in any configuration) initialized^{t_0}{i, h_0, v_0} = 1 & \qquad \forall i \in R^{OK}\ initialized^{t_0}{i, h, v} = 0 & \qquad \forall i \in R^{OK}, h \in H \setminus {h_0}, v \in V \setminus {v_0}\ %only one view can be initialized at a time \sum_{v \in V} initialized^{t}{i, h, v} = 1 & \qquad \forall i \in R, t \in T \setminus {t_0}, h \in H\ %only one height can be initialized at a time \sum{h \in H} initialized^{t}_{i, h, v} = 1 & \qquad \forall i \in R, t \in T \setminus {t_0}, v \in V \end{align}

Time zero constraints

\begin{align} % cannot prep req on time zero SendPrepReq^{t_0}{i, h, b, v} = 0 & \qquad \forall i \in R, \forall h, b, v\ % sent prep request did not happen on time zero sentPrReq^{t_0}{i, h, b, v} = 0 & \qquad \forall h, b, i, v\ % cannot receive prep req on time zero RecvPrepReq^{t_0}{i, j, h, b, v} = 0 & \qquad \forall i \in R, \forall h, b, v\ % received prep req did not happen on time zero recvdPrReq^{t_0}{i, j, h, b, v} = 0 & \qquad \forall j, h, b, i, v\ % cannot send prep response on time zero SendPrepResp^{t_0}{i, h, b, v} = 0 & \qquad \forall i \in R, \forall h, b, v\ % sent prep response did not happen on time zero sentPrResp^{t_0}{i, h, b, v} = 0 & \qquad \forall h, b, i, v\ % cannot receive prep resp on time zero RecvPrepResp^{t_0}{i, j, h, b, v} = 0 & \qquad \forall i,j \in R, \forall h, b, v\ % received prep resp did not happen on time zero recvdPrResp^{t_0}{i, j, h, b, v} = 0 & \qquad \forall j, h, b, i, v\ % cannot relay block on time zero BlockRelay^{t_0}{i, h, b} = 0 & \qquad \forall i \in R, \forall h, b\ % sent block persist did not happen in time zero sentBlkPersist^{t_0}{i,h,b} = 0 & \qquad \forall i \in R,\forall h, b\ % cannot receive block persist on time zero RecvBlkPersist^{t_0}{i, j, h, b} = 0 & \qquad \forall i, j \in R, \forall h, b\ % received block persist did not happen in time zero recvdBlkPersist^{t_0}{i,j,h,b} = 0 & \qquad \forall i,j \in R,\forall h, b\ \end{align}

Prepare request constraints

\begin{align} % can send prep req only if initialized SendPrepReq^{t}{i, h, b, v} \leq initialized^t{i, h, v} & \qquad \forall i, h, b, v, t\ % can send prep req only if primary SendPrepReq^{t}{i, h, b, v} \leq primary{i, h, v} & \qquad \forall i, h, b, v, t\ % sent prep request from i to j, subject to send i in past time sentPrReq^{t}{i, h, b, v} = sentPrReq^{t-1}{i, h, b, v} + SendPrepReq^{t-1}{i, h, b, v} & \qquad \forall h, b, i, v, t \in T \setminus {t_0}\ % received prep req on i from j, only if sent from j to i (in past time) RecvPrReq^{t}{i, j, h, b, v} \leq sentPrReq^{t}{j, h, b, v} & \qquad \forall h, b, i \neq j, v, t\ % self received prep req RecvPrReq^{t}{i, i, h, b, v} = SendPrepReq^{t}{i, h, b, v} & \qquad \forall h, b, i, v, t\ % if received in past time, keep variable received recvdPrReq^{t}{i, j, h, b, v} = recvdPrReq^{t-1}{i, j, h, b, v} + RecvPrReq^{t-1}{i, j, h, b, v} & \qquad \forall h, b, i, j, v, t \in T \setminus {t_0} \end{align}

Prepare response constraints

\begin{align} % can send prep resp only if initialized SendPrepResp^{t}{i, h, b, v} \leq initialized^t{i, h, v} & \qquad \forall i, h, b, v, t\ % will send prepare response if received any prepare request (OK nodes) 1/N will force up! SendPrepResp^{t}{i, h, b, v} \geq \frac{1}{N}\sum{j \in R} recvdPrReq^{t-1}{i, j, h, b, v} & \qquad \forall i \in R^{OK}, h, b, v, t\ % may send prepare response only if received any prepare request SendPrepResp^{t}{i, h, b, v} \leq \sum_{j \in R} recvdPrReq^{t-1}{i, j, h, b, v} & \qquad \forall i \in R, h, b, v, t\ % sent prep response from i, subject to send i in past time sentPrResp^{t}{i, h, b, v} = sentPrResp^{t-1}{i, h, b, v} + SendPrepResp^{t-1}{i, h, b, v} & \qquad \forall h, b, i, v, t \in T \setminus {t_0}\ % received prep resp on i from j, only if sent from j to i (in past time) RecvPrResp^{t}{i, j, h, b, v} \leq sentPrResp^{t}{j, h, b, v} & \qquad \forall h, b, i \neq j, v, t\ % self received prep resp RecvPrResp^{t}{i, i, h, b, v} = SendPrepResp^{t}{i, h, b, v} & \qquad \forall h, b, i, v, t\ % if received in past time, keep variable received recvdPrResp^{t}{i, j, h, b, v} = recvdPrResp^{t-1}{i, j, h, b, v} + RecvPrResp^{t-1}_{i, j, h, b, v} & \qquad \forall h, b, i, j, v, t \in T \setminus {t_0} \end{align}

Block persist constraints \begin{align} % sent persist message to all, after BlockRelay sentBlkPersist^t_{i,h,b} = sentBlkPersist^{t-1}{i,h,b} + BlockRelay^{t-1}{i,h,b} & \qquad \forall i,j \in R, h, b, t\ % received Block Relay on i from j, only if sent from j to i (in past time) RecvBlkPersist^{t}{i, j, h, b} \leq sentBlkPersist^{t}{j, h, b} & \qquad \forall h, b, i \neq j, v, t\ % self received persist block RecvBlkPersist^{t}{i, i, h, b} = BlockRelay^{t}{i, h, b} & \qquad \forall h, b, i, v, t\ % if received in past time, keep variable received recvdBlkPersist^{t}{i, j, h, b} = recvdBlkPersist^{t-1}{i, j, h, b} + RecvBlkPersist^{t-1}_{i, j, h, b} & \qquad \forall h, b, i, j, t \in T \setminus {t_0} \end{align}

Block relay constraints

\begin{align} % for every replica and height, a single block can be relayed \sum_{t \in T} BlockRelay^t_{i,h,b} \leq 1 & \qquad \forall i \in R, \forall h, b \ %blockRelayed b only if relayed in time t height h blockRelayed_b \geq \frac{1}{N|H|} \sum_{t \in T}\sum_{i \in R}\sum_{h \in H} BlockRelay^t_{i,h,b} & \qquad \forall b \in B\ % if received M signatures until t-1, can relay block at time t BlockRelay^t_{i,h,b} \leq \frac{1}{M} \sum_{j \in R} recvdPrResp^{t-1}{i,j,h,b,v} + \sum{j \in R} recvdBlkPersist^t_{i,j,h,b} & \qquad \forall i \in R, h, b, v, t \end{align}

You can’t perform that action at this time.