Credits: 5 EC
Prerequisites:
- Software Security (201600051) or Language Based Security (CS4106) and
- System Validation (192140122) or System Validation (IN4387).
Prerequisites checklist: For this course, you are expected to have a working knowledge of the following concepts:
- Writing formal specifications in first-order logic (SV manual, chapter 2)
- Temporal logic (SV manual, chapter 4)
- Program annotations (SV manual, chapter 6 or KeY book, chapter 7)
- Dynamic validation of program behaviour (SV manual, chapters 5 + 7)
- Static validation of program behaviour (SV manual, chapter 5 + 7)
- System Modeling (SV manual, chapter 2)
- Abstraction (SV manual, chapters 9)
SV manual: Course manual System Validation (192140122), can be obtained by sending an email to Marieke Huisman.
KeY book: Deductive Software Verification - The KeY Book. LNCS, Volume 10001, Springer, 2016.
Motivation: Many security problems in software systems can be detected by using formal verification techniques in an adequate way. In this course, the students experience this in a hands-on setting: in the form of an individual project, they use a suitable formal verification technique to analyse the security of a software system.
Synopsis: This course is done in the form of an individual project. In the prerequisite courses, the students have obtained knowledge about possible security threats for software systems, and how formal techniques can be used to specify and verify the behaviour of a software system. In this course, they combine this knowledge in a concrete case study.
The student agrees with the supervisor on a suitable software system to be analysed. Possible security threats are identified, and the student then studies the literature how formal verification techniques have been used to detect the identified security threats. Based on this literature study, a suitable verification approach is identified.
The student then uses the formal verification technique to identify whether the system indeed suffers from security issues. If appropriate, a fix is proposed, and the student uses the formal verification technique to show that the security issue has been properly addressed.
Learning outcomes: The student will acquire:
- A good understanding of how formal verification techniques can be used to detect security vulnerabilities in software
- Practical experience with applying formal specification techniques to realistic software to detect security vulnerabilities.
Lecturers: Prof. Dr Marieke Huisman (Twente) & Dr Tom van Dijk (Twente) are contact persons for this course. The individual supervisor can be any member of the FMT group. This is decided in deliberation with the student, and depends on the student’s particular interest.
Examination: A report and a presentation, describing the literature studied by the student, and the work on the security analysis using formal verification of the software system at hand.
Scheduling: This course can be done throughout the year on an individual basis.
Core text: Various papers from the literature, depending on the specific case study selected.