#  : A Verifiable Logical Clock for P2P Networks

Working Draft

###### Abstract.

Logical clocks are a fundamental tool to establish causal ordering of events
in a distributed system. They have been applied in weakly consistent storage
systems, causally ordered broadcast, distributed snapshots, deadlock
detection, and distributed system debugging. However, prior logical clock
constructs fail to work in an open network with Byzantine participants. In
this work, we present , a novel logical clock system that targets such
challenging environment. We first redefine causality properties among
distributed processes under the Byzantine failure model. To enforce these
properties, defines a new _validator_ abstraction for building fault-tolerant
logical clocks. Furthermore, our validator abstraction is customizable:
includes multiple backend implementations for the abstraction, each with
different security-performance trade-offs. We have applied to build two
decentralized applications, a mutual exclusive service and a weakly consistent
key-value store. adds only marginal overhead compared to systems that tolerate
no Byzantine faults. It also out-performs state-of-the-art BFT total order
protocols by significant margins.

##  1\. Introduction

The ordering of events is a fundamental concept in distributed systems. In
state machine replication systems (smr, ; paxos, ; vr, ; raft, ), the set of
replicas needs to agree on the order of operations in the log; shards in a
distributed database (spanner, ; megastore, ; calvin, ) are tasked to execute
distributed transactions in a consistent partial order; for mutual exclusion
of shared resources, participants in a distributed system have to agree on the
order of acquiring locks (chubby, ; lockmanager, ; netlock, ); in a
distributed storage system (gfs, ; ceph, ; bigtable, ; dynamo, ; pegasus, ),
servers apply a consistent order of mutations to storage objects.

It is well-known that perfectly synchronized clocks do not exist in realistic
distributed systems, due to clock drift and relativity. Ordering events using
physical clock timestamps is therefore not reliable and can lead to anomalies.
Logical clocks (lamport-clock, ; vector-clock, ), on the other hand, offer a
solution to order events in a distributed system without relying on physical
time. Logical clocks order events based on _causal relationship_ instead of
real-time information. Concretely, if event $e_{1}$ potentially causes event
$e_{2}$ to happen, a logical clock ensures the clock value of $e_{1}$ is
smaller than the clock value of $e_{2}$. Logical clocks have been applied to a
wide range of distributed applications, including mutual exclusion (lamport-
clock, ), consistent distributed snapshot (snapshots, ), eventual consistency
(dynamo, ), and causally consistent data stores (cops, ; bayou, ; tact, ).

Many forms of logical clocks have been proposed in the literature (lamport-
clock, ; vector-clock, ; bloom-clock, ; plausible-clock, ; tree-clock, ).
Existing logical clock constructs, however, fall short in an open,
decentralized network (bitcoin, ; ethereum, ). In these networks, any
participant can join or leave the system at any time. Such dynamic environment
presents deep scalability challenges for vector-based logical clocks (vector-
clock, ; plausible-clock, ; tree-clock, ). More critically, prior systems
assume all participants in the system faithfully follow the protocol to update
and propagate their clocks. In a decentralized network, Byzantine (byzantine,
) behaviors, where a participant can deviate arbitrarily from the specified
protocol, can make the clocks violate the causality properties, potentially
corrupting application state or leading to undefined behavior. Unfortunately,
existing logical clock constructs are not Byzantine-fault tolerant. Without
reliable logical clocks, systems and applications are forced to use expensive
BFT SMR protocols (pbft, ; hotstuff, ; bitcoin, ; honeybadger, ) which
enforces total order of requests, even though their application semantics may
only require partial ordering guarantees.

In this work, we propose , a novel logical clock system that offers secure
reasoning of causality for distributed applications in a P2P network. At the
core of is a _verifiable logical clock_ () construct. provides similar
“happened-before” partial order relation for events in a P2P network. It uses
a map structure to record clock values for each process, ensuring the size of
each is only proportional to the causal history and not to the system size. A
novel property of is its _verifiability_. Each is accompanied by a _proof_
that is verifiable by any third party. By validating the proof, any process in
the system can be convinced that the attached is correctly generated by a
_sequence_ of clock operations. Moreover, the proof verifies that each clock
input to the sequence of operations is also correct. This _recursive
verifiability_ is very powerful: It gives the same causality correctness
properties as previous logical clocks, even in the presence of Byzantine
processes. To improve usability of , we further strengthen verifiability of
each to tolerate adversaries who intentionally create concurrent clocks, or
generate erroneous clocks which deviates from application semantics.

We design as a concrete instance of . is a user-space library loaded into each
distributed application. To handle the complexity and diverse requirement of
verifiability, we define a _validator_ abstraction. The abstraction is divided
into a _frontend_ and a _backend_. The frontend defines the _semantics_ of
each validator. For , we develop three such validator frontends: An _update
validator_ which verifies that the clock update operation obeys the rules; a
_monotonicity validator_ to detect processes violating local ordering rules;
an _application validator_ that checks if the clock update follows
application-specific semantics. The backend, on the other hand, defines
_execution_ of validators, , how proofs are generated and validated. We
designed and implemented three such validator backends. The _quorum backend_
relays the clock operation to a group a validator nodes. Each validator checks
the operation and signs a validation certificate. The threshold signature from
a group of validators serve as the proof. The _TEE backend_ uses a validator
with trusted execution environment (TEE) to verify the operation. The backend
uses attestation from the TEE as the proof. Lastly, the _IVC backend_ uses a
cryptographic construct called incrementally verifiable computation (IVC) to
generate succinct recursive proofs without relaying on external validator
nodes.

We leverage to build two distributed applications which tolerate Byzantine
behaviors. The first use case develops a mutual exclusion protocol. The
protocol enforces the same set of guarantees as the original protocol
(lamport-clock, ) in a fail-stop model, including ordered resource
acquisition. The second use case is a casually consistent key-value store,
following the storage semantics of COPS (cops, ). The data store ensures
client reads to obey causal consistency while allowing writes to be done
without expensive global coordination.

We evaluate and the use cases. The end to end evaluations on the use cases
show secures verifiable causality with reasonable and sometimes even marginal
overhead. In the mutex evaluation, adds less than 1%/38% latency to the unsafe
baseline to handle one request, while a total order based approach would incur
4.3x latency to the baseline. When all processes concurrently requesting, is
able to finalize all requests in 4.3s/18.8s with 60 processes. In the data
store evaluation, is able to maintain over 200Kops/second throughput with
100ms latency, while a total order replicated store can only reach
70Kops/second while latency already goes up to 1s. In the micro-benchmarks, we
study the various backends with fixed or varying computational resources. Each
of the backends is able to maintain steady proving time with up to 1000 clock
size. While circuit backend takes more than 1s to prove, the other backends
are able to prove with millisecond scale latency. The backends also scales
well regarding clock size, the number of CPUs, the number of merged clocks and
the number of faulty quorum members.

##  2\. Background and Related Work

###  2.1. Causal Event Ordering

Determining the order of events is a fundamental and important problem in
distribute systems. It is well-known that physical clocks are an unreliable
source of event ordering due to relativity and clock skews. The seminal work
by Lamport (lamport-clock, ) addresses the issue by introducing a _happened-
before_ relationship that defines the possible causality between events in a
distributed system. Specifically, let $\prec$ be a binary relation between
pairs of events in an execution of a distributed system. $e_{1}\prec e_{2}$ if
event $e_{1}$ may influence event $e_{2}$, or equivalently, $e_{2}$ is
causally dependent on $e_{1}$. $\prec$ is a strict partial order, , it is
irreflexive, asymmetric, and transitive. Being a partial order, not all pairs
of events are causally dependent. If neither $e_{1}\prec e_{2}$ nor
$e_{2}\prec e_{1}$, $e_{1}$ and $e_{2}$ are defined to be logically concurrent
(represented as $e_{1}\parallel e_{2}$). Without perfectly synchronized
physical clocks, it is impossible to determine which of $e_{1}$ or $e_{2}$
happens first if $e_{1}\parallel e_{2}$.

Events in an execution are categorized into three general types. Local events,
, are any event happened on a process that does not involve messages; is a
message send event from a source process, and for each , there is a
corresponding message receive event, , on the destination process if the
message is successfully delivered. Note that the model assumes all local
events on a process happen _sequentially_.

The happened-before relation $\prec$ on the set of events in an execution
obeys the following rules:

  * •

1 $\prec$ 2 if both events happen on the same process and 1 happens before 2
in the local sequential event order.

  * •

$\prec$ if and are the corresponding message send and receive pair.

###  2.2. Logical Clocks

Logical clocks are a common approach to determine the happened-before relation
defined in subsection 2.1. One instance of logical clocks is the Lamport clock
(lamport-clock, ). Using Lamport clock, each process $n_{i}$ in the system
maintains a local clock $c_{i}$, represented as a natural number. Upon a local
event i, $n_{i}$ increments its local clock by one. When $n_{i}$ sends a
message, $n_{i}$ increments its local clock, and attaches the local clock
value in the message. When $n_{i}$ receives a message with a clock value
$c_{m}$, it sets its local clock to $max(c_{i},c_{m})+1$.

The logical time of an event $e$, represented as $c_{e}$, is the local clock
value after the clock update. Lamport clock guarantees the following property:
If $e_{1}\prec e_{2}$, then $c_{e_{1}}<c_{e_{2}}$. However, the inverse is not
true, , $c_{e_{1}}<c_{e_{2}}$ does not imply that $e_{1}\prec e_{2}$. To be
more precise, if $c_{e_{1}}<c_{e_{2}}$, either $e_{1}\prec e_{2}$ or
$e_{1}||e_{2}$, but not $e_{2}\prec e_{1}$.

Vector clock (vector-clock, ; holy_grail, ) addresses this shortcoming of
Lamport clock. As the name suggested, a vector clock, $v$, consists of a
vector of natural numbers. Cardinality of a vector clock equals the size of
the system. Each process is assigned a unique index in the vector clock. We
use $v[i]$ to denote the $i$th number in a vector clock $v$. Upon a local
event, $n_{i}$ increments $v_{i}[i]$ by one. When $n_{i}$ sends a message,
$n_{i}$ increments $v_{i}[i]$, and attaches $v_{i}$ in the message. When
$n_{i}$ receives a message with a clock $v_{m}$, it sets $v_{i}$ to
$v_{i}^{\prime}$, where $\forall
p\in[0..S),v_{i}^{\prime}[p]=max(v_{i}[p],v_{m}[p])$, $S$ is the size of the
system. $n_{i}$ then increments $v_{i}[i]$.

