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


Location: MCS B29
Time: Tu-Th 11:00-12:15
Instructors: Marco Gaboardi and Alley Stoughton
EasyCrypt Lab Option (a): Monday 11:15am-12:05pm MCS 122
EasyCrypt Lab Option (b): Monday 12:20-1:10pm MCS 122
EasyCrypt Lab Option (c): Tuesday 6:30-7:20pm MCS B30 (opposite restrooms)
e-mail: gaboardi@bu.edu and stough@bu.edu

Office Hours: Marco Gaboardi (MCS 116) Tues 2-4pm or by appointment; Alley Stoughton (MCS 122) 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 grading will be based on assignments, participation in class, and project.
The final grade will be composed as:

  • 40% Assignments,
  • 10% Participation,
  • 50% Project.

  • 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:

  • using EasyCrypt or one of its extension to prove secure and privacy of a new complex algorithm,
  • design or implementation of a new programming language, system, or tool for security and privacy,
  • development and implementation of heuristics and optimizations to speed up the verification tasks for security and privacy,
  • investigation of new applications of relational logics.

  • 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 notes that will be distributed during class. 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/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 and Differential Privacy
    Tr 4/02 Examples of differentially private proofs
    Tu 4/07 More advanced examples of formal cryptography proofs
    Tr 4/09 More advanced examples of formal cryptography proofs
    Tu 4/14 More differential privacy
    Tr 4/16 Examples of differentially private proofs using Coupling
    Tu 4/21 Examples of differentially private proofs using Coupling
    Tr 4/23 Students' presentation
    Tu 04/28 Students' presentation
    Tr 04/30 Students' presentation

    EasyCrypt Lab Schedule

    Date Topic Notes
    Week 1 EasyCrypt's Ambient Logic
    Slides
    logic-examp2-fill.ec logic-examp2.ec
    Week 2 EasyCrypt's Hoare Logic
    Slides
    fast-expon-fill.ec fast-expon.ec
    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
    noninter-fill.ec noninter.ec
    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
    rnd-fill.ec rnd.ec
    Week 7 Working with Procedure Calls and Adversaries
    EasyCrypt Manual: Sections 2.4 and 3.4
    procs-and-adversaries-fill.ec procs-and-adversaries.ec
    Week 8 Pseudorandom Generators (PRGs)
    EasyCrypt Manual: Sections 2.4 and 3.4
    prg-fill.ec prg.ec

    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