Security and privacy breaches are constantly on the news. Often these breaches are due to vulnerabilities in the design and implementations of software components. In this class we will study some of the formal tools that have been developed to formally support the correctness of software with respect to security and privacy requirements. We will focus on a few security and privacy properties such as: information flow control and non-interference, provable security, and differential privacy.
The course consists of a series of lectures on different formalisms that have been developed to reason about security and privacy properties. The basic formalism we will use is the one provided by relational program logics. We will first study a deterministic logic which is useful for reasoning about information flows and non-interference. Then, we will study a probabilistic extension of this logic which supports reasoning about cryptographic security and differential privacy. We will see how different natural proofs from cryptography and differential privacy can be expressed using this formalism. We will also experiment practically with these topics on different examples by using the EasyCrypt tool, which you can find here.
The course has a significant component based on analysis of algorithms, and formal techniques. So, the following are required classes: CAS CS 237 or equivalent; CAS CS 320 or equivalent; CAS CS 330 or equivalent; or consent of instructor. Additionally, some rudimentary understanding of probability and statistics is expected.
The course has two main requirements:
The grading will be based on assignments, participation in class, and project.
The final grade will be composed as:
Projects can take different forms depending on the interest of each student but all the projects must have a research component. Some examples of what would constitute a good project are:
| Date | Topic | Notes |
|---|---|---|
| Tu 1/21 | No Class |
|
| Tr 1/23 | Introduction to the topic + basic logic recap |
Slides Notes: Section 1.1.1 |
| Tu 1/28 | Introduction to EasyCrypt + Basics of the while language (syntax and semantics) + Basic Hoare Logic |
Slides EasyCrypt Manual: Chapter 1 Installing EasyCrypt Emacs Text Editor EasyCrypt example: logic-examp-fill.ec logic-examp.ec |
| Tr 1/30 | Basic Hoare Logic and properties |
Slides |
| Tu 2/4 | Hoare Logic - part 1 |
Slides |
| Tr 2/6 | Hoare Logic - part 2 |
Slides |
| Tu 2/11 | Hoare Logic and Information flow |
Slides |
| Tr 2/13 | Noninterference and Relational Hoare Logic |
Slides |
| Tu 2/18 | No Class - President's Day substitute Monday |
|
| Tr 2/20 | Noninterference and Relational Hoare Logic |
Slides |
| Tu 2/25 | Probabilistic While Language |
Slides |
| Tr 2/27 | Probabilistic Relational Reasoning |
Slides |
| Tu 3/3 | Formal Proofs for Cryptography |
Slides |
| Tr 3/5 | Formal Proofs for Cryptography |
Slides |
| Tu 3/10 | No Class - spring break |
|
| Tr 3/12 | No Class - spring break |
|
| Tu 3/17 | Probabilistic Relational Hoare Logic |
Slides |
| Tr 3/19 | Probabilistic Relational Hoare Logic |
Slides |
| Tu 3/24 | Approximate Probabilistic Hoare Logic |
Slides |
| Tr 3/26 | Approximate Probabilistic Hoare Logic |
Slides |
| Tu 3/31 | Approximate Probabilistic Hoare Logic |
Slides |
| Tr 4/02 | Differential privacy |
Slides |
| Tu 4/07 | Differential Privacy |
Slides |
| Tr 4/09 | Examples of differentially private proofs |
Slides |
| Tu 4/14 | Formal Proofs for Cryptography (Cont.) |
Slides |
| Tr 4/16 | Formal Proofs for Cryptography (Cont.) |
Slides |
| Tu 4/21 | Formal Proofs for Cryptography (Cont.) |
Slides |
| Tr 4/23 | Examples of differentially private proofs using Coupling |
Slides |
| Tu 04/28 | Students' presentations |
|
| Tr 04/30 | Students' presentations |
|
| Date | Topic | Notes |
|---|---|---|
| Week 1 | EasyCrypt's Ambient Logic |
Slides |
| Week 2 | EasyCrypt's Hoare Logic |
Slides |
| Week 3 | EasyCrypt's Hoare Logic |
Questions and answers relating to Assignment 1 |
| Week 4 | Noninterference and EasyCrypt's Relational Hoare Logic |
EasyCrypt Manual: Section 3.4 |
| Week 5 | Noninterference and EasyCrypt's Relational Hoare Logic |
Questions and answers relating to Assignment 2 |
| Week 6 | EasyCrypt's pRHL (probabilistic Relational Hoare
Logic) |
EasyCrypt Manual: Section 3.4 |
| Week 7 | Working with Procedure Calls and Adversaries |
EasyCrypt Manual: Sections 2.4 and 3.4 |
| Week 8 | Pseudorandom Generators (PRGs) |
EasyCrypt Manual: Sections 2.4 and 3.4 |
| Week 9 | More probabilistic Hoare Logic (pHL) |
EasyCrypt Manual: Section 3.4 |
| Week 10 | Differential Privacy |
|
| Week 11 | Differentially Private Sums |
|
| Assignment | Topic | Files |
|---|---|---|
| Assignment 0 | EasyCrypt's Ambient Logic |
|
| Assignment 1 | EasyCrypt's Hoare Logic |
|
| Assignment 2 | Noninterference and EasyCrypt's Relational Hoare Logic |
|
| Assignment 3 | Probabilistic Noninterference and EasyCrypt's pRHL |
|