CS 591 - Spring 2021 - Formal Methods in Security and Privacy


Lecture time and location: Tu-Th 3:30-4:45pm - CAS 221
EasyCrypt Lab (on Zoom): We 6:30pm-7:45pm
Instructors: Marco Gaboardi and Alley Stoughton
e-mail: gaboardi@bu.edu and stough@bu.edu

Office Hours: on Zoom by appointment
Discussion forums: Piazza
Reading material: We will base the class on a working draft of a book by Gilles Barthe (MPI and IMDEA) that is available at the following link:
http://software.imdea.org/~gbarthe/__introrelver.pdf
Note: The draft above is a work in progress. Please, feel free to contact Gilles with any feedback, typos, etc.

Overview

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.

Course prerequisites

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.

Course requirements

The course has two main requirements:

Grading

The final grade will be composed as:

Projects

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 (3-4 times during the term) to check on the advancements and directions of the project.

Class material

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.

Lecture Schedule

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

EasyCrypt Lab Schedule

Date Topic Notes
Week 1 Installing EasyCrypt and EasyCrypt's Ambient Logic
EasyCrypt installation instructions
check-install.ec
EasyCrypt Reference Manual
Slides on EasyCrypt's Ambient Logic
logic-examp-fill.ec logic-examp.ec
Week 2 EasyCrypt's Ambient Logic
Slides on EasyCrypt's Ambient Logic
logic-examp-fill.ec logic-examp.ec
logic-examp2-fill.ec logic-examp2.ec
int-div-examp-fill.ec int-div-examp.ec
Week 3 EasyCrypt's While Language and Hoare Logic
Slides on EasyCrypt's While Language and Hoare Logic
fast-expon-fill.ec fast-expon.ec
Week 4 EasyCrypt's Hoare Logic
Slides on EasyCrypt's While Language and Hoare Logic
Slides on EasyCrypt's Ambient Logic
find-primes-fill.ec find-primes.ec
Week 5 Noninterference and EasyCrypt's Relational Hoare Logic
Slides on EasyCrypt's Relational Hoare Logic and Noninterference
noninter-fill.ec noninter.ec
Week 6 Noninterference and EasyCrypt's Relational Hoare Logic
Slides on EasyCrypt's Relational Hoare Logic and Noninterference
xor-loop-fill.ec xor-loop.ec
Week 7 Probabilistic Noninterference and EasyCrypt's Probabilistic Relational Hoare Logic
Slides on EasyCrypt's Probabilistic Relational Hoare Logic and Probabilistic Noninterference
prob-noninter-fill.ec prob-noninter.ec
Week 8 EasyCrypt's Probabilistic Hoare and Probabilistic Relational Hoare Logics
phl-prhl-fill.ec phl-prhl.ec
Week 9 Secure Message Communication (SMC) in a Real/Ideal Paradigm Style
SMC-fill.ec SMC.ec
Week 10 approximate probabilistic Relational Hoare Logic
dp.ec
Week 11 More on approximate probabilistic Relational Hoare Logic
rnm.ec

Assignments

Assignment Topic Files
Assignment 1 EasyCrypt's Ambient Logic Assignment1.ec
Assignment1-answers.ec
Assignment 2 EasyCrypt's Ambient Logic Assignment2.ec
Assignment2-answers.ec
Assignment 3 Hoare Logic and Relational Hoare Logic Assignment3.pdf
Assignment3-answers.pdf
Assignment 4 Noninterference and EasyCrypt's Relational Hoare Logic Assignment4.ec
Assignment4-answers.ec
Assignment 5 Probabilistic Noninterference and EasyCrypt's Probabilistic Relational Hoare Logic Assignment5.ec
Assignment5-answers.ec
Assignment 6 Differential Privacy Assignment6.ec
Assignment6-answers.ec

Last Year's Assignments

Assignment Topic Files
Assignment 0 EasyCrypt's Ambient Logic ass0.ec
Assignment 1 EasyCrypt's Hoare Logic 1-assigns-fill.ec 2-sort3-fill.ec 3-expon-fill.ec
1-assigns.ec 2-sort3.ec 3-expon.ec
Assignment 2 Noninterference and EasyCrypt's Relational Hoare Logic simpl-fill.ec mod3-fill.ec xor-loop-fill.ec
simpl.ec mod3.ec xor-loop.ec
Assignment 3 Probabilistic Noninterference and EasyCrypt's pRHL prob-noninter-fill.ec
prob-noninter.ec