After successful completion of the course, students are able to develop a static analysis technique for enforcing security and privacy properties in a variety of domains, such as concurrent and distributed programs, cryptographic protocols, and bytecode.
In particular, this course explains the foundations of the static analysis of security and privacy properties, with a particular focus on type systems and SMT solving. Students will learn how to formalize a static analysis, how to prove its soundness, and how to implement it in an efficient way using state-of-the-art verification tools.
The course is based on a combination of lectures, which are based on slides released online, and two projects, which give hands-on experience with state-of-the-art security verification tools (ProVerif, Z3, F*).
ECTS Breakdown:---------------------------------------------------
30h lectures, tutorials, exam
40h self-study
80h projects and exercises
---------------------------------------------------150 hours (6 ECTS)
Students will be evaluated based on a written exam and projects.
Some background in verification and security is ideal, but motivated students with a good background in either of them are also welcome to the course.