$v_{i}<v_{j}$ if and only if $\forall p\in[0..S),v_{i}[p]\leq v_{j}[p]$ and
$\exists p\in[0..S),v_{i}[p]<v_{j}[p]$. By definition, there exists $v_{i}$
and $v_{j}$ such that neither $v_{i}<v_{j}$ nor $v_{j}<v_{i}$, , $<$ is a
partial order on the set of vector clocks. Vector clock guarantees the
following stronger property: $e_{1}\prec e_{2}$ _if and only if_
$v_{e_{1}}<v_{e_{2}}$.

Logical clocks and causal event ordering have wide applicability to
distributed systems and algorithms designs. Lamport showed in his original
paper how Lamport clocks can be used to implement distributed mutual exclusion
(lamport-clock, ). Vector clocks are applied to realize consistent distributed
snapshots (snapshots, ). Amazon leverages version vectors, a type of vector
clocks, to build eventually consistent data store Dynamo (dynamo, ). Logical
clocks are also used to implement various causally consistent key value stores
(cops, ; bayou, ; tact, ).

###  2.3. Byzantine Fault Tolerance

Failures are common events in a distributed system. There are in general two
types of failure models, crash failure model and Byzantine failure model. In
the crash failure model, once a process fails, it stops communication with all
other processes until it recovers. In the Byzantine failure model (byzantine,
), a failed process can behave arbitrarily, including launching adversarial
attacks to break the system. Numerous distributed protocols have been
developed to tolerate Byzantine faults. The most common setting these
protocols target is the state machine replication (smr, ) problem. The core of
the problem is reaching consensus on a _totally ordered_ request log, even in
the presence of Byzantine behaviors. The seminal work in this space is PBFT
(pbft, ), which is the first practical BFT protocol that tolerates up to $f$
Byzantine nodes using $3f+1$ replicas. PBFT is leader-based protocol. After
the leader orders and disseminates client requests, the backup replicas use
two rounds of all-to-all communication to commit a batch of requests. The
protocol therefore incurs a latency of five message delays and an
authenticator complexity of $O(N^{2})$. A long line of work subsequently
improves various aspects of PBFT. Zyzzyva (zyzzyva, ) uses speculative
execution to reduce communication overhead. It enables a fast path protocol
that commits client requests in only three message delays. HotStuff (hotstuff,
) adds one round of communication in normal operation to reduce the expensive
view change protocol in PBFT from $O(N^{3})$ to $O(N)$ authenticator
complexity. Several protocols (a2m, ; trinc, ; minbft, ) leverage trusted
hardware, such as Trusted Platform Module (TPM) (tpm, ) and Trusted Execution
Environment (TEE) (tee, ), to reduce the replication factor to $2f+1$. A
different line of BFT work (honeybadger, ; narwhal_tusk, ; dumbo, ) uses
randomness to ensure protocol liveness even in a fully asynchronous network,
bypassing the FLP impossibility result (flp, ).

##  3\. A Verifiable Logical Clock

We start the section with a motivating example to illustrate the impact of
Byzantine behaviors on causal event ordering. We then define a new type of
logical clock, the verifiable logical clock (), to address the issues.

###  3.1. Motivating Example

Figure 1.  A motivating example.

We use the causal message delivery (reli_comm, ; causal_ordering, ) problem as
a motivating example. In a system that guarantees causal message delivery, if
two messages $m$ and $m^{\prime}$ are received by the same process, and $m$ is
ordered before $m^{\prime}$ by the happened-before relationship $\prec$
(subsection 2.1), then the process delivers $m$ before $m^{\prime}$. Figure 1
shows an example involving three processes, $P1$, $P2$, and $P3$. The event of
sending message $m_{1}$ happened before the message send event of $m_{3}$
($\es{m_{1}}\prec\es{m_{2}}$, $\es{m_{2}}\prec\er{m_{2}}$,
$\er{m_{2}}\prec\es{m_{3}}$ $\implies\es{m_{1}}\prec\es{m_{3}}$). However,
$P3$ receives $m_{3}$ before $m_{1}$. This can happen even if processes use
ordered, reliable point-to-point channels (, TCP). If the system enforces
causal message delivery, $P3$ can only deliver $m_{3}$ after delivering
$m_{1}$.

Vector clocks can be used to implement causal message delivery
(causal_ordering, ). By following the protocol described in subsection 2.2,
the vector clocks attached in messages $m_{1}$, $m_{2}$, and $m_{3}$ are
$\text{\flqq}1,0,0\text{\frqq}$, $\text{\flqq}2,0,0\text{\frqq}$, and
$\text{\flqq}2,2,0\text{\frqq}$ respectively. To ensure that all the received
messages are delivered in causal order (but allows dropping of messages), $P3$
compares its local clock against the clock of every received message. If the
received clock is smaller (the partial order comparison as defined in
subsection 2.2) than the local clock, the message is discarded. When $P3$
first receives $m_{3}$ with clock $\text{\flqq}2,2,0\text{\frqq}$, its local
clock is smaller than the received clock, so $P3$ delivers $m_{3}$ and updates
its local clock to $\text{\flqq}2,2,1\text{\frqq}$. When $P3$ later receives
$m_{1}$, since the message clock $\text{\flqq}1,0,0\text{\frqq}$ is smaller
than $P3$’s local clock, $m_{1}$ is not delivered.

The original causal message delivery definition (reli_comm, ; causal_ordering,
), however, does not allow rejection of message $m_{1}$. To deliver $m_{1}$
while not violating causal ordering, $m_{3}$ needs to include extra
information so that $P3$ is aware that it should wait for $m_{1}$ which
happened before $m_{3}$. Following the protocol proposed in (causal_ordering,
), each process maintains a vector clock mapped to every other process (called
ord_buff_s in (causal_ordering, )). Each vector clock maintains the maximum
111Note the maximum operation here is a per-element maximum, ,
$v_{max}={max}(v_{a},v_{b})\iff\forall
p\in[0..S),v_{max}[p]=max(v_{a}[p],v_{b}[p])$ message clock _destined_ to the
mapped process known by the local process. The map is attached to each sent
message. In the example above, $P2$ updates the clock mapped to $P1$ to
$\text{\flqq}1,0,0\text{\frqq}$ after receiving $m_{2}$, and attaches this
information in $m_{3}$. When $P3$ receives $m_{3}$, it detects that its local
clock $\text{\flqq}0,0,0\text{\frqq}$ is smaller than the mapped clock value
$\text{\flqq}1,0,0\text{\frqq}$ in the message. $P3$ then knows it has not
received all messages with earlier causal dependencies, and therefore buffers
$m_{3}$. When $P3$ later receives $m_{1}$, the attached clock map is empty, so
$P3$ delivers $m_{1}$ and updates local clock to
$\text{\flqq}1,0,1\text{\frqq}$. Now the local clock is greater than $m_{3}$’s
mapped value, so $P3$ can deliver $m_{3}$.

###  3.2. Impact of Byzantine Processes

The above protocol assumes that all processes are honest and strictly follow
the protocol. Now, we show how Byzantine processes can violate the causal
message delivery properties. To simplify the discussion, we allow processes to
reject messages that happened before previously delivered messages, so
processes do not need to maintain and attach vector clock mapping ord_buff_s.
Note that since a Byzantine process can deliver messages in any arbitrary
order, we can only enforce causal message delivery on non-faulty processes. We
should probably also discuss omission failures.

##### Erroneous clock updates

A Byzantine process may violate the logical clock update rules as defined in
subsection 2.2. Suppose $P2$ is a Byzantine process in the scenario depicted
in Figure 1. When $P2$ receives $m_{2}$ with vector clock
$\text{\flqq}2,0,0\text{\frqq}$, it could generate an erroneous vector clock
$\text{\flqq}0,2,3\text{\frqq}$ for message $m_{3}$. As such, vector clocks
for $m_{1}$ ($\text{\flqq}1,0,0\text{\frqq}$) and $m_{3}$
($\text{\flqq}0,2,3\text{\frqq}$) are concurrent. Subsequently, $P3$ is unable
to detect the true causal dependency between $m_{1}$ and $m_{3}$, and will
deliver $m_{3}$ before $m_{1}$.

Should we also draw a figure for this case? Even a weaker form of clock
forging can break causal message deliver. Suppose a signature scheme is
applied (signed_clock, ) so that a Byzantine process can only manipulate its
own index in a vector clock. Assume $P3$ has sent messages $m_{a}$ with clock
$\text{\flqq}0,0,1\text{\frqq}$ to $P2$ and $m_{b}$ with clock
$\text{\flqq}0,0,2\text{\frqq}$ to $P1$, before the message trace in Figure 1.
$m_{1}$ and $m_{2}$ will now have vector clocks
$\text{\flqq}2,0,2\text{\frqq}$ and $\text{\flqq}3,0,2\text{\frqq}$
respectively. After $P2$ receives $m_{2}$, it now has two vector clocks
locally, $\text{\flqq}0,0,1\text{\frqq}$ (for $m_{a}$) and
$\text{\flqq}3,0,2\text{\frqq}$ (for $m_{2}$). Even if $P2$ cannot forge clock
values for other indices, it could still generate a vector clock
$\text{\flqq}3,2,1\text{\frqq}$ for $m_{3}$ by cherry-picking values from each
received clock. The clocks for $m_{1}$ ($\text{\flqq}2,0,2\text{\frqq}$) and
$m_{3}$ ($\text{\flqq}3,2,1\text{\frqq}$) are concurrent; $P3$ again will
deliver $m_{1}$ after $m_{3}$.

##### Local ordering violation

Lamport and vector clocks assume a sequential processor model, , a process
handles all events (including local events, message receive events, and
message send events) sequentially. An implication is that the logical clock of
each process increases _monotonically_ : for any two events $e_{1}$ and
$e_{2}$ happened on a process $p$, suppose $e_{1}$ occurred before $e_{2}$ in
the local sequential order, then $e_{1}\prec e_{2}$ and $c_{e_{1}}<c_{e_{2}}$.
To enforce this monotonicity property, a process maintains a single local
clock which it sequentially updates on each event.

