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.

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.