Formal Verification and Performance Simulation in Real-World Applications - A Case Study with the Stellar Blockchain

Explore formal verification and performance simulation techniques applied to real-world blockchain systems through a case study of the Stellar network. Delve into the practical approach of network simulation, focusing on transaction subsystems and distributed network behavior. Examine the theoretical approach of formal verification, learning how to create models, list properties to prove, and test implementations. Gain insights into solving complex problems iteratively, starting with simplified solutions and building towards comprehensive understanding. This conference talk, presented by Nicolas Barry and Hidenori Shinohara from the Stellar Development Foundation, offers valuable lessons for developers and researchers working on distributed systems and blockchain technologies.

Intro
Intro: What is Stellar?
Maintains a local copy of a cryptographic ledger Processes transactions against it, in consensus with a set of peers. Implements the Stellar Consensus Protocol, a federated consensus protocol. Written in C++14
Practical approach: Network Simulation
We split the problem into two main parts: 1. Transaction subsystem • Requires a complicated database setup • Improved with standard performance & stress testing 2. Simulation that focuses on the distributed
Create a network based on the public network topology Have them talk to each other Monitor metrics of each node (e.g., CPU/memory usage, consensus latency)
Node count, transaction volume, etc Analysis on the degree distribution, diameter,... Network behavior in different situations - Anomalies at the node level - Traffic pattern changes, etc
Theoretical approach: Formal Verification
Verify a new change to the protocol - Security: Does the network function as a proper
Step 1: Create a model - Implement the protocol in Ivy Step 2: List properties to prove - Examples
Test the actual C++ implementation • Alternative ballot-protocol model • More work on liveness properties
Ask What's the simplest solution that represents a significant step towards the full solution? • Learn from each iteration, and apply it to the next iteration
Questions?