csc2125-project

Formal verification on (P)BFT consensus protocols

Overview

This project aims for building a TLA+ ¹ specification for the PBFT protocol ² and validate its core safety and liveness properties.

Project structure

Report.

Source codes:

| pbft
| | | pbft.tla          main specification
| | | model.tla         helper to run the model
| | | model.cfg         tlc config file to run the model
| | | messages.tla      message specification
| | | network.tla       network specification
| | | primary.tla       primary specific transitions
| | | secondary.tla     secondary specific transitions
| | | tsc.tla           helper for counting number of steps
| | | util.tla          utilites
| | | view.tla          view change specification
| | data                state statistics (generated by pytest)
| | | *.cfg             generated config file
| | | *.out             state counts
| | run.py              driver to run the specification
| | tests
| | | test_basic.py     safety and reachability tests
| | | test_project.py   linter tools

Environment:

| .envrc
| prefix
| | lib
| | | tla2tools.jar
| venv

Setup

Download tla2tools.jar from here to prefix/lib/.

Setup a virtual environment using python3 -m venv venv from the project root.

The file .envrc is a bash script that shows how the environmental variables are being setup.

cd pbft
pip install -r requirements.txt
pytest

Run

The following tests runs the specification.

<Dir pbft>
  <Dir tests>
    <Module test_basic.py>
      <Function test_path_reachable[Path_stage2_ViewChange-stage2]>
      <Function test_path_reachable[Path_stage2_NewView-stage2]>
      <Function test_path_reachable[Path_stage2_View1-stage2]>
      <Function test_path_reachable[Path_base_Prepared-base]>
      <Function test_path_reachable[Path_base_Committed-base]>
      <Function test_path_reachable[Path_base_AllCommitted-base]>
      <Function test_path_reachable[Path_stage2_AllCommittedTwice-stage2]>
      <Function test_profile[base-override0-False]>
      <Function test_profile[view1-override1-False]>
      <Function test_profile[stage2-override2-False]>
      <Function test_profile[stage3-override3-True]>
      <Function test_liveness[base-override0-False]>
      <Function test_liveness[view1-override1-False]>
      <Function test_liveness[stage2-override2-False]>
      <Function test_liveness[stage3-override3-True]>

test_profile runs the full specification (without liveness) with different profiles. The base profile is located in pbft/model.cfg, and overrides can be found in pbft/tests/test_basic.py::PROFILES.

test_liveness is the same as test_profile, except that it also checks liveness. It needs to be run with --run-slow.

test_path_reachable checks if a certain state is reachable. The states are specified as an invariant in pbft/model.tla. To check if state state is reachable with profile profile, add Path_{profile}_{name} = ~{state} and run

pytest "pbft/tests/test_basic.py::test_path_reachable[Path_{profile}_{name}-{profile}]"

Pytest can be ran with flag -s to show the outputs from TLC.

Limitations

• The model assumes only one request can be pending. i.e., the primary will not send another PRE-PREPARE until the current request is executed by the primary.

Footnotes

1. TLA+ IDE ↩

2. PBFT paper ↩