Formal Verification of Systems Software

The lectures and tutorials for this course will be recorded, but we recommend attending in person,
as the lectures and tutorials are designed to be interactive.

You will submit graded exercises and projects online, no attendance is needed to submit these.

---

 

➡️ Lecture Recordings, Slides, and other material

➡️ Setting up Verus, documentation, and how to submit take-home exercises

 

---

Systems Software underpins our modern computing infrastructure, both in datacenters, and on personal devices. When it fails or misbehaves because of bugs, they can lose or leak your data, make online services unavailable for a long period of time, and -- if you are a developer -- cost your company its reputation and revenue. For example, a corruption in a filesystem, or storage system may make you lose your e-mail, messages, photos, or banking information.

Regular testing can be insufficient for complex (often distributed) systems, which is why you keep hearing about software failures in online services. In this course, you will learn how to formally verify the correctness of these programs, so that we can have near certainty that the software we deploy is bug-free. You will learn how to model the expected behavior of a system, -- for example, how a distributed storage system (like Amazon's S3) is nothing else than a very simple map from keys to values from the perspective of its clients. You will then learn how to write Rust code for and such a system and formally prove, at compile time, that this implementation matches the simple key-value abstract model, i.e. that the program code is correct, without however having to run it or any tests.

We'll use the Rust-based Verus verification framework. Verus is being developed primarily at MPI-SWS, CMU, Microsoft, and is used for cutting edge research at MPI-SWS, MIT, CMU, UIUC (and more), and in industry: for example, Microsoft is developing a storage system verified with Verus, and Amazon is evaluating Verus to verify some of their systems. On the Verus website you can find a list of research papers and projects using Verus.

You will learn the necessary Rust and Verus syntax, and the formal verification principles we will use to write a systems' specification, and to prove the correctness of the implementation. Verus is a modern semi-automated tool that leverages SMT (satisfiability modulo theories) solvers to automatically handle many of the trivial and not-so-trivial steps of the proofs: you will learn how to write the rest of the proof as assertions written in Rust. At the end you will be able to design, implement, and prove correct a small but complex system, such as a distributed, sharded hash table. 

Prerequisites. Programming experience, preferably in a Systems language (like C/C++). Knowing Rust is not a prerequisite. A background in formal methods and/or logic is helpful, but not required.

---

 

Course Structure (Weekly)

• 1.5-hour lecture: Fridays 10:15-11:45 in E1 5 029
  More info on how to find the rooms.
• 1 hour tutorial and exercise discussion: Wednesdays 16:10-17:00 in E1 5 029 (starting October 30th)
• take home exercises (graded)

Evaluation

• need to pass 7 out of 8 of take home exercise chapters to register for the exam
  • students get feedback on submissions, and can resubmit take home exercises
  • note that "Chapter 00: Submitting" is not part of the graded take home exercises and was simply a test of the ability of Student to submit through CMS
• 2 graded projects, done individually (25% + 25%)
  • need to pass (50% score) both project to register for the exam
• exam (50%) (with a re-exam)
  • you will need to pass 7 out of 8 of the take home exercises, and score at least 50% in both projects to register for the exam (and re-exam)

Exam Dates

• End of Term: February 26, 9:30-12:00 in E1 3 hall 002.
• Re-Exam: March 18th, 9:30-12:00 in E1 3 hall 002.

(The actual duration may be a bit shorter than the full 2.5 hours slots.)

Projects

• (mid-term) design and verify a distributed lock service
• (final, in parallel to lectures on advanced topics) design and verify a sharded key-value store

Course Development

The concept and part of this course (with exercises in Dafny, instead of Verus) have initially been developed by Manos Kapritsos, University of Michigan, Jon Howell, VMware Research, with later contributions by Tej Chajed, University of Wisconsin-Madison, and Andrea Lattuada (the instructor), MPI-SWS.

Schedule (tentative)

- 2024-10-18: Intro
- 2024-10-25: Verus Mechanics (datatypes, predicates, assertions)

- 2024-11-15: Specification and state machines
- 2024-11-22: State machines and behaviors
- 2024-11-29: Proving properties and inductive invariants
- 2024-12-06: Leader election demo
- 2024-12-13: Modeling distributed and asynchronous systems
- 2024-12-20: Recap + Project 1 assignment

- 2025-01-10: Asynchronous specifications + Application correspondence
- 2025-01-17: Multi-layer refinement
- 2025-01-24: Cross-host concurrency + Project 2 assignment
- 2025-01-31: Case studies + Research 
- 2025-02-07: Recap

Take-home exercises and project rules

• Exercises and projects are individual
  • Okay to clarify problem or discuss Verus syntax
  • on Discourse, in person
• It is not okay to discuss solutions
• Do not publish your exercise solutions anywhere

• You may not use /* */ comments
• You must leave the existing /* */ comments in place
• You may only change text between /*{*/ and /*}*/
• You are not allowed to add axioms (I have not taught you how to do this)
• You are not allowed to use assume(_); or admit(); in the code you submit
• Do not rename the files

 

Verus logo CC-BY Verus Contributors, Rust logo CC-BY Rust Foundation