A Byzantine process may violate this local causal ordering property, even if
it follows all clock update rules. Same question: should we draw another
figure for this case? This example is not entirely correct. Need to rethink.
The example you are seeking probably involves concurrent clocks generated by
the same process. This implies the merging pattern of events. The only way to
build such case with current message pattern in the figure is to assume a
faulty P3, because the only merging pattern happens on P3. P3 should first
merge with receiving m3, then rewind its clock and merge again to m1. Then it
can confuse the other processes with the two concurrent clocks. Suppose the
Byzantine process $P2$ generates a clock $\text{\flqq}0,3,0\text{\frqq}$ and
attaches it to a message that it sends to $P1$. The same message pattern then
occurs following Figure 1. $m_{1}$ and $m_{2}$ will have vector clocks
$\text{\flqq}2,3,0\text{\frqq}$ and $\text{\flqq}3,3,0\text{\frqq}$
respectively. When $P2$ receives $m_{2}$, instead of updating based on its
current clock $\text{\flqq}0,3,0\text{\frqq}$, $P2$ uses one of its older
clocks, $\text{\flqq}0,1,0\text{\frqq}$ for clock update. Note that this is a
legitimate clock generated by $P2$, so this is not an erroneous clock update.
$P2$ attaches the resulting clock, $\text{\flqq}3,2,0\text{\frqq}$, to
$m_{3}$. Since $\text{\flqq}3,2,0\text{\frqq}$ and
$\text{\flqq}2,3,0\text{\frqq}$ are concurrent, $P3$ delivers $m_{1}$ after
$m_{3}$ which violates causal ordering.

###  3.3. Verifiable Logical Clocks

We now define a new form of logical clock, a _verifiable logical clock_ (),
that tolerates the Byzantine behaviors described in subsection 3.2. section 4
elaborates on the concrete design of . We first define the system model, the
clock operations, and the clock properties. The system consists of a group of
entities, each identified by a unique $id$. We do not constraint the entities
to be physical participants of the system; they can also be virtual nodes,
objects, or database keys. We define two operations:

  * •

$\fn{Init}()\rightarrow c$: Creates a genesis clock.

  * •

$\fn{Update}(id,c,[c_{1},c_{2},\cdots])\rightarrow c^{\prime}$: Generates a
new clock $c^{\prime}$ by merging clock $c$ with a set of clocks
$c_{1},c_{2},\cdots$ and then incrementing the merged clock. $id$ denotes the
identifier of the entity that performs the increment. The set
$\text{\flqq}c_{1},c_{2},\cdots\text{\frqq}$ could be empty.

Performing $\fn{Update}()$ with an empty set is equivalent to a local event
clock update in prior logical clocks, while $\fn{Update}()$ with a single
clock in the set is equivalent to a message receive event. The set of s forms
a _partially ordered set_. The partial order relation $\prec$ on the set is
defined by the following rule: If
$\fn{Update}(id,c,[c_{1},c_{2},\cdots])\rightarrow c^{\prime}$, then $c\prec
c^{\prime}$, $c_{1}\prec c^{\prime}$, $c_{2}\prec c^{\prime}$, $\cdots$

The partial order $\prec$ has the following properties:

  * •

_Irreflexivity_ : $\forall c\in C,c\nprec c$

  * •

_Asymmetry_ : $\forall c_{1},c_{2}\in C,c_{1}\prec c_{2}\implies c_{2}\nprec
c_{1}$

  * •

_Transitivity_ : $\forall c_{1},c_{2},c_{3}\in C,c_{1}\prec c_{2}\land
c_{2}\prec c_{3}\implies c_{1}\prec c_{3}$

The above rules and properties also _completely_ define $\prec$, , $c_{1}\prec
c_{2}$ _if and only if_ there exists a sequence of $\fn{Update()}$ operations
that takes $c_{1}$ as an initial input and generates $c_{2}$. An implication
is that there exists s that are not ordered by $\prec$. For instance, given a
genesis clock $c$ and two identifiers $id_{1}$ and $id_{2}$ such that
$id_{1}\neq id_{2}$, $c_{1}\leftarrow\fn{Update}(c,id_{1},[])$ and
$c_{2}\leftarrow\fn{Update}(c,id_{2},[])$, then $c_{1}\nprec c_{2}$ and
$c_{2}\nprec c_{1}$. Two s that are not ordered by $\prec$ are called
_concurrent_ , and we use $c_{1}\parallel c_{2}$ to denote concurrency.

Given the above definitions, we also define a compare function to determine
the partial order of two s:

  * •

$\fn{Compare}(c_{1},c_{2})\rightarrow\\{BF,EQ,AF,CC\\}$: Returns $BF$ if
$c_{1}\prec c_{2}$, $AF$ if $c_{2}\prec c_{1}$, $EQ$ if $c_{1}=c_{2}$, and
$CC$ if $c_{1}\parallel c_{2}$.

##### Clock Verifiablility.

As discussed in subsection 3.2, Byzantine processes can tamper with logical
clock updates to violate causal order relationship among events. To tolerate
such Byzantine behaviors, additionally provides _verifiability_. Each $c$ is a
tuple of $\tuple{v,\pi}$, where $v$ is the clock value and $\pi$ is a _proof_.
The proof proves the following properties of $c$ in the tuple:

  1. (1)

The clock is _correctly_ generated by a sequence of $\fn{Init}()$ and
$\fn{Update}()$ operations.

  2. (2)

Each $\fn{Update}(id,c,[c_{1},c_{2},\cdots])$ in the sequence is invoked by a
process with permission on the entity $id$.

  3. (3)

For each $\fn{Update}(id,c,[c_{1},c_{2},\cdots])$ in the sequence, each input
clock ($c,c_{1},c_{2},\cdots$) _recursively_ satisfies the above properties.

The proof can _optionally_ enforce the following global property: For each
$id$ in the system, the set of s correctly generated by
$\fn{Update}(id,\dots)$ is _totally ordered_ by $\prec$. Equivalently, no two
clocks in the set are concurrent.

We only define the above property as optional since it is not required by all
use cases. We elaborate the impact of this optional property in section 4 and
example applications that do not require it in section 5.

The system defines a $\fn{Verify}()$ function to validate the correctness of a
:

  * •

$\fn{Verify}(c)\rightarrow\\{\var{true},\var{false}\\}$: Returns _true_ if the
proof $\pi$ in $c$ is valid, and _false_ otherwise.

Note that invoking $\fn{Update}()$ and $\fn{Compare()}$ with invalid clocks
will simply return an error. Properly invoked $\fn{Init}()$ and
$\fn{Update}()$ operations return clocks that are verifiable. More formally:

  * •

If $\fn{Init}()\rightarrow c$, then $\fn{Verify}(c)\rightarrow\var{true}$

  * •

If $\fn{Verify}(c)\rightarrow\var{true}$,
$\fn{Verify}(c_{1})\rightarrow\var{true}$,
$\fn{Verify}(c_{2})\rightarrow\var{true}$, $\cdots$, and
$\fn{Update}(id,c,[c_{1},c_{2},\cdots])\rightarrow c^{\prime}$, then
$\fn{Verify}(c^{\prime})\rightarrow\var{true}$

If the optional property of proof is enforced, we need to augment the second
clock verifiability rule by adding the clause: $c^{\prime}$ is not $\parallel$
to any clock $c_{id}$ where $c_{id}\leftarrow\fn{Update}(id,\dots)$ and
$\fn{Verify}(c_{id})\rightarrow\var{true}$.

Similar to $\prec$, the above rules also _completely_ define verifiability, ,
$\fn{Verify}(c)$ returns $\var{true}$ _if and only if_ $c$ is generated by a
sequence of properly executed $\fn{Init}()$ and $\fn{Update}()$ operations.

##### Byzantine Fault Tolerance

Clock verifiability eliminates the causal message delivery violations in
subsection 3.2. Once we have figures for each of these violations, can easily
refer to the figure. Suppose the ID for $P1$, $P2$, and $P3$ are $id_{1}$,
$id_{2}$, and $id_{3}$ respectively. Each process starts with an initial clock
$c_{0}$ generated from $\fn{Init}()$. In the first scenario, $P1$ generates
for $m_{1}$ and $m_{2}$ by $c_{1}\leftarrow\fn{Update}(id_{1},c_{0},[])$ and
$c_{2}\leftarrow\fn{Update}(id_{1},c_{1},[])$. By definition, $c_{1}\prec
c_{2}$. When $P2$ receives $m_{2}$, the only _valid_ clock it can generate for
$m_{3}$ is $c_{3}\leftarrow\fn{Update}(id_{2},c_{0},[c_{2}])$222$P2$ can also
use valid clocks other than $c_{0}$ as input to generate $c_{3}$. Regardless,
the causal relationship between $c_{3}$ and $c_{1}$ will not change.. $P2$
does not have permission to other IDs when invoking $\fn{Update}()$, and
$c_{2}$ is the only clock it receives from other processes. $P3$ simply
ignores any invalid clocks that do not pass $\fn{Verify}()$. As such,
$c_{2}\prec c_{3}$ and therefore $c_{1}\prec c_{3}$ by our clock properties.
$P3$ will thus reject $m_{1}$ after delivering $m_{3}$.

In the second weak forging scenario, clocks for $m_{a}$ and $m_{b}$ are
generated by $P3$ as $c_{a}\leftarrow\fn{Update}(id_{3},c_{0},[])$ and
$c_{b}\leftarrow\fn{Update}(id_{3},c_{a},[])$ respectively. $P1$ will then
generate $c_{1}\leftarrow\fn{Update}(id_{1},c_{0},[c_{b}])$ for $m_{1}$, and
$c_{2}\leftarrow\fn{Update}(id_{1},c_{1},[])$. As such, $c_{a}\prec c_{b}\prec
c_{1}\prec c_{2}$. After $P2$ receives $m_{2}$, it possesses two valid clocks
from other processes, $c_{a}$ and $c_{2}$. We do need to discuss omission
issues earlier. When generating a valid clock $c_{3}$ for $m_{3}$, $P2$ can
either include or exclude $c_{a}$ in the $\fn{Update}()$ invocation. In either
case, the resulting valid clock $c_{3}$ will have $c_{2}\prec c_{3}$.

In the last local ordering scenario, suppose $P2$ generates a sequence of
clocks, $c_{a}$, $c_{b}$, and $c_{c}$, by repeatedly invoking $\fn{Update}()$.
Therefore, $c_{0}\prec c_{a}\prec c_{b}\prec c_{c}$. It attaches $c_{c}$ to
the first message it sends to $P1$. When $P1$ receives the message and
generates $c_{1}$ for $m_{1}$ and $c_{2}$ for $m_{2}$, we will have
$c_{c}\prec c_{1}\prec c_{2}$. After $P2$ receives $m_{2}$, it can no longer
use $c_{0}$, $c_{a}$, or $c_{b}$ as input to
$\fn{Update}(id_{2},c_{input},[\cdots])$ and produce a valid clock, since any
resulting clock $c_{output}$ will have $c_{output}\parallel c_{c}$. This is a
violation of the augmented clock verifiability rule. Complete this after
correcting the example in subsection 3.2.

