Part of the
4TU.
Cyber Security
TU DelftTU EindhovenUniversity of TwenteWageningen University
4TU.
Cyber Security
Close

4TU.Federation

+31(0)6 48 27 55 61

projectleider@4tu.nl

Website: 4TU.nl

Archive

4TU.CybSec Syllabus Security Verification until 2016/2017 (SeV)

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:

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.