From 66e9106b4dbacdbf7911f3da9b3b5836f7313ba7 Mon Sep 17 00:00:00 2001 From: Giuliano Date: Mon, 9 Nov 2020 02:05:26 -0800 Subject: [PATCH] add Ivy proofs (#210) * add Ivy proofs * fix docker-compose command --- ivy-proofs/Dockerfile | 37 +++ ivy-proofs/README.md | 27 ++ ivy-proofs/abstract_tendermint.ivy | 173 +++++++++++ ivy-proofs/accountable_safety_1.ivy | 144 ++++++++++ ivy-proofs/accountable_safety_2.ivy | 52 ++++ ivy-proofs/check_proofs.sh | 38 +++ ivy-proofs/classic_safety.ivy | 85 ++++++ ivy-proofs/docker-compose.yml | 8 + ivy-proofs/domain_model.ivy | 90 ++++++ ivy-proofs/network_shim.ivy | 140 +++++++++ ivy-proofs/output/.gitignore | 4 + ivy-proofs/tendermint.ivy | 430 ++++++++++++++++++++++++++++ 12 files changed, 1228 insertions(+) create mode 100644 ivy-proofs/Dockerfile create mode 100644 ivy-proofs/README.md create mode 100644 ivy-proofs/abstract_tendermint.ivy create mode 100644 ivy-proofs/accountable_safety_1.ivy create mode 100644 ivy-proofs/accountable_safety_2.ivy create mode 100755 ivy-proofs/check_proofs.sh create mode 100644 ivy-proofs/classic_safety.ivy create mode 100644 ivy-proofs/docker-compose.yml create mode 100644 ivy-proofs/domain_model.ivy create mode 100644 ivy-proofs/network_shim.ivy create mode 100644 ivy-proofs/output/.gitignore create mode 100644 ivy-proofs/tendermint.ivy diff --git a/ivy-proofs/Dockerfile b/ivy-proofs/Dockerfile new file mode 100644 index 000000000..be60151fd --- /dev/null +++ b/ivy-proofs/Dockerfile @@ -0,0 +1,37 @@ +# we need python2 support, which was dropped after buster: +FROM debian:buster + +RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections +RUN apt-get update +RUN apt-get install -y apt-utils + +# Install and configure locale `en_US.UTF-8` +RUN apt-get install -y locales && \ + sed -i -e "s/# $en_US.*/en_US.UTF-8 UTF-8/" /etc/locale.gen && \ + dpkg-reconfigure --frontend=noninteractive locales && \ + update-locale LANG=en_US.UTF-8 +ENV LANG=en_US.UTF-8 + +RUN apt-get update +RUN apt-get install -y git python2 python-pip g++ cmake python-ply python-tk tix pkg-config libssl-dev python-setuptools + +# create a user: +RUN useradd -ms /bin/bash user +USER user +WORKDIR /home/user + +RUN git clone --recurse-submodules https://github.com/kenmcmil/ivy.git +WORKDIR /home/user/ivy/ +RUN git checkout 271ee38980699115508eb90a0dd01deeb750a94b + +RUN python2.7 build_submodules.py +RUN mkdir -p "/home/user/python/lib/python2.7/site-packages" +ENV PYTHONPATH="/home/user/python/lib/python2.7/site-packages" +# need to install pyparsing manually because otherwise wrong version found +RUN pip install pyparsing +RUN python2.7 setup.py install --prefix="/home/user/python/" +ENV PATH=$PATH:"/home/user/python/bin/" +WORKDIR /home/user/tendermint-proof/ + +ENTRYPOINT ["/home/user/tendermint-proof/check_proofs.sh"] + diff --git a/ivy-proofs/README.md b/ivy-proofs/README.md new file mode 100644 index 000000000..80dc0ce7b --- /dev/null +++ b/ivy-proofs/README.md @@ -0,0 +1,27 @@ +``` +Copyright (c) 2020 Galois, Inc. +SPDX-License-Identifier: Apache-2.0 +``` + +This folder contains: +* `tendermint.ivy`, a specification of Tendermint algorithm as described in *The latest gossip on BFT consensus* by E. Buchman, J. Kwon, Z. Milosevic. +* `abstract_tendermint.ivy`, a more abstract specification of Tendermint that is more verification-friendly. +* `classic_safety.ivy`, a proof that Tendermint satisfies the classic safety property of BFT consensus: if every two quorums have a well-behaved node in common, then no two well-behaved nodes ever disagree. +* `accountable_safety_1.ivy`, a proof that, assuming every quorum contains at least one well-behaved node, if two well-behaved nodes disagree, then there is evidence demonstrating at least f+1 nodes misbehaved. +* `accountable_safety_2.ivy`, a proof that, regardless of any assumption about quorums, well-behaved nodes cannot be framed by malicious nodes. In other words, malicious nodes can never construct evidence that incriminates a well-behaved node. +* `network_shim.ivy`, the network model and a convenience `shim` object to interface with the Tendermint specification. +* `domain_model.ivy`, a specification of the domain model underlying the Tendermint specification, i.e. rounds, value, quorums, etc. + +All specifications and proofs are written in [Ivy](https://github.com/kenmcmil/ivy). + +The license above applies to all files in this folder. + + +# Building and running +The easiest way to check the proofs is to use [Docker](https://www.docker.com/). + +1. Install [Docker](https://docs.docker.com/get-docker/) and [Docker Compose](https://docs.docker.com/compose/install/). +2. Build a Docker image: `docker-compose build` +3. Run the proofs inside the Docker container: `docker-compose run +tendermint-proof`. This will check all the proofs with the `ivy_check` +command and write the output of `ivy_check` to a subdirectory of `./output/' diff --git a/ivy-proofs/abstract_tendermint.ivy b/ivy-proofs/abstract_tendermint.ivy new file mode 100644 index 000000000..d0c0e8d5f --- /dev/null +++ b/ivy-proofs/abstract_tendermint.ivy @@ -0,0 +1,173 @@ +#lang ivy1.7 +# --- +# layout: page +# title: Abstract specification of Tendermint in Ivy +# --- + +# Here we define an abstract version of the Tendermint specification. We use +# two main forms of abstraction: a) We abstract over how information is +# transmitted (there is no network). b) We abstract functions using relations. +# For example, we abstract over a node's current round, instead only tracking +# with a relation which rounds the node has left. We do something similar for +# the `lockedRound` variable. This is in order to avoid using a function from +# node to round, and it allows us to emit verification conditions that are +# efficiently solvable by Z3. + +# This specification also defines the observations that are used to adjudicate +# misbehavior. Well-behaved nodes faithfully observe every message that they +# use to take a step, while Byzantine nodes can fake observations about +# themselves (including withholding observations). Misbehavior is defined using +# the collection of all observations made (in reality, those observations must +# be collected first, but we do not model this process). + +include domain_model + +module abstract_tendermint = { + +# Protocol state +# ############## + + relation left_round(N:node, R:round) + relation prevoted(N:node, R:round, V:value) + relation precommitted(N:node, R:round, V:value) + relation decided(N:node, R:round, V:value) + relation locked(N:node, R:round, V:value) + +# Accountability relations +# ######################## + + relation observed_prevoted(N:node, R:round, V:value) + relation observed_precommitted(N:node, R:round, V:value) + +# relations that are defined in terms of the previous two: + relation observed_equivocation(N:node) + relation observed_unlawful_prevote(N:node) + relation agreement + + object defs = { # we hide those definitions and use them only when needed + private { + definition [observed_equivocation_def] observed_equivocation(N) = exists V1,V2,R . + V1 ~= V2 & (observed_precommitted(N,R,V1) & observed_precommitted(N,R,V2) | observed_prevoted(N,R,V1) & observed_prevoted(N,R,V2)) + + definition [observed_unlawful_prevote_def] observed_unlawful_prevote(N) = exists V1,V2,R1,R2 . + V1 ~= value.nil & V2 ~= value.nil & V1 ~= V2 & R1 < R2 & observed_precommitted(N,R1,V1) & observed_prevoted(N,R2,V2) + & forall Q,R . R1 <= R & R < R2 & nset.is_quorum(Q) -> exists N2 . nset.member(N2,Q) & ~observed_prevoted(N2,R,V2) + + definition [agreement_def] agreement = forall N1,N2,R1,R2,V1,V2 . well_behaved(N1) & well_behaved(N2) & decided(N1,R1,V1) & decided(N2,R2,V2) -> V1 = V2 + } + } + +# Protocol transitions +# #################### + + after init { + left_round(N,R) := R < 0; + prevoted(N,R,V) := false; + precommitted(N,R,V) := false; + decided(N,R,V) := false; + locked(N,R,V) := false; + + observed_prevoted(N,R,V) := false; + observed_precommitted(N,R,V) := false; + } + +# Actions are named after the corresponding line numbers in the Tendermint +# arXiv paper. + + action l_11(n:node, r:round) = { # start round r + require ~left_round(n,r); + left_round(n,R) := R < r; + } + + action l_22(n:node, rp:round, v:value) = { + require ~left_round(n,rp); + require ~prevoted(n,rp,V) & ~precommitted(n,rp,V); + require (forall R,V . locked(n,R,V) -> V = v) | v = value.nil; + prevoted(n, rp, v) := true; + left_round(n, R) := R < rp; # leave all lower rounds. + + observed_prevoted(n, rp, v) := observed_prevoted(n, rp, v) | well_behaved(n); # the node observes itself + } + + action l_28(n:node, rp:round, v:value, vr:round, q:nset) = { + require ~left_round(n,rp) & ~prevoted(n,rp,V); + require ~prevoted(n,rp,V) & ~precommitted(n,rp,V); + require vr < rp; + require nset.is_quorum(q) & (forall N . nset.member(N,q) -> (prevoted(N,vr,v) | ~well_behaved(N))); + var proposal:value; + if value.valid(v) & ((forall R0,V0 . locked(n,R0,V0) -> R0 <= vr) | (forall R,V . locked(n,R,V) -> V = v)) { + proposal := v; + } + else { + proposal := value.nil; + }; + prevoted(n, rp, proposal) := true; + left_round(n, R) := R < rp; # leave all lower rounds + + observed_prevoted(N, vr, v) := observed_prevoted(N, vr, v) | (well_behaved(n) & nset.member(N,q)); # the node observes the prevotes of quorum q + observed_prevoted(n, rp, proposal) := observed_prevoted(n, rp, proposal) | well_behaved(n); # the node observes itself + } + + action l_36(n:node, rp:round, v:value, q:nset) = { + require v ~= value.nil; + require ~left_round(n,rp); + require exists V . prevoted(n,rp,V); + require ~precommitted(n,rp,V); + require nset.is_quorum(q) & (forall N . nset.member(N,q) -> (prevoted(N,rp,v) | ~well_behaved(N))); + precommitted(n, rp, v) := true; + left_round(n, R) := R < rp; # leave all lower rounds + locked(n,R,V) := R <= rp & V = v; + + observed_prevoted(N, rp, v) := observed_prevoted(N, rp, v) | (well_behaved(n) & nset.member(N,q)); # the node observes the prevotes of quorum q + observed_precommitted(n, rp, v) := observed_precommitted(n, rp, v) | well_behaved(n); # the node observes itself + } + + action l_44(n:node, rp:round, q:nset) = { + require ~left_round(n,rp); + require ~precommitted(n,rp,V); + require nset.is_quorum(q) & (forall N .nset.member(N,q) -> (prevoted(N,rp,value.nil) | ~well_behaved(N))); + precommitted(n, rp, value.nil) := true; + left_round(n, R) := R < rp; # leave all lower rounds + + observed_prevoted(N, rp, value.nil) := observed_prevoted(N, rp, value.nil) | (well_behaved(n) & nset.member(N,q)); # the node observes the prevotes of quorum q + observed_precommitted(n, rp, value.nil) := observed_precommitted(n, rp, value.nil) | well_behaved(n); # the node observes itself + } + + action l_57(n:node, rp:round) = { + require ~left_round(n,rp); + require ~prevoted(n,rp,V); + prevoted(n, rp, value.nil) := true; + left_round(n, R) := R < rp; # leave all lower rounds + + observed_prevoted(n, rp, value.nil) := observed_prevoted(n, rp, value.nil) | well_behaved(n); # the node observes itself + } + + action l_61(n:node, rp:round) = { + require ~left_round(n,rp); + require ~precommitted(n,rp,V); + precommitted(n, rp, value.nil) := true; + left_round(n, R) := R < rp; # leave all lower rounds + + observed_precommitted(n, rp, value.nil) := observed_precommitted(n, rp, value.nil) | well_behaved(n); # the node observes itself + } + + action decide(n:node, r:round, v:value, q:nset) = { + require v ~= value.nil; + require nset.is_quorum(q) & (forall N . nset.member(N, q) -> (precommitted(N, r, v) | ~well_behaved(N))); + decided(n, r, v) := true; + + observed_precommitted(N, r, v) := observed_precommitted(N, r, v) | (well_behaved(n) & nset.member(N,q)); # the node observes the precommits of quorum q + + } + + action misbehave = { +# Byzantine nodes can claim they observed whatever they want about themselves, +# but they cannot remove observations. + observed_prevoted(N,R,V) := *; + assume (old observed_prevoted(N,R,V)) -> observed_prevoted(N,R,V); + assume well_behaved(N) -> old observed_prevoted(N,R,V) = observed_prevoted(N,R,V); + observed_precommitted(N,R,V) := *; + assume (old observed_precommitted(N,R,V)) -> observed_precommitted(N,R,V); + assume well_behaved(N) -> old observed_precommitted(N,R,V) = observed_precommitted(N,R,V); + } +} diff --git a/ivy-proofs/accountable_safety_1.ivy b/ivy-proofs/accountable_safety_1.ivy new file mode 100644 index 000000000..dc083bb4d --- /dev/null +++ b/ivy-proofs/accountable_safety_1.ivy @@ -0,0 +1,144 @@ +#lang ivy1.7 +# --- +# layout: page +# title: Proof of Classic Safety +# --- + +include tendermint +include abstract_tendermint + +# Here we prove the first accountability property: if two well-behaved nodes +# disagree, then there are two quorums Q1 and Q2 such that all members of the +# intersection of Q1 and Q2 have violated the accountability properties. + +# The proof is done in two steps: first we prove the abstract specification +# satisfies the property, and then we show by refinement that this property +# also holds in the concrete specification. + +# To see what is checked in the refinement proof, use `ivy_show isolate=accountable_safety_1 accountable_safety_1.ivy` +# To see what is checked in the abstract correctness proof, use `ivy_show isolate=abstract_accountable_safety_1 accountable_safety_1.ivy` +# To check the whole proof, use `ivy_check accountable_safety_1.ivy`. + + +# Proof of the accountability property in the abstract specification +# ================================================================== + +# We prove with tactics (see `lemma_1` and `lemma_2`) that, if some basic +# invariants hold (see `invs` below), then the accountability property holds. + +isolate abstract_accountable_safety = { + + instantiate abstract_tendermint + +# The main property +# ----------------- + +# If there is disagreement, then there is evidence that a third of the nodes +# have violated the protocol: + invariant [accountability] agreement | exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & (forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N)) + proof { + apply lemma_2.thm # this reduces to goal to three subgoals: p1, p2, and p3 (see their definition below) + proof [p1] { + assume invs.inv1 + } + proof [p2] { + assume invs.inv2 + } + proof [p3] { + assume invs.inv3 + } + } + +# The invariants +# -------------- + + isolate invs = { + + # well-behaved nodes observe their own actions faithfully: + invariant [inv1] well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V)) + # if a value is precommitted by a well-behaved node, then a quorum is observed to prevote it: + invariant [inv2] (exists N . well_behaved(N) & precommitted(N,R,V)) & V ~= value.nil -> exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V) + # if a value is decided by a well-behaved node, then a quorum is observed to precommit it: + invariant [inv3] (exists N . well_behaved(N) & decided(N,R,V)) -> 0 <= R & V ~= value.nil & exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_precommitted(N2,R,V) + private { + invariant (precommitted(N,R,V) | prevoted(N,R,V)) -> 0 <= R + invariant R < 0 -> left_round(N,R) + } + + } with this, nset, round, accountable_bft.max_2f_byzantine + +# The theorems proved with tactics +# -------------------------------- + +# Using complete induction on rounds, we prove that, assuming that the +# invariants inv1, inv2, and inv3 hold, the accountability property holds. + +# For technical reasons, we separate the proof in two steps + isolate lemma_1 = { + +# complete induction is not built-in, so we introduce it with an axiom. Note that this only holds for a type where 0 is the smallest element + axiom [complete_induction] { + relation p(X:round) + { # base case + property p(0) + } + { # inductive step: show that if the property is true for all X lower or equal to x and y=x+1, then the property is true of y + individual a:round + individual b:round + property (forall X. 0 <= X & X <= a -> p(X)) & round.succ(a,b) -> p(b) + } + #-------------------------- + property forall X . 0 <= X -> p(X) + } + +# the main lemma: if inv1 and inv2 below hold and a quorum is observed to +# precommit V1 at R1 and another quorum is observed to precommit V2~=V1 at +# R2>=R1, then the intersection of two quorums (i.e. f+1 nodes) is observed to +# violate the protocol + theorem [thm] { + property [p1] forall N,R,V . well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V)) + property [p2] forall R,V . (exists N . well_behaved(N) & precommitted(N,R,V)) -> V = value.nil | exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V) + #----------------------------------------------------------------------------------------------------------------------- + property forall R2. 0 <= R2 -> ((exists V2,Q1,R1,V1,Q1 . V1 ~= value.nil & V2 ~= value.nil & V1 ~= V2 & 0 <= R1 & R1 <= R2 & nset.is_quorum(Q1) & (forall N . nset.member(N,Q1) -> observed_precommitted(N,R1,V1)) & (exists Q2 . nset.is_quorum(Q2) & forall N . nset.member(N,Q2) -> observed_prevoted(N,R2,V2))) -> exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N)) + } + proof { + apply complete_induction # the two subgoals (base case and inductive case) are then discharged automatically + } + } with this, round, nset, accountable_bft.max_2f_byzantine, defs.observed_equivocation_def, defs.observed_unlawful_prevote_def + +# Now we put lemma_1 in a form that matches exactly the accountability property +# we want to prove. This is a bit cumbersome and could probably be improved. + isolate lemma_2 = { + + theorem [thm] { + property [p1] forall N,R,V . well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V)) + property [p2] forall R,V . (exists N . well_behaved(N) & precommitted(N,R,V)) & V ~= value.nil -> exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V) + property [p3] forall R,V. (exists N . well_behaved(N) & decided(N,R,V)) -> 0 <= R & V ~= value.nil & exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_precommitted(N2,R,V) + #------------------------------------------------------------------------------------------------------------------------------------------- + property agreement | exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N) + } + proof { + assume lemma_1.thm + } + + } with this, round, defs.agreement_def, lemma_1, nset, accountable_bft.max_2f_byzantine + +} with round + +# The final proof +# =============== + +isolate accountable_safety_1 = { + +# First we instantiate the concrete protocol: + instantiate tendermint(abstract_accountable_safety) + +# We then define what we mean by agreement + relation agreement + definition [agreement_def] agreement = forall N1,N2. well_behaved(N1) & well_behaved(N2) & server.decision(N1) ~= value.nil & server.decision(N2) ~= value.nil -> server.decision(N1) = server.decision(N2) + + invariant abstract_accountable_safety.agreement -> agreement + + invariant [accountability] agreement | exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & forall N . nset.member(N,Q1) & nset.member(N,Q2) -> abstract_accountable_safety.observed_equivocation(N) | abstract_accountable_safety.observed_unlawful_prevote(N) + +} with value, round, proposers, shim, abstract_accountable_safety, abstract_accountable_safety.defs.agreement_def, accountable_safety_1.agreement_def diff --git a/ivy-proofs/accountable_safety_2.ivy b/ivy-proofs/accountable_safety_2.ivy new file mode 100644 index 000000000..5dd0a5bec --- /dev/null +++ b/ivy-proofs/accountable_safety_2.ivy @@ -0,0 +1,52 @@ +#lang ivy1.7 + +include tendermint +include abstract_tendermint + +# Here we prove the second accountability property: no well-behaved node is +# every observed to violate the accountability properties. + +# The proof is done in two steps: first we prove the the abstract specification +# satisfies the property, and then we show by refinement that this property +# also holds in the concrete specification. + +# To see what is checked in the refinement proof, use `ivy_show isolate=accountable_safety_2 accountable_safety_2.ivy` +# To see what is checked in the abstract correctness proof, use `ivy_show isolate=abstract_accountable_safety_2 accountable_safety_2.ivy` +# To check the whole proof, use `ivy_check accountable_safety_2.ivy`. + +# Proof that the property holds in the abstract specification +# ============================================================ + +isolate abstract_accountable_safety_2 = { + + instantiate abstract_tendermint + +# the main property: + invariant [wb_never_punished] well_behaved(N) -> ~(observed_equivocation(N) | observed_unlawful_prevote(N)) + +# the main invariant for proving wb_not_punished: + invariant well_behaved(N) & precommitted(N,R,V) & ~locked(N,R,V) & V ~= value.nil -> exists R2,V2 . V2 ~= value.nil & R < R2 & precommitted(N,R2,V2) & locked(N,R2,V2) + + invariant (exists N . well_behaved(N) & precommitted(N,R,V) & V ~= value.nil) -> exists Q . nset.is_quorum(Q) & forall N . nset.member(N,Q) -> observed_prevoted(N,R,V) + + invariant well_behaved(N) -> (observed_prevoted(N,R,V) <-> prevoted(N,R,V)) + invariant well_behaved(N) -> (observed_precommitted(N,R,V) <-> precommitted(N,R,V)) + +# nodes stop prevoting or precommitting in lower rounds when doing so in a higher round: + invariant well_behaved(N) & prevoted(N,R2,V2) & R1 < R2 -> left_round(N,R1) + invariant well_behaved(N) & locked(N,R2,V2) & R1 < R2 -> left_round(N,R1) + + invariant [precommit_unique_per_round] well_behaved(N) & precommitted(N,R,V1) & precommitted(N,R,V2) -> V1 = V2 + +} with nset, round, abstract_accountable_safety_2.defs.observed_equivocation_def, abstract_accountable_safety_2.defs.observed_unlawful_prevote_def + +# Proof that the property holds in the concrete specification +# =========================================================== + +isolate accountable_safety_2 = { + + instantiate tendermint(abstract_accountable_safety_2) + + invariant well_behaved(N) -> ~(abstract_accountable_safety_2.observed_equivocation(N) | abstract_accountable_safety_2.observed_unlawful_prevote(N)) + +} with round, value, shim, abstract_accountable_safety_2, abstract_accountable_safety_2.defs.observed_equivocation_def, abstract_accountable_safety_2.defs.observed_unlawful_prevote_def diff --git a/ivy-proofs/check_proofs.sh b/ivy-proofs/check_proofs.sh new file mode 100755 index 000000000..2663eb894 --- /dev/null +++ b/ivy-proofs/check_proofs.sh @@ -0,0 +1,38 @@ +#!/bin/bash + +# returns non-zero error code if any proof fails + +success=0 +log_dir=$(cat /dev/urandom | tr -cd 'a-f0-9' | head -c 6) +mkdir -p output/$log_dir + +echo "Checking classic safety:" +res=$(ivy_check classic_safety.ivy | tee "output/$log_dir/classic_safety.txt" | tail -n 1) +if [ "$res" = "OK" ]; then + echo "OK" +else + echo "FAILED" + success=1 +fi + +echo "Checking accountable safety 1:" +res=$(ivy_check complete=fo accountable_safety_1.ivy | tee "output/$log_dir/accountable_safety_1.txt" | tail -n 1) +if [ "$res" = "OK" ]; then + echo "OK" +else + echo "FAILED" + success=1 +fi + +echo "Checking accountable safety 2:" +res=$(ivy_check complete=fo accountable_safety_2.ivy | tee "output/$log_dir/accountable_safety_2.txt" | tail -n 1) +if [ "$res" = "OK" ]; then + echo "OK" +else + echo "FAILED" + success=1 +fi + +echo +echo "See ivy_check output in the output/ folder" +exit $success diff --git a/ivy-proofs/classic_safety.ivy b/ivy-proofs/classic_safety.ivy new file mode 100644 index 000000000..b422a2c17 --- /dev/null +++ b/ivy-proofs/classic_safety.ivy @@ -0,0 +1,85 @@ +#lang ivy1.7 +# --- +# layout: page +# title: Proof of Classic Safety +# --- + +include tendermint +include abstract_tendermint + +# Here we prove the classic safety property: assuming that every two quorums +# have a well-behaved node in common, no two well-behaved nodes ever disagree. + +# The proof is done in two steps: first we prove the the abstract specification +# satisfies the property, and then we show by refinement that this property +# also holds in the concrete specification. + +# To see what is checked in the refinement proof, use `ivy_show isolate=classic_safety classic_safety.ivy` +# To see what is checked in the abstract correctness proof, use `ivy_show isolate=abstract_classic_safety classic_safety.ivy` + +# To check the whole proof, use `ivy_check classic_safety.ivy`. + +# Note that all the verification conditions sent to Z3 for this proof are in +# EPR. + +# Classic safety in the abstract model +# ==================================== + +# We start by proving that classic safety holds in the abstract model. + +isolate abstract_classic_safety = { + + instantiate abstract_tendermint + + invariant [classic_safety] classic_bft.quorum_intersection & decided(N1,R1,V1) & decided(N2,R2,V2) -> V1 = V2 + +# The notion of choosable value +# ----------------------------- + + relation choosable(R:round, V:value) + definition choosable(R,V) = exists Q . nset.is_quorum(Q) & forall N . well_behaved(N) & nset.member(N,Q) -> ~left_round(N,R) | precommitted(N,R,V) + +# Main invariants +# --------------- + +# `classic_safety` is inductive relative to those invariants + + invariant [decision_is_quorum_precommit] (exists N1 . decided(N1,R,V)) -> exists Q. nset.is_quorum(Q) & forall N2. well_behaved(N2) & nset.member(N2, Q) -> precommitted(N2,R,V) + + invariant [precommitted_is_quorum_prevote] V ~= value.nil & (exists N1 . precommitted(N1,R,V)) -> exists Q. nset.is_quorum(Q) & forall N2. well_behaved(N2) & nset.member(N2, Q) -> prevoted(N2,R,V) + + invariant [prevote_unique_per_round] prevoted(N,R,V1) & prevoted(N,R,V2) -> V1 = V2 + +# This is the core invariant: as long as a precommitted value is still choosable, it remains protected by a lock and prevents any new value from being prevoted: + invariant [locks] classic_bft.quorum_intersection & V ~= value.nil & precommitted(N,R,V) & choosable(R,V) -> locked(N,R,V) & forall R2,V2 . R < R2 & prevoted(N,R2,V2) -> V2 = V | V2 = value.nil + +# Supporting invariants +# --------------------- + +# The main invariants are inductive relative to those + + invariant decided(N,R,V) -> V ~= value.nil + + invariant left_round(N,R2) & R1 < R2 -> left_round(N,R1) # if a node left round R2>R1, then it also left R1: + + invariant prevoted(N,R2,V2) & R1 < R2 -> left_round(N,R1) + invariant precommitted(N,R2,V2) & R1 < R2 -> left_round(N,R1) + +} with round, nset, classic_bft.quorum_intersection_def + +# The refinement proof +# ==================== + +# Now, thanks to the refinement relation that we establish in +# `concrete_tendermint.ivy`, we prove that classic safety transfers to the +# concrete specification: +isolate classic_safety = { + + # We instantiate the `tendermint` module providing `abstract_classic_safety` as abstract model. + instantiate tendermint(abstract_classic_safety) + + # We prove that if every two quorums have a well-behaved node in common, + # then well-behaved nodes never disagree: + invariant [classic_safety] classic_bft.quorum_intersection & server.decision(N1) ~= value.nil & server.decision(N2) ~= value.nil -> server.decision(N1) = server.decision(N2) + +} with value, round, proposers, shim, abstract_classic_safety # here we list all the specifications that we rely on for this proof diff --git a/ivy-proofs/docker-compose.yml b/ivy-proofs/docker-compose.yml new file mode 100644 index 000000000..1d4a8ffe1 --- /dev/null +++ b/ivy-proofs/docker-compose.yml @@ -0,0 +1,8 @@ +version: '3' +services: + tendermint-proof: + build: . + volumes: + - ./:/home/user/tendermint-proof:ro + - ./output:/home/user/tendermint-proof/output:rw + diff --git a/ivy-proofs/domain_model.ivy b/ivy-proofs/domain_model.ivy new file mode 100644 index 000000000..3de98da03 --- /dev/null +++ b/ivy-proofs/domain_model.ivy @@ -0,0 +1,90 @@ +#lang ivy1.7 +# --- +# layout: page +# title: Proof of Classic Safety +# --- + +include order # this is a file from the standard library (`ivy/ivy/include/1.7/order.ivy`) + +isolate round = { + type this + individual minus_one:this + relation succ(R1:round, R2:round) + action incr(i:this) returns (j:this) + specification { +# to simplify verification, we treat rounds as an abstract totally ordered set with a successor relation. + instantiate totally_ordered(this) + property minus_one < 0 + property succ(X,Z) -> (X < Z & ~(X < Y & Y < Z)) + after incr { + ensure succ(i,j) + } + } + implementation { +# here we prove that the abstraction is sound. + interpret this -> int # rounds are integers in the Tendermint specification. + definition minus_one = 0-1 + definition succ(R1,R2) = R2 = R1 + 1 + implement incr { + j := i+1; + } + } +} + +instance node : iterable # nodes are a set with an order, that can be iterated over (see order.ivy in the standard library) +relation well_behaved(N:node) # whether a node is well-behaved or not. NOTE: Use only in the proof! Nodes do know know that. + +isolate proposers = { + # each round has a unique proposer in Tendermint. In order to avoid a + # function from round to node (which makes verification more difficult), we + # abstract over this function using a relation. + relation is_proposer(N:node, R:round) + action get_proposer(r:round) returns (n:node) + specification { + property is_proposer(N1,R) & is_proposer(N2,R) -> N1 = N2 + after get_proposer { + ensure is_proposer(n,r); + } + } + implementation { + # here we prove that the abstraction is sound + function f(R:round):node + definition is_proposer(N,R) = N = f(R) + implement get_proposer { + n := f(r); + } + } +} + +isolate value = { # the type of values + type this + relation valid(V:value) + individual nil:value + specification { + property ~valid(nil) + } + implementation { + definition valid(V) = V ~= nil + } +} + +object nset = { # the type of node sets + type this # a set of N=3f+i nodes for 0 sent(M,D) + { + var n := iter.val; + call net.send(src,n,m); + iter := iter.next; + } + } + + implement send { + call net.send(src,dst,m) + } + + private { + invariant net.sent(M,D) -> sent(M,D) + } + } + +} with net, node # to prove that the shim implementation satisfies the shim specification, we rely on the specification of net and node. diff --git a/ivy-proofs/output/.gitignore b/ivy-proofs/output/.gitignore new file mode 100644 index 000000000..5e7d2734c --- /dev/null +++ b/ivy-proofs/output/.gitignore @@ -0,0 +1,4 @@ +# Ignore everything in this directory +* +# Except this file +!.gitignore diff --git a/ivy-proofs/tendermint.ivy b/ivy-proofs/tendermint.ivy new file mode 100644 index 000000000..950ce28b1 --- /dev/null +++ b/ivy-proofs/tendermint.ivy @@ -0,0 +1,430 @@ +#lang ivy1.7 +# --- +# layout: page +# title: Specification of Tendermint in Ivy +# --- + +# This specification closely follows the pseudo-code given in "The latest +# gossip on BFT consensus" by E. Buchman, J. Kwon, Z. Milosevic +# + +include domain_model +include network_shim + +# We model the Tendermint protocol as an Ivy object. Like in Object-Oriented +# Programming, the basic structuring unit in Ivy is the object. Objects have +# internal state and actions (i.e. methods in OO parlance) that modify their +# state. We model Tendermint as an object whose actions represent steps taken +# by individual nodes in the protocol. Actions in Ivy can have preconditions, +# and a valid execution is a sequence of actions whose preconditions are all +# satisfied in the state in which they are called. + +# For technical reasons, we define below a `tendermint` module instead of an +# object. Ivy modules are a little bit like classes in OO programs, and like +# classes they can be instantiated to obtain objects. To instantiate the +# `tendermint` module, we must provide an abstract-protocol object. This allows +# us to use different abstract-protocol objects for different parts of the +# proof, and to do so without too much notational burden (we could have used +# Ivy monitors, but then we would need to prefix every variable name by the +# name of the object containing it, which clutters things a bit compared to the +# approach we took). + +# The abstract-protocol object is called by the resulting tendermint object so +# as to run the abstract protocol alongside the concrete protocol. This allows +# us to transfer properties proved of the abstract protocol to the concrete +# protocol, as follows. First, we prove that running the abstract protocol in +# this way results in a valid execution of the abstract protocol. This is done +# by checking that all preconditions of the abstract actions are satisfied at +# their call sites. Second, we establish a relation between abstract state and +# concrete state (in the form of invariants of the resulting, two-object +# transition system) that allow us to transfer properties proved in the +# abstract protocol to the concrete protocol (for example, we prove that any +# decision made in the Tendermint protocol is also made in the abstract +# protocol; if the abstract protocol satisfies the agreement property, this +# allows us to conclude that the Tendermint protocol also does). + +# The abstract protocol object that we will use is always the same, and only +# the abstract properties that we prove about it change in the different +# instantiations of the `tendermint` module. Thus we provide common invariants +# that a) allow to prove that the abstract preconditions are met, and b) +# provide a refinement relation (see end of the module) relating the state of +# Tendermint to the state of the abstract protocol. + +# In the model, Byzantine nodes can send whatever messages they want, except +# that they cannot forge sender identities. This reflects the fact that, in +# practice, nodes use public key cryptography to sign their messages. + +# Finally, note that the observations that serve to adjudicate misbehavior are +# defined only in the abstract protocol (they happen in the abstract actions). + +module tendermint(abstract_protocol) = { + + # the initial value of a node: + parameter init_val(N:node): value + + # the three type of steps + object step_t = { + type this = {propose, prevote, precommit} + } # refer to those e.g. as step_t.propose + + object server(n:node) = { + + # the current round of a node + individual round_p: round + + individual step: step_t + + individual decision: value + + individual lockedValue: value + individual lockedRound: round + + individual validValue: value + individual validRound: round + + + relation done_l34(R:round) + relation done_l36(R:round, V:value) + relation done_l47(R:round) + + # variables for scheduling request + relation propose_timer_scheduled(R:round) + relation prevote_timer_scheduled(R:round) + relation precommit_timer_scheduled(R:round) + + relation _recved_proposal(Sender:node, R:round, V:value, VR:round) + relation _recved_prevote(Sender:node, R:round, V:value) + relation _recved_precommit(Sender:node, R:round, V:value) + + relation _has_started + + after init { + round_p := 0; + step := step_t.propose; + decision := value.nil; + + lockedValue := value.nil; + lockedRound := round.minus_one; + + validValue := value.nil; + validRound := round.minus_one; + + done_l34(R) := false; + done_l36(R, V) := false; + done_l47(R) := false; + + propose_timer_scheduled(R) := false; + prevote_timer_scheduled(R) := false; + precommit_timer_scheduled(R) := false; + + _recved_proposal(Sender, R, V, VR) := false; + _recved_prevote(Sender, R, V) := false; + _recved_precommit(Sender, R, V) := false; + + _has_started := false; + } + + action getValue returns (v:value) = { + v := init_val(n) + } + + export action start = { + assume ~_has_started; + _has_started := true; + # line 10 + call startRound(0); + } + + # line 11-21 + action startRound(r:round) = { + # line 12 + round_p := r; + + # line 13 + step := step_t.propose; + + var proposal : value; + + # line 14 + if (proposers.get_proposer(r) = n) { + if validValue ~= value.nil { # line 15 + proposal := validValue; # line 16 + } else { + proposal := getValue(); # line 18 + }; + call broadcast_proposal(r, proposal, validRound); # line 19 + } else { + propose_timer_scheduled(r) := true; # line 21 + }; + + call abstract_protocol.l_11(n, r); + } + + # This action, as not exported, can only be called at specific call sites. + action broadcast_proposal(r:round, v:value, vr:round) = { + var m: msg; + m.m_kind := msg_kind.proposal; + m.m_src := n; + m.m_round := r; + m.m_value := v; + m.m_vround := vr; + call shim.broadcast(n,m); + } + + + implement shim.proposal_handler.handle(msg:msg) { + _recved_proposal(msg.m_src, msg.m_round, msg.m_value, msg.m_vround) := true; + } + + + # line 22-27 + export action l_22(v:value) = { + assume _has_started; + assume _recved_proposal(proposers.get_proposer(round_p), round_p, v, round.minus_one); + assume step = step_t.propose; + + if (value.valid(v) & (lockedRound = round.minus_one | lockedValue = v)) { + call broadcast_prevote(round_p, v); # line 24 + call abstract_protocol.l_22(n, round_p, v); + } else { + call broadcast_prevote(round_p, value.nil); # line 26 + call abstract_protocol.l_22(n, round_p, value.nil); + }; + + # line 27 + step := step_t.prevote; + } + + + + # line 28-33 + export action l_28(r:round, v:value, vr:round, q:nset) = { + assume _has_started; + assume r = round_p; + assume _recved_proposal(proposers.get_proposer(r), r, v, vr); + assume nset.is_quorum(q); + assume nset.member(N,q) -> _recved_prevote(N,vr,v); + assume step = step_t.propose; + assume vr >= 0 & vr < r; + + # line 29 + if (value.valid(v) & (lockedRound <= vr | lockedValue = v)) { + call broadcast_prevote(r, v); + } else { + call broadcast_prevote(r, value.nil); + }; + + call abstract_protocol.l_28(n,r,v,vr,q); + step := step_t.prevote; + } + + action broadcast_prevote(r:round, v:value) = { + var m: msg; + m.m_kind := msg_kind.prevote; + m.m_src := n; + m.m_round := r; + m.m_value := v; + call shim.broadcast(n,m); + } + + implement shim.prevote_handler.handle(msg:msg) { + assume msg.m_vround = round.minus_one; + _recved_prevote(msg.m_src, msg.m_round, msg.m_value) := true; + } + + + # line 34-35 + export action l_34(r:round, q:nset) = { + assume _has_started; + assume round_p = r; + assume nset.is_quorum(q); + assume exists V . nset.member(N,q) -> _recved_prevote(N,r,V); + assume step = step_t.prevote; + assume ~done_l34(r); + done_l34(r) := true; + + prevote_timer_scheduled(r) := true; + } + + + # line 36-43 + export action l_36(r:round, v:value, q:nset) = { + assume _has_started; + assume r = round_p; + assume exists VR . _recved_proposal(proposers.get_proposer(r), r, v, VR); + assume nset.is_quorum(q); + assume nset.member(N,q) -> _recved_prevote(N,r,v); + assume value.valid(v); + assume step = step_t.prevote | step = step_t.precommit; + + assume ~done_l36(r,v); + done_l36(r, v) := true; + + if step = step_t.prevote { + lockedValue := v; # line 38 + lockedRound := r; # line 39 + call broadcast_precommit(r, v); # line 40 + step := step_t.precommit; # line 41 + call abstract_protocol.l_36(n, r, v, q); + }; + + validValue := v; # line 42 + validRound := r; # line 43 + + } + + + # line 44-46 + export action l_44(r:round, q:nset) = { + assume _has_started; + assume r = round_p; + assume nset.is_quorum(q); + assume nset.member(N,q) -> _recved_prevote(N,r,value.nil); + assume step = step_t.prevote; + + call broadcast_precommit(r, value.nil); # line 45 + step := step_t.precommit; # line 46 + + call abstract_protocol.l_44(n, r, q); + } + + action broadcast_precommit(r:round, v:value) = { + var m: msg; + m.m_kind := msg_kind.precommit; + m.m_src := n; + m.m_round := r; + m.m_value := v; + m.m_vround := round.minus_one; + call shim.broadcast(n,m); + } + + implement shim.precommit_handler.handle(msg:msg) { + assume msg.m_vround = round.minus_one; + _recved_precommit(msg.m_src, msg.m_round, msg.m_value) := true; + } + + + # line 47-48 + export action l_47(r:round, q:nset) = { + assume _has_started; + assume round_p = r; + assume nset.is_quorum(q); + assume nset.member(N,q) -> exists V . _recved_precommit(N,r,V); + assume ~done_l47(r); + done_l47(r) := true; + + precommit_timer_scheduled(r) := true; + } + + + # line 49-54 + export action l_49_decide(r:round, v:value, q:nset) = { + assume _has_started; + assume exists VR . _recved_proposal(proposers.get_proposer(r), r, v, VR); + assume nset.is_quorum(q); + assume nset.member(N,q) -> _recved_precommit(N,r,v); + assume decision = value.nil; + + if value.valid(v) { + decision := v; + # MORE for next height + call abstract_protocol.decide(n, r, v, q); + } + } + + # line 55-56 + export action l_55(r:round, b:nset) = { + assume _has_started; + assume nset.is_blocking(b); + assume nset.member(N,b) -> exists V,VR . _recved_proposal(N,r,V,VR) | _recved_prevote(N,r,V) | _recved_precommit(N,r,V); + assume r > round_p; + call startRound(r); # line 56 + } + + # line 57-60 + export action onTimeoutPropose(r:round) = { + assume _has_started; + assume propose_timer_scheduled(r); + assume r = round_p; + assume step = step_t.propose; + call broadcast_prevote(r,value.nil); + step := step_t.prevote; + + call abstract_protocol.l_57(n,r); + + propose_timer_scheduled(r) := false; + } + + # line 61-64 + export action onTimeoutPrevote(r:round) = { + assume _has_started; + assume prevote_timer_scheduled(r); + assume r = round_p; + assume step = step_t.prevote; + call broadcast_precommit(r,value.nil); + step := step_t.precommit; + + call abstract_protocol.l_61(n,r); + + prevote_timer_scheduled(r) := false; + } + + + # line 65-67 + export action onTimeoutPrecommit(r:round) = { + assume _has_started; + assume precommit_timer_scheduled(r); + assume r = round_p; + call startRound(round.incr(r)); + + precommit_timer_scheduled(r) := false; + } + +# The Byzantine actions +# --------------------- + +# Byzantine nodes can send whatever they want, but they cannot send +# messages on behalf of well-behaved nodes. In practice this is implemented +# using cryprography (e.g. public-key cryptography). + + export action byzantine_send = { + assume ~well_behaved(n); + var m:msg; + var dst:node; + assume ~well_behaved(m.m_src); # cannot forge the identity of well-behaved nodes + call shim.send(n,dst,m); + } + +# Byzantine nodes can also report fake observations, as defined in the abstract protocol. + export action fake_observations = { + call abstract_protocol.misbehave + } + +# Invariants +# ---------- + +# We provide common invariants that a) allow to prove that the abstract +# preconditions are met, and b) provide a refinement relation. + + + invariant 0 <= round_p + invariant abstract_protocol.left_round(n,R) <-> R < round_p + + invariant lockedRound ~= round.minus_one -> forall R,V . abstract_protocol.locked(n,R,V) <-> R <= lockedRound & lockedValue = V + invariant lockedRound = round.minus_one -> forall R,V . ~abstract_protocol.locked(n,R,V) + + invariant forall M:msg . well_behaved(M.m_src) & M.m_kind = msg_kind.prevote & shim.sent(M,N) -> abstract_protocol.prevoted(M.m_src,M.m_round,M.m_value) + invariant well_behaved(N) & _recved_prevote(N,R,V) -> abstract_protocol.prevoted(N,R,V) + invariant forall M:msg . well_behaved(M.m_src) & M.m_kind = msg_kind.precommit & shim.sent(M,N) -> abstract_protocol.precommitted(M.m_src,M.m_round,M.m_value) + invariant well_behaved(N) & _recved_precommit(N,R,V) -> abstract_protocol.precommitted(N,R,V) + + invariant (step = step_t.prevote | step = step_t.propose) -> ~abstract_protocol.precommitted(n,round_p,V) + invariant step = step_t.propose -> ~abstract_protocol.prevoted(n,round_p,V) + invariant step = step_t.prevote -> exists V . abstract_protocol.prevoted(n,round_p,V) + + invariant round_p < R -> ~(abstract_protocol.prevoted(n,R,V) | abstract_protocol.precommitted(n,R,V)) + invariant ~_has_started -> step = step_t.propose & ~(abstract_protocol.prevoted(n,R,V) | abstract_protocol.precommitted(n,R,V)) & round_p = 0 + + invariant decision ~= value.nil -> exists R . abstract_protocol.decided(n,R,decision) + } +}