Towards a Verified Model of the Algorand Consensus Protocol in Coq

TL;DR

This paper presents a formal Coq model of the Algorand consensus protocol, incorporating timing and adversarial factors, and proves its asynchronous safety in a realistic environment.

Contribution

It is the first to model and verify Algorand's protocol with timing and adversarial considerations in Coq, ensuring safety properties.

Findings

Proved asynchronous safety of Algorand in the model

Model includes timing issues and adversarial actions

Demonstrated the potential for verifying additional properties

Abstract

The Algorand blockchain is a secure and decentralized public ledger based on pure proof of stake rather than proof of work. At its core it is a novel consensus protocol with exactly one block certified in each round: that is, the protocol guarantees that the blockchain does not fork. In this paper, we report on our effort to model and formally verify the Algorand consensus protocol in the Coq proof assistant. Similar to previous consensus protocol verification efforts, we model the protocol as a state transition system and reason over reachable global states. However, in contrast to previous work, our model explicitly incorporates timing issues (e.g., timeouts and network delays) and adversarial actions, reflecting a more realistic environment faced by a public blockchain. Thus far, we have proved asynchronous safety of the protocol: two different blocks cannot be certified in the same round, even when the adversary has complete control of message delivery in the network. We believe that our model is sufficiently general and other relevant properties of the protocol such as liveness can be proved for the same model.

Full text

Thus far, we have proved asynchronous safety of the protocol: two different blocks cannot be certified in the same round, even when the adversary has complete control of message delivery in the network. We believe that our model is sufficiently general and other relevant properties of the protocol such as liveness can be proved for the same model.

1 Introduction

The Algorand blockchain is a scalable and permissionless public ledger for secure and decentralized digital currencies and transactions. To determine the next block, it uses a novel consensus protocol [1, 3] based on pure proof of stake. In contrast to Bitcoin [6] and other blockchains based on proof of work, where safety is achieved by making it computationally expensive to add blocks, Algorand’s consensus protocol is highly efficient and does not require solving cryptographic puzzles. Instead, it uses cryptographic self-selection, which allows each user to individually determine whether it is selected into the committees responsible for generating the next block. The self-selection is done independently by every participant, with probability proportional to its stake. Private communication channels are not needed; committees propagate their messages in public. They reach Byzantine consensus on the next block and certify it, so that all users learn the next block without ambiguity. That is, rather than waiting for a long time so as to be sure that a block will not disappear from the longest chain, as in Bitcoin, the Algorand blockchain does not fork: a certified block is immediately final, and transactions contained in it can be relied upon right away. The Algorand blockchain guarantees fast generation of blocks as long as the underlying propagation network is not partitioned (i.e., as long as messages are delivered in a timely fashion). The Algorand consensus protocol, its core technology, and mathematical proofs of its safety and liveness properties are described in [1, 2, 3].

The focus of this work is to formally model and verify the Algorand consensus protocol (described in [2, 3]) using the Coq proof assistant. Automated formal verification of desired properties adds another level of assurance about its correctness, and developing a precise model to capture the protocol’s runtime environment and the assumptions it depends on is interesting from a formal-methods perspective as well. For example, [11] proves state machine safety and linearizability for the Raft consensus protocol in a non-Byzantine setting, and [7] focuses on safety properties of blockchains and, using a largest-chain-based fork-choice rule and a clique network topology, proves eventual consistency for an abstract parameterized protocol. Similar to previous work, we define a transition system relation on global protocol states and reason inductively over traces of states reachable via the relation from some initial state. We abstract away details on cryptographic primitives, modeling them as functions with the desired properties. We also omit details related to blockchain transactions and currencies.

However, our goal and various aspects of the Algorand protocol present new challenges. First, our goal is to verify the protocol’s asynchronous safety under Byzantine faults. Thus, we explicitly allow arbitrary adversarial actions, such as user corruption and message replay. Also, rather than assuming a particular network topology, the Algorand protocol assumes that messages are delivered within given real-valued deadlines when the network is not partitioned (messages may be arbitrarily delayed and their delivery is fully controlled by the adversary when the network is partitioned). We capture this by explicitly modeling global time progression and message delivery deadlines in the underlying propagation network. Moreover, as mentioned above, the Algorand protocol uses cryptographic self-selection to randomly select committees responsible for generating blocks. As mechanizing probabilistic analysis is still an open field in formal verification, instead of trying to fully capture randomized committee selection, we identify properties of the committees that are used to verify the correctness of the protocol without reference to the protocol itself. We then express these properties as axioms in our formal model. Pen-and-paper proofs that these properties hold (with overwhelming probability) can be found in [1, 3].