We should move the following clock sealing part to design, together with
discussions on application semantics.

##  4\. System Design

In section 3, we define the high-level properties of our new logical clock .
In this section, we elaborate on the design of which leverages a general
_validator_ abstraction. We then describe multiple concrete implementation of
the validator abstraction that use quorum certificates, trusted hardware, and
verifiable computation, each with its own trade-offs.

###  4.1. Design Overview

Figure 2.  overview. Add more descriptions in the caption.

As shown in Figure 2, is a user-space library linked into distributed
applications. The library exposes an API that includes the $\fn{Init}()$,
$\fn{Update}()$, $\fn{Verify}()$, and $\fn{Compare}()$ functions as introduced
in section 3. The main data structure exposed to the application is an opaque
. Internally, each contains both numerical clock values and a proof
(corresponding to the $\tuple{v,\pi}$ tuple in subsection 3.3). Besides using
as input for the API functions, also provides $\fn{serialize}()$ and
$\fn{deserialize}()$ interfaces for the application to send/receive s over the
network. The API should include signatures and public keys. There should also
be a global configuration service that keeps ID, public key, and application-
specific permission control rules. Maybe describe them in the validator part.

The library internally consists of two main components: a clock module and a
validator module. The clock module defines the clock value structure in (, $v$
in $\tuple{v,\pi}$), and implements the basic clock update and comparison
functionalities. For each , the module maintains a _map_ between an ID and an
integer which presents the current clock value. IDs not inserted in a are
implicitly mapped to clock value 0; a clock generated from $\fn{Init()}$
contains an empty map. We use a map instead of a vector to support open
systems with potentially unbounded participant set. Size of each is only
linear to its causally dependent IDs.

When an application invokes $\fn{Update}(id,c,[c_{1},c_{2},\cdots])$, the
module creates a new clock $c^{\prime}$, and installs the _maximum_ clock
value mapped to each present ID among $c,c_{1},c_{2},\cdots$ into
$c^{\prime}$. It then increments the clock value mapped to the input $id$ in
$c^{\prime}$ by one. To compare two clocks $c_{1},c_{2}$ using
$\fn{Compare}(c_{1},c_{2})$, the module returns $BF$ if the mapped clock value
for each ID is not bigger in $c_{1}$ than that in $c_{2}$, and at least one of
the values is smaller. For the symmetrical opposite case, the modules returns
$AF$. It returns $EQ$ when all mapped values are equal. For all other cases,
the module returns $CC$. Both the update and the comparison operation are
similar to those in vector clocks.

The validator module is responsible for proving and verifying the _validity_
of s, as defined in subsection 3.3. The module defines a general _validator
abstraction_ (subsection 4.2). The abstraction exposes a $\fn{prove}()$ and
$\fn{validate}()$ interface to the library. The $\fn{prove}()$ function
includes instance-specific logic to test clock update invocations and
generates a small _proof_ ; $\fn{check}()$ verifies the validity of an input
proof generated by $\fn{prove}()$. includes three concrete instances of the
abstraction. The _update validator_ checks the validity of a clock
$\fn{Update}()$ invocation, as defined by the base clock verifiability
properties in subsection 3.3. The _monotonicity validator_ ensures that the
clock for each ID is increasing in a monotonic fashion, which corresponds to
the optional clock verifiability property in subsection 3.3. The _application
validator_ includes additional application-specific logic to further constrain
$\fn{Update}()$ invocations; such constraints were not covered in subsection
3.3, and we elaborate their use cases in subsection 4.2. Proofs generated by
each validator instance are _typed_. We use $\pi_{up}$, $\pi_{mono}$, and
$\pi_{app}$ and represent each proof type. The proof in each ($\pi$ in
$\tuple{v,\pi}$) is effectively a union of $\pi_{up}$, $\pi_{mono}$, and
$\pi_{app}$. Not all applications require all three proof types.

We are now ready to give an overview of how the library uses the two modules
to process user API calls. When $\fn{Verify}(c)$ is invoked, where $c$ is
$\tuple{v,\tuple{\pi_{up},\pi_{mono},\pi_{app}}}$, the library inputs each of
the $\pi_{update}$, $\pi_{mono}$, and $\pi_{app}$ to the $\fn{check}()$
functions of the corresponding validator instance. The library returns
$\var{true}$ if and only if all three $\fn{check}()$ calls return
$\var{true}$.

When $\fn{Update}(id,c,[c_{1},c_{2},\cdots])$ is invoked, the library first
calls $\fn{Verify}()$ on each of the input clocks $c,c_{1},c_{2},\cdots$. If
all input clocks are properly verified, the library invokes the $\fn{prove}()$
function in the update, the monotonicity, and the application validator
instances to get
$\pi^{\prime}\leftarrow\tuple{\pi_{up},\pi_{mono},\pi_{app}}$. It then applies
the update function in the clock module with $id$ and the input clock values
to get $v^{\prime}$. The library then returns
$c^{\prime}\leftarrow\tuple{v^{\prime},\pi^{\prime}}$ to the application.

Add $\fn{Init}()$ and $\fn{Compare}()$ overview.

###  4.2. The Validator Abstraction

The critical property differentiating from prior logical clocks is its
_verifiability_. Traditional approaches such as public key signature schemes
or verifiable computation (pantry, ; pinocchio, ; zaatar, ) establish
verifiability for a single computational result. , however, requires
_recursive verifiability_ : Validity of a $c$ depends on not only the correct
execution of the $\fn{Update}()$ function that generates $c$, but also
_recursively_ on the validity of each of the input clocks.

Moreover, the exact semantics of _logical clock correctness_ depends on the
application. As we discussed in subsection 3.3, the causal order relationship
$\prec$ only requires the base clock verifiability properties. For
applications that additionally require _local ordering_ guarantees, needs to
enforce the augmented verifiability rule. An application may also have
specific restrictions on the set of logical clocks that can be generated. As a
concrete example, consider a storage application where clients include logical
clocks as dependency set (cops, ; dynamo, ) in their put requests. The
application may require access control on the set of keys each client can
write. When generating logical clocks for new key versions, the clock update
function needs to reject the request if the client lacks permission. Such
application-specific constraints are not enforced by the verifiability rules
in subsection 3.3. We will elaborate this exact use case in subsection 5.2.

In , we address these challenges by applying a _modular_ architecture with a
common _validator abstraction_ for clock verifiability. We forgo a monolithic
design due to its inherit design complexity, and more importantly, its lack of
flexibility. Our validator abstraction defines a simple $\fn{prove}()$ and
$\fn{check}()$ interface:

  * •

$\fn{prove}(\var{req},\var{aux})\rightarrow\\{\pi,\bot\\}$: Verify the
validity of the $\fn{Update}()$ invocation in $\var{req}$. $\var{aux}$ is an
optional auxiliary input for proof generation. Returns a proof $\pi$ if the
request is valid, or $\bot$ otherwise.

  * •

$\fn{check}(\pi)\rightarrow\\{{\var{true},\var{false}}\\}$: Returns
$\var{true}$ if the input proof $\pi$ is correct, $\var{false}$ otherwise.

We design three concrete instances of the validator abstraction. Each instance
applies specific clock verifiability rules: the _clock update validator_
enforces the base properties defined in subsection 3.3; the _monotonicity
validator_ checks the optional local ordering properties; the _application
validator_ applies any application-specific clock generation constraints.
offers flexibility: an application can choose the appropriate validator
instances based on its requirements.

also provides _configurability_. Different implementations exist for each
validator instance: A validator can be implemented using a group of servers
and their signatures, or a single server with trusted execution environment.
To enable this configurability, we further split the abstraction into a
_validator frontend_ and a _validator backend_. The frontend defines the
_semantics_ of a validator instance. Semantics of a validator defines the
verification logic, , what $\var{req}$ and $\var{aux}$ combinations are valid,
as discussed above. They, however, do not define the execution of the
verification procedure, which is the responsibility of the validator backend.
Each backend type implements a _security protocol_ that generates and verifies
_proofs_ for the validator frontend logic. The protocol can use a quorum-
certificate-based protocol (subsubsection 4.4.1) or leverage trusted execution
environment (subsubsection 4.4.2), each with different trade-offs in security,
performance, and hardware requirements. The frontends and backends are
completely decoupled. An application can use any backend for its validator
instances depending on its specific requirements.

###  4.3. Validator Frontend

We now elaborate on the frontend logic for the three validator instances.

####  4.3.1. Clock Update Validity

The _clock update validator_ ensures that a is properly generated using the
base clock update rules defined in subsection 3.3. For each
$\fn{prove}(\var{req},\var{aux})$ call, $\var{req}$ includes the inputs to a
$\fn{Update}(id,c,[c_{1},c_{2},\cdots])$ invocation, signed by the invoking
process, while $\var{aux}$ is empty. The validator first checks the validity
of each input clock by calling $\fn{Verify}()$ on the clock proof
$\pi\leftarrow\\{\pi_{up},\pi_{mono},\pi_{app}\\}$, which internally performs
$\fn{check}()$ on each validator proof. Any invalid input clock results in the
validator outputting $\bot$. Next, the validator checks $\var{req}$ is signed
by a process with permission on the identifier $id$. The permission table is
either determined statically, or maintained by a global configuration service.
Details of such a service is out of the scope of the paper. If the permission
check passes, the $\var{req}$ is fully validated, and the validator outputs a
$\pi_{up}$. The exact mechanism of generating $\pi_{up}$, as well as verifying
$\pi_{up}$, is implemented by the validator backend.

One interesting property of the clock update validator is its _statelessness_.
Besides the permission table (which is either static or global information),
the validator does not maintain any state to perform request validation. Such
stateless property has critical implication on the design of certain validator
backends, which we will elaborate in subsection 4.4.

####  4.3.2. Local Ordering

The _monotonicity validator_ prohibits a process from generating concurrent
clocks, or equivalently, enforcing the local ordering property. The inputs to
$\fn{prove}()$ are similar to those of the update validator. Input probably
shouldn’t be the update function, but just the mapped clock value. The
validator stores a local table that maintains the highest clock value mapped
to each identifier $id$. It validates the request only if the process has the
permission to update $id$, the input clock $c$ is valid and contains a clock
value mapped to $id$ which is _no less_ than the mapped value in its local
table. If the request is validated, the validator updates its $id$ mapped
clock value to an increment of the mapped clock value in $c$, and generates a
proof $\pi_{mono}$. Unlike the update validator, the monotonicity validator is
_stateful_ since it maintains a clock value table across $\fn{prove}()$ calls.
We will discuss its implications to the validator backend in subsection 4.4.

