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 cryptographic protocols, programming languages, 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.  

• Analysis of Cryptographic Protocols via type systems and SMT solving (Applied Pi-Calculus and ProVerif)
• Language-based Security (Non-Interference, Hyperproperties, and Side Channels)
• Foundations of Security Static Analysis (Taint Analysis, Symbolic Execution, SMT solving)
• Static Analysis of Bytecode (Ethereum Smart Contracts)
• Secure programming in F* 

The course is based on a combination of lectures and two projects, which provide theoretical foundations as well as hands-on experience with state-of-the-art security verification tools (ProVerif, Z3, F*).

The lectures and tutorials are released in the form of videos and slides on a weekly basis, and they are accompanied by online Q/A (question/answer) sessions. All the lectures, tutorials, and Q/A sessions are recorded and made available online.

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.