**Verification for Security (XM_0099)** *[Klaus v. Gleissenthall*](https://gleissen.github.io) About ============================================================== This course focuses on formal verification with an eye on security. We will cover the basics of formal verification through lectures. We'll start from zero, but move fast. The purpose of this part of the course is to give you the necessary background to understand and implement program verification tools. In fact, we'll build both an SMT solver and a fully functioning program verifier, similar to Amazon's [Dafny](http://dafny.org/), from the ground up. You'll then implement an information-flow type system that shows that a piece of code doesn't leak its secrets to an attacker. The purpose of the course is to give you a deep understanding of program verification and prepare you for research and practice in the area. Lectures: - Tuesday, 11:00--12:45 in HG-12A33 and Wednesday 15:30--17:15 in HG-12A33. - Check [rooster](https://rooster.vu.nl/schedule) for more detailed scheduling info. Staff: - **Lectures**: Klaus v. Gleissenthall - **Practicals**: Robin Webbers, Alp Adnan Basar Practical Session: - Friday 11:00 - 12:45 in HG-11A33. Flipped Classroom ============================================================== This class will be using the flipped classroom model. That means, we will make videos of the lecture material available online. Please watch the videos before the corresponding lecture slot. We will use the actual classroom time for questions and discussion. You can find the lecture videos on [Canvas](https://canvas.vu.nl/courses/78421/files/folder/videos). We highly recommend attending the lecture slots and using them for questions about the material. In our experience, students who actively participate do better in assignments and the exam. Grading ============================================================== The grade will consist of assignment grades (50%) and final exam grade (50%). The exam must be passed with a grade >= 5.5. Each of the practical assignments must be passed with a grade >= 4.0. There will be a resit exam on January 7, 2025, but there is no resit for the practical assignments. Component | Percentage ------------------------------|------------------- Assignments | 50% Final Exam | 50% We offer an optional project for the ambitious. You can skip the last assignment, and earn a bonus of up to 3 grade points for the exam. If you're interested in doing a project, please let us know at the lecture or practical slot. See [this page](projects.html) for a list of project ideas. Other than a programming project, you may also prove a theorem about one of the topics discussed in the course. Syllabus and Calendar ============================================================== Tue Sep 3 2024: Intro & Propositional Logic - In this lecture we'll go over course admin. - We'll also start with the material. - To reason about programs, we need to know logic, the language of computation. - We'll start with the simplest one: propositional logic. - [Slides](slides/lecture1.pdf) - *Videos*: - 0 and 1a,1b - *Reading*: - For this first part of the course, we'll closely follow the following book, which you can access with your VU account. - [The Calculus of Computation](https://link.springer.com/book/10.1007/978-3-540-74113-8) - This and next lecture will cover chapter 1. Wed Sep 4 2024: Normal Forms & DPLL - To use propositional logic for reasoning about programs, we need to be able to solve questions about formulas alorithmically. - In this lecture, we cover the DPLL algorithm that can check whether a propositional formula is satisfiable. - [Slides](slides/lecture2.pdf) - *Videos*: - 2a-2c - *Reading* - [Fast Decision Procedures](https://web.eecs.umich.edu/~weimerw/2021-590/reading/dpllt.pdf) Sun Sep 8 2024: Deadline: Assignment 0 due (2 pts) - Intro to Haskell & Monads due - Take a look at this [tutorial](https://docs.google.com/document/d/1On06ZVBocHEOzlIQFq1MrQzwOjeKE-MyDE7eNPkyiDo/edit?usp=sharing) we wrote about monads. Tue Sep 10 2024: First-order Logic - We now know how to solve questions about propositional logic, but the logic is too limited to encode many interesting questions about programs. - In this lecture, we'll look at a *way* more expressive logic: first order logic (FOL). - In fact, we'll see that FOL is *too* expressive! - It's no longer possible to answer questions algorithmically in an efficient way, as most interesting problems are undecidable. - [Slides](slides/lecture3.pdf) - *Videos*: - 3a;3b - *Reading*: - Chapter 2 of [The Calculus of Computation](https://link.springer.com/book/10.1007/978-3-540-74113-8). Wed Sep 11 2024: First-order Theories - Propositional logic was not expressive enough, FOL was too expressive. - In this lecture, we'll talk about the Goldilocks of logics: first-order theories. - First-order theories allow us to encode many interesting questions about programs while still maintaining decidability. - We'll learn about satisfiability modulo theories (or SMT) which underlies most modern tools for verification, symbolic execution and bug finding. - [Slides](slides/lecture4.pdf) - *Videos*: - 4 - *Reading* - Chapter 3 of [The Calculus of Computation](https://link.springer.com/book/10.1007/978-3-540-74113-8). - [Handbook of Satisfiability](https://people.eecs.berkeley.edu/~sseshia/pubdir/SMT-BookChapter.pdf) Sun Sep 15 2024: Deadline: Assignment 1a (2 pt) Tue Sep 17 2024: Nano & Hoare Logic - Now that we've learned about the right logic to reason about programs, we can start to look at actual programs! - We'll start by defining an imperative language, called Nano, and giving it formal semantics. - As is often the case in PL research, Nano is a minimal, stripped down version of a programming language. - This will help us focus on the conceptually important problems. - Next, we need to think about when these programs are correct. For this, we'll take a look at Hoare logic. - [Slides](slides/lecture5.pdf) - - *Videos*: - 5a, 5b - *Reading* - Chapter 2 of [The formal semantics of programming languages : an introduction](https://vu.on.worldcat.org/oclc/26764522) - [A Structural Approach to Operational Semantics](papers/SOS.pdf) - [Proof of a program Find](https://web.eecs.umich.edu/~weimerw/2021-590/reading/HoareFind.pdf) Wed Sep 18 2024: Hoare Logic & VCGen - Hoare logic is great, as it lets us talk about the correctness of programs. - But so far, we have to do proofs manually by constructing a derivation in Hoare logic. - Instead, we'll now partially automate proofs by creating a set of verification conditions--SMT formulas whose validity lets us deduce whether the program is correct. - This is called verification condition generation (VCGen). - We can then send these formulas to an SMT solver who will solve them automatically. - Now, all we have to do to verify a program is write down its loop invariants, and we can check their correctness automatically. - [Slides](slides/lecture6.pdf) - *Videos*: - 6a, 6b - *Reading* - Chapter 6 of [The formal semantics of programming languages : an introduction](https://vu.on.worldcat.org/oclc/26764522) Tue Sep 24 2024: VCs for Functions and Pointer - While Nano defines the core of an imperative language, it's still missing some crucial features. - In this lecture, we'll add two important missing ones: functions and pointers. - We'll then show how to extend VCGen to account for them. - [Slides](slides/lecture7.pdf) - *Videos*: - 7 Wed Sep 25 2024: Horn Clauses - With VCGen, the only thing a user needs to supply to verify a program are the loop invariants. - Now, we want to try to automate this step as well. - As a first step, we'll show how to encode the search for loop invariants in logic--as Horn clauses. - [Slides](slides/lecture8.pdf) - *Videos*: - 8a, 8b Friday Sep 27 2024: Deadline: 1b DPLL & SMT (6 pt) Tue Oct 1 2024: Solving Horn Clauses - Now we know how to encode the search for invariants as Horn clauses. - But we also need to solve Horn clauses--that is, find the invariants automatically. - The method we'll look at will be based on `predicates`-- sets of building blocks that our invariants will be made out of. - [Slides](slides/lecture9.pdf) - *Videos*: - 9 - *Reading* - [Abstract Interpretation](https://web.eecs.umich.edu/~weimerw/2021-590/reading/AbramskiAI.pdf) - [Cousot & Cousot](https://web.eecs.umich.edu/~weimerw/2021-590/reading/CousotCousot.pdf) - [Horn clauses](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-yurifest.pdf) - [Lazy Abstraction](https://courses.cs.washington.edu/courses/cse501/15sp/papers/henzinger.pdf) Wed Oct 2 2024: Information Flow Control - We'll now shift towards security problems. - We'll quickly see how we can use our verification tools to help with security. - Then, we'll look at a completely different approach for ensuring security: type systems. - They are an example of a quite different philosophy for program correctness. - While in the earlier part of the course, we tried to prove correctness for any program that we might be given, with this approach we're more picky. - We'll reject programs that are not obviously correct, and let the programmer come up with a better solution. - [Slides](slides/lecture10.pdf) - *Videos*: - 10 - *Reading* - This [survey](https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf) Tue Oct 8 2024: IFC & Side-Channels - In the last content lecture of the course, we'll see how to use type-systems to show that programs are free of certain types of side-channels. - We'll start with timing and cache, and then move on to more advanced side-channels caused by speculative execution. - [Slides](slides/lecture11.pdf) - *Videos*: - 11 - *Reading* - This [paper](https://gleissen.github.io/papers/spectre-semantics.pdf) on defining leakage in the presence of Spectre-BCB. - This [paper](https://gleissen.github.io/papers/BLADE.pdf) on defending against Spectre-BCB. - This [paper](https://gleissen.github.io/papers/ccs2023.pdf) on provably bounding leakage of hardware. - This [survey](https://cseweb.ucsd.edu/~dstefan/pubs/cauligi:2022:sok.pdf) - This [paper](https://www.scs.stanford.edu/~nickolai/papers/zeldovich-histar.pdf) on IFC for an operating system. Wed Oct 9 2024: Liquid Types - In this lecture, we'll see how to extend our verification approach for procedures, to a functional language (where functions can themselves be arguments). - [Slides](slides/lecture12.pdf) - *Videos*: - 12 - *Reading* - Chapter 3 of [this monograph](https://arxiv.org/pdf/2010.07763). - This [paper](https://gleissen.github.io/papers/refinement-refutations.pdf) on debugging typing failures. - You can also start with this [blog post](https://vusecpl.github.io/2024-06-29-type-refutations/). - [This tutorial](https://liquid.kosmikus.org/01-intro.html) for liquid Haskell. Tue Oct 15 2024: Deadline: Assignment 2: VCGen (10 pt) Wed Oct 16 2024: Review and Mock Exam - We'll use this slot for exam preparation. Tue Oct 22 2024: Exam Fr Oct 25 2024: Extra Practical IFC Assignment (HG-15A33) Sun Oct 31 2024: Deadline: Assignment 3 Assignments ============================================================== ## Overview Assignments | Points | Due Date ---------------------|----------|------------------- 0: Haskell & Monads | 2 pt | 08 Sep 2024 1a: Formal Proofs | 2 pt | 15 Sep 2024 1b: DPLL & SMT | 6 pt | 27 Sep 2024 2 : VCGen | 10 pt | 15 Oct 2024 3 : IFC Types | 5 pt | 31 Oct 2024 - We highly recommend attending the practicals. In our experience, students who regularly attend the practical sessions do much better in the assignments. - If you have problems, or don't know where to start, please come to the practicals, we're here to help! - The assignments will be taken in groups of 2. You can sign up for a group on [Canvas](https://canvas.vu.nl/courses/78421/groups#tab-39784). - All assignments will be written in [Haskell](https://www.haskell.org/). - *You will need a good background in functional programming* for the assignments. - We will offer material to catch up, in case you're missing it, but you will have to work extra hard to keep up. - If you need a refresher, take a look at this [tutorial](http://learnyouahaskell.com/chapters). - Monads have proven to be one of the toughest topics to understand. We wrote this [tutorial](https://docs.google.com/document/d/1On06ZVBocHEOzlIQFq1MrQzwOjeKE-MyDE7eNPkyiDo/edit?usp=sharing) to help. ## Details - Assignment 0: Haskell and Monads - The purpose of this assignment is to get you up to speed on Haskell. - You'll implement a bunch of simple functions in Haskell and get acquainted with the concept of monads. - Don't forget to take a look at the [monad tutorial](https://docs.google.com/document/d/1On06ZVBocHEOzlIQFq1MrQzwOjeKE-MyDE7eNPkyiDo/edit?usp=sharing). - Assignment 1: DPLL and SMT - In this assignment, you'll implement a SAT solver yourself! - You'll even turn it into a simple SMT solver for linear arithmetic. - Once you're done, please fill out [this anonymous feedback form](https://docs.google.com/forms/d/1IQzEiNOiue__Ca5qLbcAMewfOYfr7DLH5hc0UY0fCVU/edit) to give us feedback on the assignment. - Assignment 2: Hoare Logic and VCGen - In this assignment, you'll implement your own verifier similar to [Dafny](http://dafny.org/), and use it to verify a suite of programs. - Assignment 3: IFC Types - In this assignment, you will implement the information flow control type system discussed in lecture. Resources ============================================================== - How to [read a paper](https://our.utah.edu/wp-content/uploads/sites/35/2022/05/HowtoReadPaper.pdf). - Book for the logic part of the course: [The Calculus of Computation](https://link.springer.com/book/10.1007/978-3-540-74113-8) - Book for semantics: [The formal semantics of programming languages : an introduction](https://vu.on.worldcat.org/oclc/26764522). - Horn clauses: [paper](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-yurifest.pdf). - IFC type systems [survey](https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf). - See [this page](projects.html) for a list of project ideas. - How to debug Haskell type errors.