####  4.3.3. Application-Specific Semantics

The _application validator_ enforces any additional restrictions the
application put on clock updates. Specifically, $\var{req}$ includes inputs to
a $\fn{Update}()$ invocation but without any signature. $\var{aux}$ contains
any application-specific information required to validate the $\fn{Update}()$
request. The validator runs pre-installed application validation function on
$\var{req}$ and $\var{aux}$. If the function returns true, the validator
outputs a proof $\pi_{app}$. The exact format of $\var{aux}$ and the
validation logic are installed on the validators prior to running the
application. We currently restrict the application validator to be
_stateless_. The application-specific validation function therefore is
required to be _pure_. As shown in section 5, stateless validation is
sufficient for a wide range of distributed applications.

Figure 3.  Validator backends. Add more descriptions to the caption.

###  4.4. Validator Backend

As shown in Figure 3, supports multiple forms of backends to generate and
verify proofs for each validator instance. We now elaborate the design of each
backend model.

####  4.4.1. Quorum Certificate

The quorum certificate (QC) validator backend consists of a group of servers.
Servers in the group are called _QC validator nodes_. We assume the group
contains $N$ QC validator nodes. At most $f$ of the nodes exhibits Byzantine
failures. A Byzantine node can behave arbitrarily, but does not have enough
computational power to subvert standard cryptographic algorithms. There exists
an external service that manages the group configuration, including nodes
joining and leaving the group. Standard techniques such as proof of stake can
be used to tolerate Sybil attacks. Details of the configuration service is out
of the scope of our work.

The group uses a $(t,N)$ threshold signature scheme to generate and verify
proofs. Some citations here. The choice of $t$ depends on the type of
validator frontend logic. Each validator node applies a distributed key
generation scheme to generate its own secrete, distribute shares of the
secrete, compute and distribute its part of the combined public key using
secrete shares, and generate the final public key by aggregating key parts.
Some citations here.

To get a validator proof, a process sends the type of validator frontend and
the input to $\fn{prove}()$, , $\var{req}$ and $\var{aux}$, to $t$ validator
nodes. Each node independently executes the frontend logic. If the frontend
check passes, the node performs the clock update function, creates a partial
signature of the output clock using its secret share, and sends the signed
clock to the requesting process. If the process fails to get replies or
receives conflicting clocks from the first $t$ nodes, the process contacts
other validator nodes from the group. It waits until it collects $t$ matching
clocks with partial signatures from distinct validator nodes. The process then
perform signature aggregation to combine the $t$ partial signatures into a
complete signature. The combined signature on the matching output clock forms
the validator proof. To validate a proof for the $\fn{check}()$ function, any
party in the system verifies the combined signature using the aggregated
public key from the group.

For stateless validators, the minimum $t$ in $(t,N)$ is $f+1$. Since the
validator does not need to maintain state across $\fn{prove}()$ invocations,
generating a valid proof only requires that _at least one_ of the partial
signatures with matching output clocks comes from an honest validator. With
$f$ Byzantine validators, setting $t$ to $f+1$ meets the requirement. Such $t$
size, however, is not sufficient for stateful validators. As each
$\fn{prove}()$ invocation needs to remember the state of all previous
successful $\fn{prove}()$ calls, every two $\fn{prove}()$ invocations need to
_intersect_ at one or more honest validators. This requirement can be
satisfied by setting $t$ to at least $\lceil\frac{N+f+1}{2}\rceil$. Is this
sufficient? Probably sufficient as long as a global view on a single point is
not required. For example, it is not sufficient if some application logic
specifies whether a clock can be issued is based on _all_ clocks that have
ever been issued to the id owner, by anyone. For mono it is probably not the
case. It only requires to consider the latest issued clock, not the even
earlier ones. Explain why we don’t need consensus for this.

Discuss the complexity when group membership changes. Need to rerun the key
generation scheme. The history of aggregated public keys must be recorded.
Since the frequency is low, can use consensus.

####  4.4.2. Trusted Hardware

A trusted execution environment (TEE) validator backend runs on a _single_
validator node with access to TEE hardware. The backend works on any existing
implementation of TEE, including ARM TrustZone (trustzone, ), Intel SGX (sgx,
), and AWS Nitro Enclaves (nitro, ). In this section, we provide a general
description of our TEE validator backend design that applies to different TEE
variants. A concrete implementation using Nitro Enclaves is illustrated in
section 6.

The code implementing the validator frontend logic is released to the public.
Any third party can independently verify the cryptographic hash of the code. A
validator node with access to TEE hardware creates and launches an enclave
image that runs the frontend code. To process a
$\fn{prove}(\var{req},\var{aux})$ call, the validator node passes the call
inputs to the running enclave. The exact information passing mechanism depends
on the TEE implementation. The enclave then performs the frontend logic on the
inputs. If the operation is properly validated, the enclave computes the
output clock, and requests an attestation document from the TEE hardware. The
attestation request includes the output clock as user data. The resulting
attestation document serves as the validator proof of the output clock.

To verify a proof in the $\fn{check}()$ function, any participant in the
system first validates the authenticity of the attestation document. Trust of
the attestation certificate authority is established through external
mechanisms (, AWS root certificate). Once the document is authenticated, the
verifier checks that the enclave image in the document matches the hash of the
publicly available frontend code. It then validates that the clock matches the
user data field in the document. The verifier outputs $\var{true}$ only if
these tests all pass.

Unlike the QC backend, _any single_ TEE validator can generate proofs for
stateless validator frontends. A valid attestation document guarantees that
the clock is verified by a correct program that implements the requested
frontend logic. The trusted computing base (TCB), in this case, is reduced to
the TEE hardware and its root of trust (, Intel, ARM, or AWS). Implementing
stateful frontends, however, still requires a quorum out of $N$ TEE
validators, as the latest state might be lost when using a single validator.
But since no TEE validator can produce erroneous outputs, only a simple
majority of matching validator outputs, , $\lceil\frac{N+1}{2}\rceil$, is
required to generate a proof for stateful frontends.

####  4.4.3. Verifiable Computation

Figure 4.  Design of verifiable computation based validator backend.

The VC backend runs the entire frontend logic using verifiable computation
(VC). Our _recursive verifiability_ requirement puts restrictions on the type
of VC that we can use. Specifically, the update validator needs to verify
multiple input clock proofs; this requires a proof carrying data (PCD) (pcd, )
supported VC technique, such as recursive SNARK (snarks, ) and HyperNova
(hypernova, ). For stateless validators, any general VC solution also apply.
However, due to the limitation of VC, stateful validators cannot be
implemented using a VC backend.

The frontend logic is first translated into arithmetic circuit. Figure 4 shows
the simplified circuit architecture of a clock update frontend. In the
circuit, a clock $c$ is updated by merging with one other clock $c_{1}$, and
both clocks hold counter values for 3 $id$s. The circuit takes four witnesses.
The first three are $c$, $c_{1}$ paired with their proofs, and the updated
$id$. These witnesses match the arguments of $\fn{Update}$, and will be used
during verification as well. The circuit additionally takes a committed value
for the updated $id$ as witness, to authenticate the processor’s identity. The
witnesses are not required during verification, but a proving process can only
be done if the processor can provide valid witnesses.

In the circuit, the two clock proofs are verified while the clock values are
maximized element wise. Next, the counter value mapped to $id$ will be
incremented using a group of muxs and a demuxs. The committed value is then
verified against the corresponding commitment programmed into circuit
statically. Lastly, a proof is generated along with the output clock value.

The circuit has only one public input, which is the output clock value. Any
participant can validate the clock by verifying the proof using the clock
value as public input. Similar to the trusted hardware backend, a single
execution of the VC is sufficient to generate proofs.

##  5\. Use Cases

In this section, we describe two use cases of : a mutual exclusion service and
a weakly consistent data store. Both systems are evaluated in section 7.

###  5.1. Mutual Exclusion

Add locking case

Our first use case is inspired by the mutual exclusion algorithm in Lamport’s
paper (lamport-clock, ). The system consists of $N$ processes and a shared
resource. Each process may request to access the shared resource. A mutual
exclusion distributed algorithm needs to satisfy the following properties:

  * •

_Mutual exclusion_ : Access to $r$ is granted to _at most one_ process at any
time.

  * •

_Ordered access_ : For any two resource access requests $r_{1}$, $r_{2}$ and
their respective logical clocks $c_{1}$ and $c_{2}$, if $c_{1}\prec c_{2}$,
then $r_{1}$ is granted before $r_{2}$. If $c_{1}\parallel c_{2}$, the two
requests can be granted in any order.

  * •

_Starvation free_ : If every process eventually releases the resource after it
is granted access, all access requests are eventually granted.

Starvation free is only possible if network is partially synchronous, and that
all nodes respond to messages. For the second point, can add incentive-based
solution in the discussion.

The ordered access property needs to be refined. A Byzantine node can always
use older logical clocks or concurrent clocks to gain unfair advantage. Need
to include some fairness property. Resource provider can always detect for it
through examining the proof right?

Given that Byzantine processes can ignore the mutual exclusion protocol and
access the shared resource at any time, we require the process accessing the
resource to present a _proof_ to demonstrate its eligibility. Owner of the
resource verifies the proof before granting it to the process, although
details of this interaction is out of the scope our protocol.

There are five message types in our protocol: Request for requesting the
shared resource, Reply for responding to Request, Release for releasing the
shared resource, Query for checking other processes, and Ack for responding to
Query. Each message is tagged with the identifier of the sending process and a
clock; a Reply message additionally contains a list of clocks, with the list
size equals the number of processes. Each process locally maintains a local
clock and a queue of Requests it has received (including from itself). It also
stores the most recent clock it has received from each other process.

We define a total order $\lessdot$ on the set of clocks. $\lessdot$ strictly
contains the partially ordered set $\prec$, i.e., if $c_{1}\prec c_{2}$ then
$c_{1}\lessdot c_{2}$. For concurrent clocks, $\lessdot$ defines some
arbitrary ordering rules. Details of the rules do not impact the core
properties of the protocol. Does it impact fairness?

When a process sends any message, it attaches its local clock $c$ into the
message. Upon receiving any message with a clock $c_{m}$, the process first
verifies $c_{m}$. It then updates its local clock $c$ to the result of
$\fn{Update}(id,c,[c_{m}])$. Do we care about duplicated messages? Safety-wise
it should still be fine.

