Skip to content

Commit 63cb0c9

Browse files
HristoStaykovteoparvanov
HristoStaykov
and
teoparvanov
authored
Formal model for SBFT - initial version (#2350)
* Initial version of SBFT formal model. In this version of the model we have the Slow Commit path, for which we have proven that honest replicas agree in their Commit messages to the assignment of Client Operations to Sequence ID-s. We have the mechanism of the View Change process in the system modeled according to the definition in BFT (excluding the Fast Commit Path) because it is not yet modeled and we are missing the specifics related to Checkpointing, since they are yet to be modeled as well. * Aligning PR with open concord-bft source policies * Fixing the GitHub repo link Co-authored-by: teoparvanov <tparvanov@vmware.com>
1 parent 9614bbf commit 63cb0c9

11 files changed

+1936
-0
lines changed

‎.gitignore

+5
Original file line numberDiff line numberDiff line change
@@ -24,3 +24,8 @@ MakefileCustom
2424
# Apollo test output
2525
*/apollo/Testing/*
2626
Testing
27+
28+
# Dafny profiling logs
29+
/.dafny
30+
dafny-qi.profile
31+
triggers

‎docs/sbft-formal-model/README.md

+77
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
# Project overview
2+
The aim of this sub-project is to both document and to formally specify the concord-bft state machine replication (SMR) protocol.
3+
4+
Given the distributed nature of the concord-bft protocol, unit tests offer limited means of establishing the desired state machine replication (SMR) safety properties. The main tool we use for proving correctness is an integration testing framework code-named [Apollo](https://github.com/vmware/concord-bft/tree/master/tests/apollo) which creates mini-blockchain deployments and exercises various runtime scenarios (including straight case, replica failures, network faults, as well as certain byzantine cases).
5+
6+
Apollo does give us good confidence as to the correctness and fault tolerance of the concord-bft SMR. But even if we bring test coverage to 100%, we can never be sure that we have discovered all possible bugs and failure scenarios.
7+
8+
We use Dafny and first-order logic to model and prove the safety properties of the protocol's core state machine (liveness properties are out of scope for now).
9+
10+
# Dev instructions
11+
12+
The Dafny model can be used as a document, for proving SBFT correctness properties, or as input for property-based tests of the implementation's core components.
13+
14+
## Install Docker itself if you don't have it already.
15+
16+
* [Mac installer](https://docs.docker.com/v17.12/docker-for-mac/install/)
17+
18+
* [Windows installer](https://docs.docker.com/v17.12/docker-for-windows/install/)
19+
20+
* On linux:
21+
22+
```bash
23+
sudo apt install docker.io
24+
sudo service docker restart
25+
sudo addgroup $USER docker
26+
newgrp docker
27+
```
28+
29+
## Pull the image.
30+
(This is the slow thing; it includes a couple GB of Ubuntu.)
31+
32+
```bash
33+
docker pull jonhdotnet/summer_school:1.1
34+
```
35+
36+
## Run the image
37+
38+
Run the image connected to your filesystem so you can edit in your OS, and then run Dafny from inside the docker container:
39+
40+
```bash
41+
mkdir work
42+
cd work
43+
docker container run -t -i --mount src="`pwd`",target=/home/dafnyserver/work,type=bind --workdir /home/dafnyserver/work jonhdotnet/summer_school:1.1 /bin/bash
44+
git clone https://github.com/vmware/concord-bft
45+
cd concord-bft/docs/sbft-formal-model
46+
```
47+
48+
Now you can edit files using your preferred native OS editor under the work/
49+
directory, and verify them with Dafny from the terminal that's running the
50+
docker image.
51+
52+
The docker-based command-line Dafny installation above is offered as a
53+
portable, simple way to get started. There do exist snazzy real-time Dafny
54+
integrations for IDEs (Visual Studio, VSCode) and editors (Emacs, Vim). You
55+
are certainly welcome to install Dafny natively and integrate it with your
56+
editor if you prefer.
57+
58+
## Test that the image works
59+
60+
From the container started as described in the previous step run:
61+
62+
```bash
63+
dafny /vcsCores:$(nproc) proof.dfy
64+
```
65+
66+
If everything is working, you should see something like:
67+
68+
```bash
69+
Dafny program verifier finished with 10 verified, 0 errors
70+
```
71+
72+
# Acknowledgements and references
73+
74+
This project builds on top of the concepts and framework described in
75+
https://github.com/GLaDOS-Michigan/summer-school-2021<br>
76+
77+
Special thanks to [@jonhnet|https://github.com/jonhnet] for his help and support along the way.

‎docs/sbft-formal-model/application.s.dfy

+68
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
// Concord
2+
//
3+
// Copyright (c) 2022 VMware, Inc. All Rights Reserved.
4+
//
5+
// This product is licensed to you under the Apache 2.0 license (the "License"). You may not use this product except in
6+
// compliance with the Apache 2.0 License.
7+
//
8+
// This product may include a number of subcomponents with separate copyright notices and license terms. Your use of
9+
// these subcomponents is subject to the terms and conditions of the sub-component's license, as noted in the LICENSE
10+
// file.
11+
12+
include "network.s.dfy"
13+
14+
module Application {
15+
import opened Library
16+
type State(!new, ==)
17+
type ClientRequest(!new, ==)
18+
type ClientReply(!new, ==)
19+
20+
function InitialState() : State
21+
function Transition(state:State, clientRequest:ClientRequest) : (result:(State, ClientReply))
22+
// This is an assumption given to us by the user.
23+
24+
datatype Variables = Variables(
25+
state:State,
26+
unprocessedRequests:set<ClientRequest>,
27+
undeliveredReplies:set<ClientReply>
28+
)
29+
30+
predicate Init(v:Variables)
31+
{
32+
&& v.s == InitialState()
33+
}
34+
35+
predicate AcceptRequest(v:Variables, v':Variables, clientRequest:ClientRequest)
36+
{
37+
&& v' == v.(unprocessedRequests := v.unprocessedRequests + {clientRequest})
38+
}
39+
40+
predicate ProcessRequest(v:Variables, v':Variables, clientRequest:ClientRequest)
41+
{
42+
&& clientRequest in v.unprocessedRequests
43+
&& var newState, clientReply := Transition(v.state, clientRequest);
44+
&& v' == v.(state := newState)
45+
.(undeliveredReplies := v.undeliveredReplies + {clientReply})
46+
.(unprocessedRequests := v.unprocessedRequests - {clientRequest})
47+
}
48+
49+
predicate DeliverReply(v:Variables, v':Variables, clientReply:ClientReply)
50+
{
51+
&& clientReply in v.undeliveredReplies
52+
&& v' == v.(undeliveredReplies := v.undeliveredReplies - {clientReply})
53+
}
54+
55+
// Jay Normal Form - Dafny syntactic sugar, useful for selecting the next step
56+
datatype Step =
57+
// Recvs:
58+
| AcceptRequestStep()
59+
60+
predicate NextStep(c:Constants, v:Variables, v':Variables, msgOps:Network.MessageOps<Message>, step: Step) {
61+
match step
62+
case RecvPrePrepareStep => RecvPrePrepare(c, v, v', msgOps)
63+
}
64+
65+
predicate Next(c:Constants, v:Variables, v':Variables, msgOps:Network.MessageOps<Message>) {
66+
exists step :: NextStep(c, v, v', msgOps, step)
67+
}
68+
}

‎docs/sbft-formal-model/client.i.dfy

+90
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
// Concord
2+
//
3+
// Copyright (c) 2022 VMware, Inc. All Rights Reserved.
4+
//
5+
// This product is licensed to you under the Apache 2.0 license (the "License"). You may not use this product except in
6+
// compliance with the Apache 2.0 License.
7+
//
8+
// This product may include a number of subcomponents with separate copyright notices and license terms. Your use of
9+
// these subcomponents is subject to the terms and conditions of the sub-component's license, as noted in the LICENSE
10+
// file.
11+
12+
include "network.s.dfy"
13+
include "cluster_config.s.dfy"
14+
include "messages.dfy"
15+
16+
module Client {
17+
import opened Library
18+
import opened HostIdentifiers
19+
import opened Messages
20+
import Network
21+
import ClusterConfig
22+
23+
// Define your Client protocol state machine here.
24+
datatype Constants = Constants(myId:HostId, clusterConfig:ClusterConfig.Constants) {
25+
// host constants coupled to DistributedSystem Constants:
26+
// DistributedSystem tells us our id so we can recognize inbound messages.
27+
predicate WF() {
28+
&& clusterConfig.WF()
29+
&& clusterConfig.N() <= myId < NumHosts()
30+
}
31+
32+
predicate Configure(id:HostId, clusterConf:ClusterConfig.Constants) {
33+
&& myId == id
34+
&& clusterConfig == clusterConf
35+
}
36+
}
37+
38+
// Placeholder for possible client state
39+
datatype Variables = Variables(
40+
lastRequestTimestamp:nat,
41+
lastReplyTimestamp:nat
42+
) {
43+
44+
predicate WF(c:Constants)
45+
{
46+
&& c.WF()
47+
&& lastRequestTimestamp >= lastReplyTimestamp
48+
}
49+
}
50+
51+
function PendingRequests(c:Constants, v:Variables) : nat
52+
requires v.WF(c)
53+
{
54+
v.lastRequestTimestamp - v.lastReplyTimestamp
55+
}
56+
57+
// Predicate that describes what is needed and how we mutate the state v into v' when SendPrePrepare
58+
// Action is taken. We use the "binding" variable msgOps through which we send/recv messages.
59+
predicate SendClientOperation(c:Constants, v:Variables, v':Variables, msgOps:Network.MessageOps<Message>)
60+
{
61+
&& v.WF(c)
62+
&& msgOps.IsSend()
63+
&& PendingRequests(c,v) == 0
64+
&& var msg := msgOps.send.value;
65+
&& msg.payload.ClientRequest?
66+
&& msg.sender == c.myId
67+
&& msg.payload.clientOp.sender == c.myId
68+
&& msg.payload.clientOp.timestamp == v.lastRequestTimestamp + 1
69+
&& v' == v.(lastRequestTimestamp := v.lastRequestTimestamp + 1)
70+
}
71+
72+
predicate Init(c:Constants, v:Variables) {
73+
&& v.WF(c)
74+
&& v.lastRequestTimestamp == 0
75+
&& v.lastReplyTimestamp == 0
76+
}
77+
78+
// Jay Normal Form - syntactic sugar, useful for selecting the next step
79+
datatype Step =
80+
| SendClientOperationStep()
81+
82+
predicate NextStep(c:Constants, v:Variables, v':Variables, msgOps:Network.MessageOps<Message>, step: Step) {
83+
match step
84+
case SendClientOperationStep() => SendClientOperation(c, v, v', msgOps)
85+
}
86+
87+
predicate Next(c:Constants, v:Variables, v':Variables, msgOps:Network.MessageOps<Message>) {
88+
exists step :: NextStep(c, v, v', msgOps, step)
89+
}
90+
}

‎docs/sbft-formal-model/cluster_config.s.dfy

+72
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
// Concord
2+
//
3+
// Copyright (c) 2022 VMware, Inc. All Rights Reserved.
4+
//
5+
// This product is licensed to you under the Apache 2.0 license (the "License"). You may not use this product except in
6+
// compliance with the Apache 2.0 License.
7+
//
8+
// This product may include a number of subcomponents with separate copyright notices and license terms. Your use of
9+
// these subcomponents is subject to the terms and conditions of the sub-component's license, as noted in the LICENSE
10+
// file.
11+
12+
include "network.s.dfy"
13+
14+
module ClusterConfig {
15+
import opened HostIdentifiers
16+
17+
datatype Constants = Constants(
18+
maxByzantineFaultyReplicas:nat,
19+
numClients:nat
20+
) {
21+
22+
predicate WF()
23+
{
24+
&& maxByzantineFaultyReplicas > 0 // Require non-trivial BFT system
25+
&& numClients > 0
26+
}
27+
28+
function ClusterSize() : nat
29+
requires WF()
30+
{
31+
N() + numClients
32+
}
33+
34+
function F() : nat
35+
requires WF()
36+
{
37+
maxByzantineFaultyReplicas
38+
}
39+
40+
function ByzantineSafeQuorum() : nat
41+
requires WF()
42+
{
43+
F() + 1
44+
}
45+
46+
function N() : nat // BFT Replica Size
47+
requires WF()
48+
{
49+
3 * F() + 1
50+
}
51+
52+
function AgreementQuorum() : nat
53+
requires WF()
54+
{
55+
2 * F() + 1
56+
}
57+
58+
predicate IsReplica(id:HostId)
59+
requires WF()
60+
{
61+
&& ValidHostId(id)
62+
&& 0 <= id < N()
63+
}
64+
65+
predicate IsClient(id:HostId)
66+
requires WF()
67+
{
68+
&& ValidHostId(id)
69+
&& N() <= id < NumHosts()
70+
}
71+
}
72+
}

0 commit comments

Comments
 (0)