Instructor

Cristina Nita-Rotaru
Email: c.nitarotaru@northeastern.edu.

Course Description

Network protocols and distributed systems are at the core of all computing systems we rely on today. Thus, it is important that we have assurance about their design and implementation, i.e. their designs and implementations are free of bugs and vulnerabilities. For secure protocols, their goals must also be achieved in the presence of adversaries that must be clearly specified. Formal methods can help disambiguate system specifications and can expose flaws in system requirements, often not captured through testing. In this class we will study how formal methods have been applied to gain assurance about network protocols and distributed systems design and implementation. We will focus both on the benefits and limitations of formal methods based approaches.

The objectives of the course are the following:

• Provide an overview of the main methods of getting assurance about protocol implementations, including secure network protocols and showing how formal methods fit in this context.
• Provide an overview of current state of the art formal methods capabilities when applied to network protocols and distributed systems. This will include an overview of existing available tools, highlighting their strengths and weaknesses.
• Read recent, state-of-the-art research papers from both systems and security conferences focused on applications of formal methods to network protocols and distributed systems and discuss them in class. Students will actively participate in class discussions, and lead discussions on multiple papers during the semester.
• Experiment with applying formal methods to network protocols and distributed systems through several programming exercises and a semester-long research project. Students can select the topic of the research project.

Grade

The grade will be based on paper review submission (PR), participation in paper discussions in class (PD), presentations of papers in class and discussion lead (PL), one programming assignment (PA) and research project (RP). Paper reviews are due by 9pm the day before the lecture when the paper is discussed.Submission is through Gradescope. Grade is computed as follows:

Academic Integrity

Academic Honesty and Ethical behavior are required in this course, as it is in all courses at Northeastern University. There is zero tolerance to cheating.

You are encouraged to talk with the professor about any questions you have about what is permitted on any particular assignment.

Resources

• How to read research papers: [PDF]
• How to write a review [PDF]
• How to prepare presentations [HTML]
• Computing ecosystem literacy [HTML]
• Docker tutorial [HTML]
• Tamarin prover tutorial [HTML]

Tools

• ACL2 [HTML]
• Alloy, [HTML]
• Coq [HTML]
• CryptoVerif [HTML]
• Dafny [HTML]
• Isabelle [HTML]
• IVy [HML]
• Proverif [HTML]
• Spin [HTML]
• TLA+ [HTML]
• Tamarin [HTML]