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, bytecode, and deep neural networks.

In particular, this course explains the foundations of the static analysis of security and privacy properties, with a particular focus on SMT solving and  type systems. 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.  

Foundations  (6 lectures)

• Static Analysis of Cryptographic Protocols  (ProVerif)
• Language-based Security (Information Flow)
• Static Analysis of Bytecode (Ethereum Smart Contracts)
• Refinement Types (F*)
• Static Analysis of Deep Neural Networks 

Advanced topics (student presentations):   

• Side Channels 
• Security of Machine Learning Models
• Robustness and Fairness in Machine Learning
• Mobile Security
• Web Security
• Blockchain Security

The course is based on a combination of

• lectures on foundational topics with weekly homeworks
• student presentations of advanced topics
• one research project  

ECTS Breakdown:
---------------------------------------------------

25h lectures, presentations

50h self-study and homeworks

75h project

---------------------------------------------------
150 hours (6 ECTS)

Students will be evaluated based on homeworks, presentation, participation in class, 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.