SluitenHelpPrint
Switch to English
Cursus: 201500039
201500039
Security Verification
Cursus informatieRooster
Cursus201500039
Studiepunten (ECTS)5
CursustypeCursus
VoertaalEngels
Contactpersoonprof.dr. M. Huisman
E-mailm.huisman@utwente.nl
Docenten
VorigeVolgende 5
Docent
A.B. Ahmad
Docent
dr. T. van Dijk
Contactpersoon van de cursus
dr. T. van Dijk
Docent
dr. A. Fehnker
Docent
dr. M. Gerhold
Collegejaar2021
Aanvangsblok
JAAR
AanmeldingsprocedureZelf aanmelden via OSIRIS Student
Inschrijven via OSIRISJa
Cursusdoelen
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.
Inhoud
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 thiscourse, 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.

Assessment:
The student and supervisor together decide how the student will report on the work done. Typically, this will be done in the form of a report, and a presentation to the FMT group.
Voorkennis
Mandatory: Software Security, System Validation
knowledge of first-order logic, basics of program specifications (pre- and postconditions)
Participating study
Master Computer Science
Verplicht materiaal
-
Aanbevolen materiaal
-
Werkvormen
Project begeleid
AanwezigheidsplichtJa

Toetsen
Individual take home assignment

SluitenHelpPrint
Switch to English