Formal Reasoning for Security and Privacy - Class at USI

Instructor: Marco Gaboardi
e-mail: gaboardi@bu.edu
Reading material: We will loosely 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.

Lecture Schedule

Date	Topic	Notes
Mon 9/9	Introduction, while language and Hoare Logic	Slides
Tue 9/10	Noninterference and Relational Hoare Logic	Slides
Wed 9/11	Probabilistic Noninterference and Probabilistic Relational Hoare Logic	Slides
Wed 9/12	Differential Privacy and Approximate Probabilistic Relational Hoare Logic	Slides

EasyCrypt Lab Schedule

Date	Topic	Notes
Mon 9/9	Installing EasyCrypt and EasyCrypt's Ambient Logic	EasyCrypt installation instructions check-install.ec EasyCrypt Reference Manual Slides on EasyCrypt's Ambient Logic logic-examp.ec logic-examp2.ec hoare-example1.ec
Tue 9/10	HL, RHL and Noninterference	HL-example.ec Slides on EasyCrypt's Hoare Logic fast-expon.ec noninter.ec Slides on EasyCrypt's Relational Hoare Logic
Wed 9/11	pRHL and Probabilistic Noninterference	Slides on EasyCrypt's Probabilistic Relational Hoare Logic prob-noninter.ec xor-loop.ec
Thu 9/12	Probabilistic Noninterference, apRHL and Differential Privacy	xor-loop.ec dp.ec