It is worth pointing out that our approach is based on reasoning about global states, in contrast to [8], which formally verifies the PBFT protocol underarbitrary local actions. While it is possible to model coordinated actions as in [8], our model explicitly allows an adversary to arbitrarily coordinate actions (at the network level) among corrupted users using both newly forged and valid past messages. Finally, [10] uses distributed separation logic for consensus protocol verification in Coq with non-Byzantine failures. Using this approach to verify protocols under Byzantine faults is an interesting avenue of future work.

Thus far, we have proved in Coq asynchronous safety: two different blocks can never be certified in the same round, even when the adversary has complete control of the network. We believe that our model is sufficiently general to allow other relevant properties of the protocol such as liveness to be proved.

2 The Algorand Consensus Protocol

In this section, we give a brief overview of the Algorand consensus protocol with details salient to our formal model. More details can be found in [1, 3, 5].

All users participating in the protocol have unique identifiers (public keys). The protocol proceeds in rounds and each user learns a certified block for each round. Rounds are asynchronous: each user individually starts a new round whenever it learns a certified block for its current round.

A round consists of one or more periods, which are attempts to generate a certified block. A period consists of several steps: users propose blocks and then vote to certify a proposal. Specifically, each user waits a fixed amount of time (determined by network parameters) to receive proposals, and then votes to support the proposal with the best credential, as described below; these votes are called soft-votes. If it receives a quorum of soft-votes, it then votes to certify the block; these votes are called cert-votes. A user considers a block certified if it receives a quorum of cert-votes. If a user doesn’t receive a quorum of cert-votes within a certain amount of time, it votes to begin a new period; these votes are called next-votes. A next-vote may be for a proposal, if the user received a quorum of soft-votes for it, or it may be open. A user begins a new period when it receives a quorum of next-votes from the same step for the same proposal or a quorum of open next-votes; and repeats the next-vote logic otherwise.

Committees.

For scalability, not all users send their messages in every step. Instead, a committee is randomly selected for each step via a technique called cryptographic self-selection: each user independently determines whether it is in the committee using a verifiable random function (VRF). Only users in the committee send messages for that step, along with a credential generated by the VRF to prove they are selected. Credentials are totally ordered, and the ones accompanying proposals are used to determine which proposal to support.

Network.

Users communicate by propagating messages over the network. Message delivery is asynchronous and may be out-of-order, but delivery times are bounded: any message sent or received by an honest user is received by all honest users within a fixed amount of time unless the network is partitioned. (There is no bound on message delivery time if the network is partitioned.)

Adversary.

The adversary can corrupt any user and control and coordinate corrupted users’ actions: for example, to resend old messages, send any message for future steps of the adversary’s choice, and decide when and to whom the messages are sent by them. The adversary also controls when messages are delivered between honest users within the bounds described above, and fully controls message delivery when the network is partitioned. The adversary must control less than 1/3 of the total stake participating in the consensus protocol.

3 Model

Our Coq model of the protocol, which is an abstracted version of the latest Algorand consensus protocol described in [2, 3], is a transition system encoded as an inductive binary relation on global states. The transition relation is parameterized on finite types of user identifiers (UserId) and values (Value); the latter abstractly represents blocks and block hashes.

User and Global State.

We represent both user state and global state as Coq records. For brevity, we omit a few components of the user state in this paper and only show some key ones, such as the Boolean indicating whether a user is corrupt, the local time, round, period, step, and blocks and cert-votes that have been observed. The global state has the global time, user states and messages via finite maps [4], and a Boolean indicating whether the network is partitioned.

⬇

Record UState := mkUState {

corrupt: bool; timer: R;

round: $\mathbb{N}~{}$; period: $\mathbb{N}~{}$; step: $\mathbb{N}~{}$;

blocks: $\mathbb{N}~{}$ $\to~{}$ seq Value;

certvotes: $\mathbb{N}~{}$ $\to~{}$ $\mathbb{N}~{}$ $\to~{}$ seq Vote;

(* ... omitted ... *)

}.

⬇

Record GState := mkGState {

network_partition: bool;

now: R;

users: {fmap UserId $\to~{}$ UState};

msgs: {fmap UserId $\to~{}$ {mset R * Msg}};

msg_history: {mset Msg};

}.

State Transition System.

The transition relation on global states g and g’, written g $\!\rightsquigarrow\;$ g’, is defined in the usual way via inductive rules. For example, the rule for adversary message replay is as follows:

⬇

step_replay_msg : $\forall~{}$ (pre:GState) uid (ustate_key : uid \in pre.(users)) msg,

$\lnot\;$ pre.(users).[ustate_key].(corrupt) $\to~{}$ msg \in pre.(msg_history) $\to~{}$

pre $\!\rightsquigarrow\;$ replay_msg_result pre uid msg

Here, replay_msg_result is a function that builds a global state where msg is broadcast. We call a sequence of global states a trace if it is nonempty and g $\!\rightsquigarrow\;$ g’ holds whenever g and g’ are adjacent in the sequence.

