pbft

PBFT (Practical Byzantine Fault Tolerance)

Models the PBFT 3-phase protocol: pre-prepare, prepare, commit. This spec combines the concepts from bft-voting, bft-proposal, and bft-locking into the actual protocol structure.

Protocol Overview

         Leader                    Replicas (N2, N3, N4)
           |                              |
           |-- PRE-PREPARE(req) --------> |  Phase 1: Leader proposes
           |                              |
           | <---- PREPARE(req) --------- |  Phase 2: Replicas echo
           | <---- PREPARE(req) --------- |
           | <---- PREPARE(req) --------- |
           |                              |
           |      [2f prepares seen]      |  Node becomes "prepared"
           |                              |
           | <---- COMMIT(req) ---------- |  Phase 3: Replicas commit
           | <---- COMMIT(req) ---------- |
           | <---- COMMIT(req) ---------- |
           |                              |
           |      [2f+1 commits seen]     |  Request is committed

Running

make test SPEC=pbft
make run SPEC=pbft
make verify SPEC=pbft

State Variables

Variable	Type	Description
status	Node -> Status	Which nodes are faulty
leader	Node	Leader for this view
prePrepare	Node -> Request	Pre-prepare received by each node
prepares	Node -> Request	Prepare sent by each node
commits	Node -> Request	Commit sent by each node
phase	Node -> Phase	Each node's protocol phase
committed	Set[Request]	Requests that have been committed

Phases

Idle

Node has not yet received a pre-prepare.

PrePrepared

Node received pre-prepare and sent prepare.

Prepared

Node saw 2f matching prepares and sent commit. This is the "lock" point - the node is committed to this request.

Committed

Node saw 2f+1 commits. Request is executed.

Actions

Correct Node Actions

correctLeaderPrePrepare(request) - Leader broadcasts pre-prepare.

correctSendPrepare(node) - Node receives pre-prepare, sends prepare.

correctSendCommit(node) - Node sees 2f prepares, becomes prepared, sends commit.

correctCommit(node) - Node sees 2f+1 commits, commits request.

Faulty Node Actions

faultyLeaderPrePrepare(node, request) - Faulty leader sends (possibly different) pre-prepare to one node.

faultySendPrepare(node, request) - Faulty node sends prepare for any request.

faultySendCommit(node, request) - Faulty node sends commit for any request.

Safety Properties

agreement

At most one request commits.

committed.size() <= 1

integrity

Committed request was pre-prepared by someone.

Why PBFT is Safe

The prepare phase creates a lock:

• To become prepared, a node needs 2f matching prepares
• Two sets of 2f prepares overlap by at least f nodes
• At least one of those is correct
• Correct nodes only prepare what they pre-prepared

The commit phase enforces agreement:

• To commit, a node needs 2f+1 commits
• Two sets of 2f+1 commits overlap by at least f+1 nodes
• At least one of those is correct and was prepared
• That correct node only prepared one request

Tests

happyPathTest

Correct leader, all phases complete, request commits.

faultyLeaderEquivocationTest

Faulty leader sends different pre-prepares to different nodes. Only one request can reach prepare quorum and commit.

faultyNodeHelpsNeitherTest

Faulty node sends prepare for wrong request. Doesn't prevent correct request from committing.

phaseOrderingTest

Verifies phase transitions enforce protocol ordering.

Simplifications

This spec omits:

• View changes - Leader replacement on timeout
• Checkpointing - Garbage collection of old messages
• Multiple slots - Concurrent consensus instances
• Request execution - Actual state machine application

These can be added as extensions.

Prerequisites

This spec builds on:

• bft-voting/ - Quorum intersection (why 2f+1 works)
• bft-proposal/ - Leader coordination (pre-prepare phase)
• bft-locking/ - Locking across rounds (prepared state)

References

• PBFT Paper - Castro, Liskov (1999)
• The Byzantine Generals Problem - Lamport, Shostak, Pease (1982)