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 noninterference, 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 noninterference. 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 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:
The instructors will provide some specific ideas for possible projects but other ideas may be accepted if well motivated and discussed with the instructors. Students may work on their projects alone or they may collaborate with others. Groups can be composed by at most two students. Each group is invited to meet with the instructors regularly (34 times during the term) to check on the advancements and directions of the project.
The class will be based on lecture slides that will be posted on this website. Every student will also be invited to engage on a project and to present the results at the end of the course. Discussion about all the aspects of the course will also take place on Piazza.
Date  Topic  Notes 

Tu 1/25  Introduction to the topic + basic logic recap 
Slides Notes: Section 1.1.1 
Tr 1/27  Semantics of Imp 
Slides 
Tu 2/2  Semantics of Imp 
Slides 
Tr 2/4  Hoare Logic  part 1 
Slides 
Tu 2/9  Hoare Logic  part 2 
Slides 
Tr 2/11  Hoare Logic, WP, Noninterference 
Slides 
Tu 2/16  No Class  President's Day substitute Monday 

Tr 2/18  Noninterference and Relational Hoare Logic 
Slides 
Tu 2/23  Noninterference and Relational Hoare Logic 
Slides 
Tr 2/25  Probabilistic Relational Reasoning 
Slides 
Tu 3/2  Probabilistic Noninterference 
Slides 
Tr 3/4  Probabilistic Relational Hoare Logic 
Slides 
Tr 3/9  Probabilistic Relational Hoare Logic and Formal
Proofs for Cryptography 
Slides on pRHL Slides on Crypto 
Tr 3/11  Formal Proofs for Cryptography 
Slides 
Tu 3/16  Differential Privacy 
Slides 
Tr 3/18  No Class  Wellness Day 

Tu 3/23  Approximate Probabilistic Hoare Logic 
Slides 
Tr 3/25  More differential privacy 
Slides 
Tu 3/30  Formal Proofs for Cryptography 
Slides 
Tr 4/01  Formal Proof for Cryptography 
Slides 
Tu 4/06  More Differential Privacy 
Slides 
Tr 4/08  Examples of differentially private proofs 
Slides 
Tu 4/13  More Examples of differentially private proofs 
Slides 
Tr 4/15  More Examples of differentially private proofs 
Slides 
Tu 4/20  Proofs of Protocol Security in Real/Ideal Paradigm 
Slides 
Tr 4/22  Proofs of Protocol Security in Real/Ideal Paradigm 
Slides 
Tu 04/27  Students' presentations 

Tr 04/29  Students' presentations 

Assignment  Topic  Files 

Assignment 1  EasyCrypt's Ambient Logic 

Assignment 2  EasyCrypt's Ambient Logic 

Assignment 3  Hoare Logic and Relational Hoare Logic 

Assignment 4  Noninterference and EasyCrypt's Relational Hoare Logic 

Assignment 5  Probabilistic Noninterference and EasyCrypt's Probabilistic Relational Hoare Logic 

Assignment 6  Differential Privacy 

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 
