Credits: 5EC
Prerequisites: Software Security
Motivation: Many security problems in software systems can be detected by using formal verification techniques in an adequate way. This course provides the students the techniques to do this.
Synopsis: The course studies several (general) formal specification techniques, in particular process algebras and program logics. It also discusses appropriate verification techniques for these specification formalisms: model checking for process algebras, and runtime and static verification for program logics. The students will learn how to apply these techniques to detect problems in authentication protocols, and to detect common security vulnerabilities in software. The course builds on the knowledge on software vulnerabilities obtained during the Software Security course.
Learning outcomes: The student will acquire:
- A good understanding of program logics, and how they can be used to detect security vulnerabilities in software
- A basic understanding how program logics can be used to capture other security properties, such as information flow security
- A good understanding of process algebras and how they can be used to specify and verify the behaviour of authentication protocols
- Practical experience with applying formal specification techniques to realistic software to detect security vulnerabilities.
Lecturers: Prof. Dr Marieke Huisman (Twente) & Prof. Dr Jaco van de Pol (Twente)
Examination: Two individual paper presentations in a seminar format and a group homework assignment, applying the proposed techniques on a non-trivial open source software example.
Contents: Process algebra (basics + data), JML modelling, static checking, run-time verification, verification of authentication protocols, Dolev Yao, security engineering, buffer overflows, data races, information flow.
Core text: Part of the written material for the courses System Validation and Modeling and Analysis of Concurrent Systems I (on formal specification and verification techniques), plus extra security-specific papers.
Scheduling: The course should be scheduled in Q1 (and only will be offered starting 2016-2017). The lectures will partly coincide with lectures in the courses System Validation and Modelling and Analysis of Concurrent Systems 1.
Participation: A maximum of 10 students can participate in this course. Students from Delft can participate. For most lectures, a Skype connection will be arranged, but 1 or 2 trips to Twente are expected. Additionally, students from Twente are expected to come to Delft once.