Assumptions.

To express assumptions about committees and quorums, we introduce a function committee that determines self-selected committees. For example, the following statement says that for any two quorums (i.e., subsets of size at least tau) of the committee for a given round-period-step triple, there is an honest user who belongs to both quorums:

⬇

Definition quorum_honest_overlap_statement (tau:$\mathbb{N}~{}$) :=

$\forall~{}$ (trace:seq GState) (r p s:$\mathbb{N}~{}$) (q1 q2:{fset UserId}),

q1 $\subseteq\;$ committee r p s $\to~{}$ #|q1| $\!\geq\;$ tau $\to~{}$

q2 $\subseteq\;$ committee r p s $\to~{}$ #|q2| $\!\geq\;$ tau $\to~{}$

$\exists~{}$ (honest_voter : UserId), honest_voter \in q1 /\ honest_voter \in q2 /\

honest_during_step (r,p,s) honest_voter trace.

Similarly, we capture that a block was certified in a period as follows (the value 3 indicates the third step, the certvote step, in period p and round r):

⬇

Definition certified_in_period (trace:seq GState) (tau r p:$\mathbb{N}~{}$) (v:Value) :=

$\exists~{}$ (certvote_quorum:{fset UserId}),

certvote_quorum $\subseteq\;$ committee r p 3 /\ #|certvote_quorum| $\!\geq\;$ tau /\

$\forall~{}$ (voter:UserId), voter \in certvote_quorum $\to~{}$

certvoted_in_path trace voter r p v.

This property is true for a trace if there exists a quorum of users selected for cert-voting who actually sent their votes in that trace for the given period (via certvoted_in_path, which we omit). This is without loss of generality since a corrupted user who did not send its cert-vote can be simulated by a corrupted user who sent its vote but the message is received by nobody.

4 Asynchronous Safety

The analysis of the protocol in the computational model shows that the probability of forking is negligible [1, 3]. In contrast, we specify and prove formally in the symbolic model with idealized cryptographic primitives that at most one block is certified in a round, even in the face of adversary control over message delivery and corruption of users. We call this property asynchronous safety:

⬇

Theorem asynchronous_safety : $\forall~{}$ (g0:GState) (trace:seq GState) (r:$\mathbb{N}~{}$),

state_before_round r g0 $\to~{}$ is_trace g0 trace $\to~{}$

$\forall~{}$ (p1:$\mathbb{N}~{}$) (v1:Value), certified_in_period trace r p1 v1 $\to~{}$

$\forall~{}$ (p2:$\mathbb{N}~{}$) (v2:Value), certified_in_period trace r p2 v2 $\to~{}$

v1 = v2.

Here, the first precondition state_before_round r g0 states that no user has taken any actions in round r in the initial global state g0, and the second precondition is_trace g0 trace states that trace follows $\!\rightsquigarrow\;$ and starts in g0.

Note that it is possible to end up with block certifications from multiple periods of a round. Specifically, during a network partition, which allows the adversary to delay messages, this can happen if cert-vote messages are delayed enough for some users to advance past the period where the first certification was produced. However, these multiple certifications will all be for the same block.

Proof Outline.

The proof of asynchronous safety proceeds by case-splitting on whether the certifications are from the same period or different periods. Forthe first and easiest case, p1 = p2, we use quorum hypotheses to establishthat there is an honest user that contributed a cert-vote to both certifications. Then, we conclude by applying the lemma no_two_certvotes_in_p, which establishes that an honest user u cert-votes at most once in a period (proved by exhaustive analysis of possible transitions by an honest node):

⬇

Lemma no_two_certvotes_in_p : $\forall~{}$ (g0:GState) (trace:seq GState) u (r p:$\mathbb{N}~{}$),

is_trace g0 trace $\to~{}$

$\forall~{}$ idx1 v1, certvoted_in_path_at idx1 trace u r p v1 $\to~{}$

user_honest_at idx1 trace u $\to~{}$

$\forall~{}$ idx2 v2, certvoted_in_path_at idx2 trace u r p v2 $\to~{}$

user_honest_at idx2 trace u $\to~{}$ idx1 = idx2 /\ v1 = v2.

The second case (p1 $\!\!\neq\;$ p2) uses an invariant which first holds in the period that produces the first certification, say, p1 for v1, and then keeps holding for all periods of the round. The invariant is that no step of the period produces a quorum of open next-votes, and any quorum of value next-votes must be for v1. (Please refer to [9] for the full definitions of predicates appearing in the lemma.)

5 Conclusion

We presented a model in Coq of the Algorand consensus protocol and outlined the specification and formal proof of its asynchronous safety. The model and the proof open up many possibilities for further formal verification of the protocol, most directly of liveness properties. Our Coq development is available on GitHub [9] and contains around 2000 specification lines and 4000 proof lines.