Formal Verification of Systems Software

Andrea Lattuada, Derek Dreyer

News

Chapter 3, exercise 2 feedback published

Written on 20.12.24 by Andrea Lattuada

Dear all, just a quick note that I have updated the chapter 3 feedback with individual feedback for exercise 2. Individual feedback for chapter 3, exercise 3 will be published in the next couple of days. Please send me an email if you have any questions.

Chapter 4 Patch

Written on 18.12.24 by Andrea Lattuada

Dear Students, there is a small issue in exercise01.rs in the handout I distributed for Chapter 4 (and Chapter 5). For an accurate model of the system, we need to state that the network's sent_msgs Set is finite as a well_formed condition. This will not have prevented you from proving safety and is a… Read more

Dear Students, there is a small issue in exercise01.rs in the handout I distributed for Chapter 4 (and Chapter 5). For an accurate model of the system, we need to state that the network's sent_msgs Set is finite as a well_formed condition. This will not have prevented you from proving safety and is a weaker network property (so it's not incorrect, just models a network where the messages could be infinite); but the update is still a valid, and more accurate, network model and makes the proof for Chapter 5 simpler.

If you have already submitted, I have applied the patch to your code and re-submitted for you: you can download the updated code from your personal status page. If you have not submitted you have two options:

(a) recommended, especially if you've only done a little bit of work: re-download the handout and copy over your solution within the grading markers,

(b) use the write up at https://cms.sic.saarland/sysverification2425/5/Chapter_4_Patch to apply the change to exercise01.rs (note that you will need to do this carefully, to make sure that your code will pass the auto-grader check for changes outside the grading markers)

Sorry for the inconvenience.

I will also soon update the incremental.rs example from the last lecture demos to match the same network model.

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: Refinement Introduction + Project 1 assignment

- 2025-01-10: Application correspondence / Reduction
- 2025-01-17: Asynchronous Specs + Multi-layer refinement + Project 2 assignment
- 2025-01-24: Cross-host concurrency
- 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

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.