To request access to the shared resource, a process broadcasts a Request
message and adds the message to its local queue. When a process $p$ receives a
Request $R$ with a valid clock $c_{r}$, it adds $R$ to the queue. If the
requesting process already had a Request in the queue, $p$ ignores $R$. For
each other process $q$, $p$ then waits until either it has a Request from $q$
in the queue, or its most recent known clock from $q$ happened after $c_{r}$
(by sending a Query message to $q$ and waits for the Ack). $p$ then responds
with a Reply message. The Reply message contains the clock of each Request
ordered before (by $\lessdot$) $c_{r}$ in the queue.

A process acquires the shared resource when the following conditions are met.
1) Its own Request has the smallest clock, ordered by $\lessdot$, among all
Requests in the queue. 2) It has received a message with a clock ordered after
(by $\prec$) its Request clock from every process.

To release the resource, a process removes its own Requests in the queue, and
broadcasts a Release message. Once a process receives a Release, it verifies
that the Release is ordered after its pending Request (if any) and any
Requests from the releasing process in its local queue. If the conditions are
met, the process removes all Requests from the releasing process in the queue.
Note that Requests and Releases from a single process is always totally
ordered. After a process $p$ receives a Release message from $q$, $p$ can
ignore further Requests from $q$ that is _not_ ordered after the Release.

To access the shared resource, a process presents an _acquisition proof_
containing its own Request, and either a Reply or a Release from every other
process. The resource owner validates the proof by checking that all Release
messages have clocks ordered after (by $\lessdot$) the Request. Moreover, for
each clock $c$ in each Reply’s clock list, the corresponding process has a
Release message in the proof.

###  5.2. Causally Consistent Data Store

Logical clocks have been used to build data stores that provide causal
consistency (cops, ). Here, we leverage to construct a similar data store that
tolerates Byzantine processes.

The system consists of $N$ servers, collectively implementing a distributed
key-value service. Each server maintains the entire key-value mappings, , the
key-value store is fully replicated on $N$ servers. Can add sharding support.
The service exposes $\fn{Get}(k)$ and $\fn{Put}(k,v)$ API calls to clients. It
provides causal consistency. Each $\fn{Put}$ implicitly contains all
previously retrieved object versions from $\fn{Get}()$ calls within the client
session. These object versions are _causal dependencies_ of the new object
version created by $\fn{Put}$. All $\fn{Get}()$ respect causal ordering: if a
client observes an object, it is guaranteed to later observe all its causally
dependent object versions (or more update-to-date versions).

Updated: hide clocks from user interface; transparently guarantee safety
Should we a. more formally define _observable_ or b. completely bypass the
concept of observable

Added.

Both of the APIs implicitly refers to and maintains a _session context_ on
client side, which is used to determine a range of dependent operations of
every operation. In a session, operations always causally depend and only
depend on all operations that are finished prior to their invocations. For
simplicity, all $\fn{Put}$ of a session happen sequentially.

The key space is divided into $N$ subspace, each assigned to a server. Clients
send $\fn{Put}$ requests to the server responsible for the key. This key
partitioning design is to eliminate conflict resolution. Byzantine servers can
still create conflicts. Other approaches are required to fix Byzantine
conflicts, such as slashing. Partitioning metadata is managed by a BFT
consensus protocol. However, $\fn{Get}$ requests can be sent to any of the $N$
servers.

Updated.

Each client maintains a _dependency clock_ for a session. Not talking about
the details of dependency clock is an incomplete clock while versioned
dependency clock is a complete clock yet. We need this distinction because
client can only do MERGE on dependency clock while server can do MERGE_AND_INC
on versioned dependency clock. Complete these details after clock section
update. The clock records the aggregated causal dependency of the session, and
is initialized with $\fn{Init}()$ at the beginning of the session. Unlike
other clocks where the clock value is considered opaque, individual counter of
a dependency clock may be individually checked during verification. Every key
corresponds to an $id$, and we use $c[id]$ to refer the counter value of $id$
in clock $c$. In a dependency clock $c$, $c[id]=ver$ means the operation
depends on the version $ver$ of the key $id$. A client can check whether the
result of a $\fn{Get}(k)$ fulfills the causality requirement by checking
whether the returned value has a version that is not older than $c[id]$ of its
dependency clock, where $id$ corresponds to $k$.

Added. Each server maintains a _versioned dependency clock_ associated with
the current value of each key. The versioned dependency clock has the same
definition as the dependency clock, except that for the $id$ that corresponds
to the mapping key, the counter $c[id]$ stores the version number of the key.

It’s easy to see that

  * •

Given a dependency clock $c$, if for every $id$, the versioned dependency
clock of the corresponded key shows that the version number is not less than
$c[id]$, then the server is _up-to-date_ regarding $c$, that is, everything
from now on happens on this server is logically ordered after all the
dependent operations involved in $c$. This is the prerequisite of serving
requests with dependency clock $c$.

  * •

If $\fn{Compare}$ shows that a versioned dependency clock $c$ is greater than
a dependency clock $c^{\prime}$, than the value clocked $c$ is considered to
be logically ordered after all the dependent operations involved in
$c^{\prime}$. This is the prerequisite of replying a $\fn{Put}$ request with
versioned dependency clock $c$.

Added. For a $\fn{Put}$ operation, the client attaches its current dependency
clock in the $\fn{Put}$ request. Server should reply both $\fn{Get}$ and
$\fn{Put}$ requests with a versioned dependency clock. For $\fn{Get}$, it is
the clock of the returned value $v$; for $\fn{Put}$, it is the newly created
clock for the requested $v$. Client first verifies the returned clock, then
checks for causal dependencies according to its local dependency clock $c$.
For $\fn{Get}(k)$ request, the returned value must have a version number that
is not less than $c[id]$ where $id$ corresponds to $k$. For $\fn{Put}$
request, the returned versioned dependency clock must be greater than the
local dependency clock ($AF$ in $\fn{Compare}()$). The server reply is only
accepted when both the clock is valid and the causal dependencies are
respected. Client then merges the returned clock into its local dependency
clock for the following operations.

Updated When server receives a client request, it first checks whether its
local state is up-to-date according to the definition above. The request is
rejected if the check fails. This is only the case when the session is served
by single server. Need more discussion on this. Also ”as long as” implies
necessary but not sufficient; the ”external causality” that happens to be able
to be satisfied is also covered here. Since causal dependencies are always
satisfied, server can immediately reply to the requests. For $\fn{Get}$
requests, server simply returns its stored value and its versioned dependency
clock. For $\fn{Put}$ requests, server creates a new clock by applying
$\fn{Update}()$, stores the created clock with the requested value, and
returns the clock to client. Clock operation name TBD.

The client signature on the dependency clock is used as (part of) the input of
the ”application blackbox” of $\fn{MergeInc}$. The application blackbox is not
mentioned at all in current text. Well, for good maybe.

Updated. Once a server installs a new versioned dependency clock and a value
for a key, it asynchronously propagates this key-value entry to all other
servers. Upon receiving the entry, a server need to ensure causal consistency.
It does so by first examines whether its local state is up-to-date based on
the versioned dependency clock. If not, it puts the propagated entry into
pending state. Otherwise, it can install the key, and recursively reexamine
and commits the pending propagated entries.

##  6\. Implementation

We have implemented the three validator backends as described in subsection
4.4. The QC backend uses the schnorrkel Rust library (schnorrkel, ) which
implements Schnorr signature on Ristretto compressed Ed25519 points. The
library provides half-aggregated (prepared) batch signature verification
functionality (chalkias2021non, ). It enables cryptographic overhead sublinear
to the number of signatures in a QC.

The trusted hardware backend is implemented on AWS Nitro Enclaves (nitro, ).
Nitro Enclaves use the same Nitro Hypervisor technology to isolate the vCPUs
and memory for an enclave from its parent instance. Enclaves establish secure
local socket connectivity (using Linux VSOCK) with their parent instances.
Nitro Enclaves also supports attestation: Using the Nitro Enclaves SDK, an
enclave can request a signed attestation document from the Nitro Hypervisor
that includes its unique measurements. The validator requests its own
measurements, platform configuration registers (PCRs), on startup. A clock
update is only considered to be valid if all the included clock are attested
with the same PCRs. To generate a proof, the validator requests an attestation
document from the hypervisor for the new clock value. The validator program is
built into an enclave image file, and is deployed with Docker using Nitro
Enclaves CLI.

The verifiable computation backend is implemented using Plonky2 (plonky2, ).
Leveraging the universal verification circuit present in Plonky2, we build a
clock circuit that verifies two input proofs which are proved by itself. maybe
add a gate breakdown here if has space We have implemented the update
validator logic in all backends; monotonic and application validators are left
as future work.

We implement the mutual exclusion use case atop a causal network protocol. The
causal network acts as a middlebox: For egress messages, it assigns the
process current logical clock to the messages; for ingress messages, it
updates the local clock using the clock update function. The application then
only considers message send and receive events with causal ordering. The
acquisition proof consists of configured number of Ed25519 signatures which
uses the same schnorrkel library as QC validator.

We implement COPS following the original protocol (cops, ). Our implementation
replicates asynchronously to remote clusters, while each local cluster works
as a replicated state machine using PBFT (pbft, ). The COPS-GT and COPS-CD
variants are omitted from our implementation.

The entire codebase is implemented with 6.5k lines of Rust code. The mutex and
COPS use cases take 595 and 585 lines of code respectively. The QC and Nitro
Enclave backends take 716 lines of code in total. The plonky2 backend takes
408 lines of code. The comparison PBFT implementation takes 1274 lines of
code.

##  7\. Evaluation

Implementation details of can be found in section 6. We performed end-to-end
evaluations on the two use cases (section 5) and micro-benchmarks on validator
backends (subsection 4.2). We set up realistic global P2P network for
performing our end-to-end evaluations. Identical instances are spawned across
5 AWS regions (ap-east-1, us-west-1, eu-central-1, sa-east-1 and af-south-1).
The instances are interconnected through public Internet even in the same
region. We compare with our own PBFT (pbft, ) implementation in end-to-end
evaluations. PBFT is used as a Byzantine fault-tolerant ordering service that
provides _total ordering_.

In end-to-end evaluations, we evaluate using both QC and TEE validator
backends. That only verify the basic properties. For QC, we spawn two
c5a.16xlarge instances in each region to simulate a validator that has
sufficient computation and network resources. We set the quorum size to two to
tolerate one faulty quorum member.

