192.059 Formal Methods for Security and Privacy
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2020S, VU, 4.0h, 6.0EC
TUWEL

Properties

  • Semester hours: 4.0
  • Credits: 6.0
  • Type: VU Lecture and Exercise

Learning outcomes

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.  

Subject of course

  • 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* 

Teaching methods

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*).

Mode of examination

Immanent

Additional information

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

30h lectures, tutorials, exam

40h self-study

80h projects and exercises

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

 

 

Lecturers

Institute

Course dates

DayTimeDateLocationDescription
Wed10:00 - 12:0011.03.2020FAV Hörsaal 1 - INF Formal Methods for Security and Privacy

Examination modalities

Students will be evaluated based on a written exam and projects. 

Course registration

Begin End Deregistration end
07.02.2020 13:00 08.04.2020 14:00 19.04.2020 14:00

Curricula

Literature

No lecture notes are available.

Previous knowledge

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. 

Language

English