Systems Software Verification Summer School Overview
"Join the Systems Software Verification Summer School to learn about formal verification in distributed protocols. Explore fundamental concepts, tools, and techniques to prove system correctness while gaining practical hands-on experience. No prior verification experience required; just a keen interest in distributed systems. Get ready to enhance your skills and knowledge!"
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Systems Software Verification Summer School Manos Kapritsos, University of Michigan Jon Howell, VMWare Research Rob Johnson, VMWare Research
PURPOSE OF THIS SUMMER SCHOOL For you For you: to learn the concepts and practical skills required to prove the correctness of distributed protocols For us For us: to make sure others learn from our mistakes
OUR GOALS FOR THIS WEEK We don t plan don t plan to make you verification experts (unless you already are) Goals Goals Understand the fundamentals fundamentals of formal verification Learn to use it Learn to use it in a distributed systems context Get hands hands- -on experience on experience with proving systems correct Become familiar with a practical verification language language
SYLLABUS Things we hope you ll learn this week: Things we hope you ll learn this week: Specify Specify behavior with TLA+ state machines Verify Verify protocols with Dafny automation How to debug debug a proof a proof Structure a proof with refinement refinement Manage proof automation automation challenges
PREREQUISITES Awareness of distributed distributed or asynchronous asynchronous systems No No verification experience required verification experience required If anything is unclear, do not hesitate to ask Disclaimer Disclaimer: this summer school is not formally verified
LECTURES AND LAB SESSIONS Duration: July 13 to July 17 Lectures and Lab Sessions through Zoom One 3-hour lecture period, 9am-12pm PDT 15-minute break halfway Two Lab Sessions: Western Hemisphere: 1-5pm PDT Eastern Hemisphere: 1-5pm CEST
LECTURES ETIQUETTE Please keep yourself muted want to ask a question You are encouraged encouraged to have your camera on muted during lectures, unless you Please ask questions if you don t understand something Please ask questions if you don t understand something Unmute yourself and ask your question
LAB SESSIONS You will be writing proofs in Dafny during the Lab Sessions, as well as today s lecture If you have questions during a Lab Session, write your name on the Google doc link we sent you over email to enter the Office Hours queue. Maintain FIFO when writing to the queue! An instructor will let you know which Zoom call to join, as soon as they are available
USING DAFNY We will be using Dafny as our verification language Dafny is an imperative verification in mind imperative language designed with formal Most of the high-level skills are transferrable... ...but some are specific to Dafny and/or automation In your docker container, type dafny dafny test.dfy test.dfy
Formal Verification of Distributed Systems
[Mickens 2013] not one of the properties claimed invariant in [PODC] is actually invariantly true of it. [Zave 2015]
SYSTEMS AND FORMAL VERIFICATION # verification papers 5 4 3 2 1 0 09 10 11 12 13 14 15 16 17 18 19 SOSP/OSDI
FORMAL VERIFICATION Step 1: Specify Step 1: Specify the correctness of the system formally Step 2: Prove Step 2: Prove that the implementation conforms to the spec If the spec expresses your correctness property, then your system is correct, correct, subject to the assumptions assumptions you have made during your proof
OTHER APPROACHES Testing Testing: run the system with a large and/or representative set of inputs to determine if it behaves correctly Quality depends on acumen of test designer Infeasible to achieve complete coverage for complex systems Model Model checking checking: : Model the system and ensure all possible states are safe Correctness depends on how accurate the model is Does not scale well to complex systems, especially those with infinite state spaces, like distributed systems
STATICALLY CHECKING FOR CORRECTNESS What we want is a static correctness check , akin to a static type check You write your code normally, but if you introduce bugs the checker will tell you When the checker complains, you have to spend some time to convince it that your code is right---if indeed it is
USING A THEOREM PROVER Express the execution of the system and its correctness as a mathematical formula mathematical formula Give the formula to a theorem prover, effectively asking: If the system behaves this way, is it possible for its correctness to be violated? A negative negative answer means the system is proven to be correct A positive positive answer means there is still work to do, either: the system is indeed incorrect the proof is incomplete proven to be correct
SYSTEMS SCOPE You will learn how to use theorem proving to prove the correctness of systems Centralized systems Centralized systems Distributed systems Distributed systems
SPECIFYING SYSTEMS Specification is the most crucial step One of the few trusted trusted steps were bugs can be introduced Multiple ways to specify a system s correctness The program never crashes Property (safety or liveness) Refinement
STATE MACHINES You will learn how to model the behavior of a system as a state machine Allows us to compose multiple machines into a distributed system Allows us to prove properties (invariants) over an entire execution of the system You will get hands-on experience modeling systems as state machines
INDUCTIVE INVARIANTS Invariants are typically proven using induction. But their original form is not amenable to an inductive proof. You will learn the difference between invariants inductive invariants inductive invariants invariants and You will get hands on experience identifying inductive invariants in increasingly complex systems
MODELING DISTRIBUTED SYSTEMS You will learn how to compose multiple state machines into a distributed system You will learn how to model the environment, such as the network and clocks At this point, you ll be ready for your midterm project Lab Session after Day 3 Lecture
REFINEMENT You will learn how to structure a proof using refinement You will learn how to prove that a system refines a high- level specification And more: application correspondence and multi-level refinement
Complexities of implementation Subtleties of distributed protocols Using efficient data structures Maintaining global invariants Dealing with hosts acting concurrently Memory management Avoiding integer overflow Ensuring progress
ADVANCED TOPICS Verification Engineering Principles Environment assumptions How to reason about cross-host concurrency Automation control techniques
FOCUS OF THIS SUMMER SCHOOL Concepts, not Dafny Spec Our main focus Protocols, not implementations Protocol Implementation
