protocol-bugs-list/table.tex at main · dranov/protocol-bugs-list · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[T2A]{fontenc}
\usepackage[main=english, russian]{babel}
\usepackage{booktabs}
\usepackage{footnote}
\usepackage{xcolor}
\makesavenoteenv{tabular}
\usepackage[backend=biber, style=alphabetic, sorting=nyt, urldate=iso]{biblatex}
\addbibresource{bibliography.bib}
\usepackage[hidelinks]{hyperref}

\title{Errors found in distributed protocols}
\date{}
\begin{document}

\maketitle

% To make it easier to filter output in table.md
\begin{center}
    {\footnotesize \color{white} (begin table)}
\end{center}

\begin{center}
\begin{tabular}{ c c c c }
    \toprule
    Protocol & Reference & Violation & Counter-example \\
    \midrule

    PBFT\footnote{With the read-only optimisation.} &
    \cite{castroPracticalByzantineFault1999} & liveness &
    \cite{bergerMakingReadsBFT2021} \\

    Chord & \cite{stoicaChordScalablePeertopeer2001,
    liben-nowellAnalysisEvolutionPeertopeer2002} &
    liveness\footnote{Eventual reachability is Chord's key
    correctness property.} & \cite{zaveUsingLightweightModeling2012,
    zaveReasoningIdentifierSpaces2017} \\

    Pastry & \cite{rowstronPastryScalableDecentralized2001} & safety &
    \cite{azmyRigorousCorrectnessProof2016, azmyMachinecheckedCorrectnessProof2018}\\

    Generalised Paxos & \cite{lamportGeneralizedConsensusPaxos2005} &
    non-triviality\footnote{Acceptors might accept commands that have not been
    proposed.} & \cite{sutraFastGenuineGeneralized2010} \\

    FaB Paxos & \cite{martinFastByzantineConsensus2005,
    martinFastByzantineConsensus2006} & liveness &
    \cite{abrahamRevisitingFastPractical2017} \\

    Multi-Paxos\footnote{As described in Paxos Made Live.} &
    \cite{chandraPaxosMadeLive2007} & safety &
    \cite{michaelRecoveringSharedObjects2017} \\

    Zyzzyva & \cite{kotlaZyzzyvaSpeculativeByzantine2007,
    kotlaZyzzyvaSpeculativeByzantine2009} & safety &
    \cite{abrahamRevisitingFastPractical2017} \\

    CRAQ & \cite{terraceObjectStorageCRAQ2009} & safety\footnote{Client reads
    might fail due to incorrect garbage collection.} &
    \cite{whittakerCRAQBug2020} \\

    JPaxos & \cite{konczakJPaxosStateMachine2011} & safety &
    \cite{michaelRecoveringSharedObjects2017} \\

    VR Revisited & \cite{liskovViewstampedReplicationRevisited2012} & safety &
    \cite{michaelRecoveringSharedObjects2017} \\

    EPaxos & \cite{moraruThereMoreConsensus2013} & safety &
    \cite{sutraCorrectnessEgalitarianPaxos2020} \\

    EPaxos & \cite{moraruThereMoreConsensus2013} & safety &
    \cite{whittakerEPaxosDependencySet2021} \\

    Raft & \cite{ongaroSearchUnderstandableConsensus2014} &
    liveness\footnote{The joint consensus membership change algorithm described
    in the paper version of Raft had a liveness bug, which was fixed in
    Ongaro's PhD thesis.} & \cite{hochConfigurationChanges2014} \\

    Raft & \cite{ongaroConsensusBridgingTheory2014} & safety\footnote{The bug
    is in the single-server membership change scheme described in Ongaro's
    thesis.} & \cite{amos15812TermPaper2015,
    ongaroBugSingleserverMembership2015} \\

    Raft & \cite{ongaroSearchUnderstandableConsensus2014,
    ongaroConsensusBridgingTheory2014} & liveness &
    \cite{howardRaftDoesNot2020, jensenExaminingRaftBehaviour2021} \\

    hBFT & \cite{duanHBFTSpeculativeByzantine2015} & safety &
    \cite{shresthaRevisitingHBFTSpeculative2019} \\

    Tendermint & \cite{buchmanTendermintByzantineFault2016} & liveness &
    \cite{cachinBlockchainConsensusProtocols2017} \\

    CAESAR & \cite{arunSpeedingConsensusChasing2017} & liveness &
    \cite{enesEfficientReplicationTimestamp2021} \\

    DPaxos & \cite{nawabDPaxosManagingData2018} & safety &
    \cite{whittakerMatchmakerPaxosReconfigurable2021} \\

    Sync HotStuff & \cite{abrahamSyncHotStuffSimple2019} & safety \& liveness &
    \cite{momoseForceLockingAttackSync2019} \\

    Gasper & \cite{buterinCombiningGHOSTCasper2020} & safety \& liveness &
    \cite{neuEbbandFlowProtocolsResolution2021} \\

    STM & \cite{Imbs2011} & safety \& liveness &
    \cite{Belyaev2010} \\

    FutureBus+ & \cite{IEEE8961Futurebus} & safety \& liveness &
    \cite{ClarkeGHJLMN93} \\

    \bottomrule
\end{tabular}
\end{center}

% To make it easier to filter output in table.md
\begin{center}
    {\footnotesize \color{white} (end table)}
\end{center}

\newpage
\printbibliography

\end{document}