###  7.1. Mutex Latency

Figure 5.  Resource acquisition latencies in the mutex use case.

We first study the latency of the mutex protocol (subsection 5.1) with varying
number of processes. We spawn a c5a.xlarge instance with four vCPUs for each
process, and evaluate the QC and Nitro Enclaves backends. Two of the four
vCPUs are allocated to Nitro Enclaves. We additionally spawn two c5a.8xlarge
instances with 32 vCPUs per region for quorum nodes.

Figure 5 compares with two other systems: the baseline original protocol
(lamport-clock, ) which tolerates no Byzantine failures, and a protocol where
processes communicate through PBFT-based broadcast so that messages are
received in the same total order on all processes. We evaluated two scenarios:
only one of the processes keeps requesting the resource, and all processes
request simultaneously. In both cases, the process immediately release the
resource after it is successfully granted the lock.

In the single process request experiment, all four systems maintain near
constant latency. with QC backend achieves a latency that is virtually
identical to the baseline, and the Nitro Enclaves backend only induces
marginal additional latency. In contrast, PBFT has significantly higher
latency due to its sequential nature. Although it can merge RequestOk messages
into one batch to avoid growing latencies, every point-to-point message
requiring two all-to-all PBFT message rounds still leads to amplified latency.

When all processes are contending for resources, request latency can be
divided into two phases: before and after the first process is granted with
the resource. The former phase is complete concurrent. A system with better
concurrency can reduce the average latency of this phase. The second phase is
complete sequential. A system with shorter step latency can benefit from this
phase, resulting in a smaller latency standard deviation. As shown in the
Figure 5, PBFT performs subpar in both phases. The two variants of , while
achieves similar standard deviation as the baseline, experiences significant
longer average latency. This is due to the quadratic per-process workload
required for generating acquisition proofs. We argue that this cost is
justifiable for tolerating Byzantine behaviors.

###  7.2. Causal Consistency Data Store

Figure 6. The throughput-latency relation of causal consistency data store
under different workload. The same results are plotted with different latency
range.

Next, we evaluate the throughput of our logical-clock-based causally
consistent data store (subsection 5.2). We deploy five causally consistent
replicas, one in each region, on c5a.8xlarge instances with 32 vCPUs and 10
Gbps network. We also evaluate the QC and Nitro Enclaves backends in this
evaluation. On each replica, 20 vCPUs are preserved for enclaves throughout
the evaluation. We set up two quorum instances per region with the same spec
as the mutex evaluation.

The system described in the original paper (cops, ) is used as the unsafe
baseline. We also directly compare to a geo-replicated PBFT deployment. The
PBFT protocol replicates every Get and Put to all regions, and the total order
of all requests fulfill the causal consistency requirement. Notice that the
security model of PBFT is difference from . PBFT can only tolerate one faulty
replica among the total five replicas, while can still ensure causality even
if all five replicas are faulty. On the other hand, PBFT can ensure stronger
availability, while can only tolerate causality related faulty behaviors.

We use a mix of YCSB workload A (50:50 read/write) and C (read-only) to
control the overall read/write ratio of the workload. Workload A is modified
to uniformly distribute access across local keys following the original work
(cops, ). We use the workload with 1% of write requests by default.

Figure 6 shows the 99.9th latency of all evaluated systems. PBFT is not
comparable to the other systems in both throughput and latency. For latency,
each request must reach every region before the reply can be generated, while
in all other systems only reply from the local replica is needed. For
throughput, although our PBFT implementation already amortizes the replication
overhead using batch size of 100, the protocol complexity still exposes
significantly higher overhead than weaker consistency models. This is
particularly true for the Get requests, which only require simple hashmap
lookups in other systems.

We then zoom into the results of the unsafe baseline and the two variants.
Although the Nitro Enclaves backend incurs higher minimal latency due to
hardware factors, the system eventually saturates at around 200Kop/s. This
performance is close to that of the QC backend, since the two variants share
the same COPS implementation, so the critical protocol path is identical. With
sufficient computational resources on the backends, we should expect other
backend variants to achieve similar throughput.

Figure 7. Normalized maximum throughput when deploying across difference
number of regions.

Figure 8. Maximum throughput under workloads of different read/write ratios.

Figure 8 shows the maximum throughput when deploying all systems with
increasing number of regions. The results are normalized to the maximum
throughput of the same system when deployed in only af-south-1 region. As
expected, both the unsafe baseline and the variants of perfectly scale against
the number of regions, because all cross region communication are asynchronous
and not on the critical path. On the contrary, PBFT does not scale. Its
performance even drops slightly when going beyond a single region, which is
attributed to the overhead introduced by imperfect network conditions (,
reordering).

The Figure 8 shows the throughput of the systems under workloads with
different read/write ratios. Both and unsafe baseline encounter performance
degradation when there are more write requests, due to the more complex code
path for handling Put. The QC variant can maintain higher throughput than PBFT
with less than 20% Put requests in the workload, while Nitro Enclaves variant
drops below PBFT with 5% Put, as the computation inside enclaves becomes the
system bottleneck. The bottleneck, however, can be eliminated by provisioning
more resources to the Nitro Enclaves backend.

###  7.3. Micro-benchmarks

Figure 9. Proving time with varying clock size and number of clock merged into
the updated clock. The circuit variant is measured with 64 CPUs.

In our first set of micro-benchmarks, we explore the factors that affect
backend performance with fixed computational resource. The first factor is the
clock size, which means how many $id$s the clock is keeping track of the
causal dependencies. For circuit backend, the maximum clock size must be
hardcoded ahead of time in order to synthesis arithmetic circuit accordingly,
and the backend will always keep track of all $id$s no matter they are
occupied or not. So in this evaluation, we build circuits for different
configured maximum clock sizes and perform update operation on them. As for
quorum and Nitro Enclaves backends, the map-based clock data structure allows
dynamically adding more $id$s, so we preload the clocks with the expected
number of $id$s before measurement.

All three variants maintain constant proving time before clock size grows over
certain threshold. Before start to grow, circuit variant has second level
latency, while both quorum and Nitro Enclaves variants have millisecond level
latency. Quorum variant’s latency increases faster than Nitro Enclaves variant
due to lower throughput transmitting to remote quorum node compare to Nitro
Enclaves’ local Vsock connection even in the absence of concurrency.

The second studied factor is the number of merged clocks inputted into Update
operation. Circuit cannot take varying number of merged clocks as input due
the limitation of verifiable computation must be finished in fixed number of
steps, so we focus on the other two variants in this micro-benchmark. The
results from both variants show linearly growing latency regarding the number
of merged clocks.

Figure 10. Proving performance with varying computational resource.

In the next set of micro-benchmarks we study the backend performance under
varying computational resource. As shown in Figure 10, both circuit and Nitro
Enclaves backends scales with the number of CPUs. However, they cannot scale
perfectly as CPU number increases. For circuit backend, the sequential
computation will eventually dominate, and for Nitro Enclaves, the backend
eventually bottlenecks on the secure socket between host and VM. Both backend
can scale well up to 20-30 CPUs.

Figure 11. Proving time with different quorum size.

Lastly we also perform a dedicated micro-benchmark on the most performant
quorum variant, studying how the performance will be affected when tolerating
more and more faulty quorum members. The result shows a linear growth, mostly
due to the longer verification time of the quorum certificates that includes
more signatures, on both quorum and user side.

##  8\. Conclusion

In this work, we introduce a new logical clock system, . addresses key
limitations of prior approaches that fail to work in networks with Byzantine
participants. It includes a novel logical clock structure, , that builds atop
a _validator_ abstraction. The abstraction defines the semantics of correct
logical clock updates. Various backend implementations, each with different
security-performance trade-offs, then enforce these validator semantics. To
demonstrate the power of , we developed two concrete applications: a mutual
exclusion protocol and a causally consistent data store. Evaluation results
showed that is an attractive solution for building decentralized applications
and systems in an open P2P network.

## References

  * (1) J. Baker, C. Bond, J. C. Corbett, J. J. Furman, A. Khorlin, J. Larson, J.-M. Leon, Y. Li, A. Lloyd, and V. Yushprakh.  Megastore: Providing Scalable, Highly Available Storage for Interactive Services.  In Proceedings of the Conference on Innovative Data system Research, CIDR ’11, pages 223–234, Asilomar, California, 2011.
  * (2) K. P. Birman and T. A. Joseph.  Reliable Communication in the Presence of Failures.  ACM Trans. Comput. Syst., 5(1):47–76, Jan. 1987.
  * (3) N. Bitansky, R. Canetti, A. Chiesa, and E. Tromer.  From extractable collision resistance to succinct non-interactive arguments of knowledge, and back again.  In Proceedings of the 3rd Innovations in Theoretical Computer Science Conference, ITCS ’12, page 326–349, New York, NY, USA, 2012. Association for Computing Machinery.
  * (4) B. Braun, A. J. Feldman, Z. Ren, S. Setty, A. J. Blumberg, and M. Walfish.  Verifying Computations with State.  In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP ’13, pages 341–357, Farminton, Pennsylvania, 2013. Association for Computing Machinery.  Pantry.
  * (5) M. Burrows.  The Chubby Lock Service for Loosely-Coupled Distributed Systems.  In Proceedings of the 7th Symposium on Operating Systems Design and Implementation, OSDI ’06, pages 335–350, Seattle, Washington, 2006. USENIX Association.
  * (6) V. Buterin.  A Next-Generation Smart Contract and Decentralized Application Platform.  2014\.
  * (7) M. Castro and B. Liskov.  Practical Byzantine fault tolerance.  In Proceedings of Symposium on Operating Systems Design and Implementation, volume 99, pages 173–186, 1999.
  * (8) K. Chalkias, F. Garillot, Y. Kondi, and V. Nikolaenko.  Non-interactive half-aggregation of eddsa and variants of schnorr signatures.  In Cryptographers’ Track at the RSA Conference, pages 577–608. Springer, 2021.
  * (9) K. M. Chandy and L. Lamport.  Distributed Snapshots: Determining Global States of Distributed Systems.  ACM Trans. Comput. Syst., 3(1):63–75, Feb. 1985.
  * (10) F. Chang, J. Dean, S. Ghemawat, W. C. Hsieh, D. A. Wallach, M. Burrows, T. Chandra, A. Fikes, and R. E. Gruber.  Bigtable: A Distributed Storage System for Structured Data.  In Proceedings of the 7th Symposium on Operating Systems Design and Implementation, OSDI ’06, pages 205–218, Seattle, Washington, 2006. USENIX Association.
  * (11) A. Chiesa and E. Tromer.  Proof-carrying data and hearsay arguments from signature cards.  In A. C. Yao, editor, Innovations in Computer Science - ICS 2010, Tsinghua University, Beijing, China, January 5-7, 2010. Proceedings, pages 310–331. Tsinghua University Press, 2010.
  * (12) B.-G. Chun, P. Maniatis, S. Shenker, and J. Kubiatowicz.  Attested append-only memory: making adversaries stick to their word.  In Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, SOSP ’07, page 189–204, New York, NY, USA, 2007. Association for Computing Machinery.
  * (13) J. C. Corbett, J. Dean, M. Epstein, A. Fikes, C. Frost, J. J. Furman, S. Ghemawat, A. Gubarev, C. Heiser, P. Hochschild, W. Hsieh, S. Kanthak, E. Kogan, H. Li, A. Lloyd, S. Melnik, D. Mwaura, D. Nagle, S. Quinlan, R. Rao, L. Rolig, Y. Saito, M. Szymaniak, C. Taylor, R. Wang, and D. Woodford.  Spanner: Google’s Globally-Distributed Database.  In Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation, OSDI ’12, pages 251–264, Hollywood, CA, USA, 2012. USENIX Association.
  * (14) G. Danezis, L. Kokoris-Kogias, A. Sonnino, and A. Spiegelman.  Narwhal and tusk: a dag-based mempool and efficient bft consensus.  In Proceedings of the Seventeenth European Conference on Computer Systems, EuroSys ’22, page 34–50, New York, NY, USA, 2022. Association for Computing Machinery.
  * (15) G. DeCandia, D. Hastorun, M. Jampani, G. Kakulapati, A. Lakshman, A. Pilchin, S. Sivasubramanian, P. Vosshall, and W. Vogels.  Dynamo: Amazon’s Highly Available Key-Value Store.  In Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, SOSP ’07, pages 205–220, Stevenson, Washington, USA, 2007. Association for Computing Machinery.
  * (16) M. J. Fischer, N. A. Lynch, and M. S. Paterson.  Impossibility of Distributed Consensus with One Faulty Process.  Journal of the ACM, 32(2):374–382, Apr. 1985.  FLP.
  * (17) S. Ghemawat, H. Gobioff, and S.-T. Leung.  The Google File System.  In Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles, SOSP ’03, pages 29–43, Bolton Landing, NY, USA, 2003. Association for Computing Machinery.
  * (18) B. Guo, Z. Lu, Q. Tang, J. Xu, and Z. Zhang.  Dumbo: Faster asynchronous bft protocols.  In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, CCS ’20, page 803–818, New York, NY, USA, 2020. Association for Computing Machinery.
  * (19) A. Hastings.  Distributed lock management in a transaction processing environment.  In Proceedings Ninth Symposium on Reliable Distributed Systems, pages 22–31, 1990.
  * (20) A. Kothapalli and S. Setty.  Hypernova: Recursive arguments for customizable constraint systems.  Cryptology ePrint Archive, 2023.
  * (21) R. Kotla, L. Alvisi, M. Dahlin, A. Clement, and E. Wong.  Zyzzyva: Speculative Byzantine Fault Tolerance.  In Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, SOSP ’07, pages 45–58, Stevenson, Washington, USA, 2007. Association for Computing Machinery.
  * (22) L. Lamport.  Time, Clocks, and the Ordering of Events in a Distributed System.  Commun. ACM, 21(7), July 1978.
  * (23) L. Lamport.  Paxos Made Simple.  ACM SIGACT News, 32(4):51–58, Dec. 2001.
  * (24) L. Lamport, R. Shostak, and M. Pease.  The Byzantine Generals Problem.  ACM Trans. Program. Lang. Syst., 4(3):382–401, July 1982.
  * (25) D. Levin, J. R. Douceur, J. R. Lorch, and T. Moscibroda.  TrInc: Small trusted hardware for large distributed systems.  In 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI 09), Boston, MA, Apr. 2009. USENIX Association.
  * (26) J. Li, J. Nelson, E. Michael, X. Jin, and D. R. K. Ports.  Pegasus: Tolerating Skewed Workloads in Distributed Storage with In-Network Coherence Directories.  In 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI ’20, pages 387–406. USENIX Association, Nov. 2020\.
  * (27) W. Lloyd, M. J. Freedman, M. Kaminsky, and D. G. Andersen.  Don’t settle for Eventual: Scalable Causal Consistency for Wide-Area Storage with COPS.  In Proceedings of the 23rd ACM Symposium on Operating Systems Principles, SOSP ’11, Cascais, Portugal, Oct. 2011.  COPS.
  * (28) U. Mathur, A. Pavlogiannis, H. C. Tunç, and M. Viswanathan.  A tree clock data structure for causal orderings in concurrent executions.  In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS ’22, page 710–725, New York, NY, USA, 2022. Association for Computing Machinery.
  * (29) F. Mattern.  Virtual time and global states of distributed systems.  In Parallel and Distributed Algorithms, pages 215–226. North-Holland, 1989.
  * (30) A. Miller, Y. Xia, K. Croman, E. Shi, and D. Song.  The Honey Badger of BFT Protocols.  In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, CCS ’16, pages 31–42, Vienna, Austria, 2016. Association for Computing Machinery.  HoneyBadgerBFT.
  * (31) S. Nakamoto.  Bitcoin: A peer-to-peer electronic cash system.  2009\.
  * (32) AWS Nitro Enclaves.  https://aws.amazon.com/ec2/nitro/nitro-enclaves/.
  * (33) B. M. Oki and B. H. Liskov.  Viewstamped Replication: A New Primary Copy Method to Support Highly-Available Distributed Systems.  In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, PODC ’88, pages 8–17, Toronto, Ontario, Canada, 1988. Association for Computing Machinery.
  * (34) D. Ongaro and J. Ousterhout.  In Search of an Understandable Consensus Algorithm.  In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference, USENIX ATC ’14, pages 305–320, Philadelphia, PA, 2014. USENIX Association.
  * (35) B. Parno, J. Howell, C. Gentry, and M. Raykova.  Pinocchio: nearly practical verifiable computation.  Commun. ACM, 59(2):103–112, jan 2016.
  * (36) Plonky2: Fast recursive arguments with PLONK and FRI.  https://github.com/0xPolygonZero/plonky2/blob/main/plonky2/plonky2.pdf.
  * (37) L. Ramabaja.  The bloom clock.  arXiv 1905.13064, 2019.
  * (38) A. Schiper, J. Eggli, and A. Sandoz.  A new algorithm to implement causal ordering.  In Proceedings of the 3rd International Workshop on Distributed Algorithms, page 219–232, Berlin, Heidelberg, 1989. Springer-Verlag.
  * (39) F. B. Schneider.  Implementing Fault-Tolerant Services Using the State Machine Approach: A Tutorial.  ACM Comput. Surv., 22(4):299–319, Dec. 1990.
  * (40) schnorrkel rust library.  https://docs.rs/schnorrkel/latest/schnorrkel/.
  * (41) R. Schwarz and F. Mattern.  Detecting causal relationships in distributed computations: In search of the holy grail.  Distributed Computing, 7(3):149–174, Mar. 1994.
  * (42) S. Setty, B. Braun, V. Vu, A. J. Blumberg, B. Parno, and M. Walfish.  Resolving the conflict between generality and plausibility in verified computation.  In Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys ’13, page 71–84, New York, NY, USA, 2013. Association for Computing Machinery.
  * (43) Intel software guard extensions.  https://www.intel.com/content/www/us/en/products/docs/accelerator-engines/software-guard-extensions.html.
  * (44) S. W. Smith and J. Tygar.  Signed vector timestamps: A secure protocol for partial order time.  CMU Technical Report, Oct. 1991.
  * (45) Trusted execution environment.  https://en.wikipedia.org/wiki/Trusted_execution_environment.
  * (46) D. B. Terry, M. M. Theimer, K. Petersen, A. J. Demers, M. J. Spreitzer, and C. H. Hauser.  Managing update conflicts in bayou, a weakly connected replicated storage system.  In Proceedings of the Fifteenth ACM Symposium on Operating Systems Principles, SOSP ’95, page 172–182, New York, NY, USA, 1995. Association for Computing Machinery.
  * (47) A. Thomson, T. Diamond, S.-C. Weng, K. Ren, P. Shao, and D. J. Abadi.  Calvin: Fast Distributed Transactions for Partitioned Database Systems.  In Proceedings of the 2012 ACM SIGMOD International Conference on Management of Data, SIGMOD ’12, pages 1–12, Scottsdale, Arizona, USA, 2012. Association for Computing Machinery.
  * (48) F. J. Torres-Rojas and M. Ahamad.  Plausible Clocks: Constant Size Logical Clocks for Distributed Systems.  Distrib. Comput., 12(4):179–195, Sept. 1999.  Place: Berlin, Heidelberg Publisher: Springer-Verlag.
  * (49) Trusted platform module.  https://en.wikipedia.org/wiki/Trusted_Platform_Module.
  * (50) ARM TrustZone.  https://www.arm.com/technologies/trustzone-for-cortex-a.
  * (51) G. S. Veronese, M. Correia, A. N. Bessani, L. C. Lung, and P. Verissimo.  Efficient Byzantine Fault-Tolerance.  IEEE Transactions on Computers, 62(1):16–30, 2013.  MinBFT.
  * (52) S. A. Weil, S. A. Brandt, E. L. Miller, D. D. E. Long, and C. Maltzahn.  Ceph: A Scalable, High-Performance Distributed File System.  In Proceedings of the 7th Symposium on Operating Systems Design and Implementation, OSDI ’06, pages 307–320, Seattle, Washington, 2006. USENIX Association.
  * (53) M. Yin, D. Malkhi, M. K. Reiter, G. G. Gueta, and I. Abraham.  HotStuff: BFT Consensus with Linearity and Responsiveness.  In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC ’19, pages 347–356, Toronto ON, Canada, 2019\. Association for Computing Machinery.
  * (54) H. Yu.  Design and evaluation of a continuous consistency model for replicated services.  In Fourth Symposium on Operating Systems Design and Implementation (OSDI 2000), San Diego, CA, Oct. 2000. USENIX Association.
  * (55) Z. Yu, Y. Zhang, V. Braverman, M. Chowdhury, and X. Jin.  Netlock: Fast, centralized lock management using programmable switches.  In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM ’20, page 126–138, New York, NY, USA, 2020. Association for Computing Machinery.