News

Postponing the QA session

Written on 27.11.23 by Hamed Nemati

Due to some technical problems, I have to cancel the QA session today and postpone it to tomorrow at 16. If it doesn’t work for you. I will aslo be present in the next week QA session to answer your questions. We apologise for the inconvenience.

Q&A Schedule Update

Written on 27.11.23 by Faezeh Nasrabdi

Dear all, 

The question and answer session will be held today via zoom.

Best,
Faezeh

PROTO1 in hybrid mode

Written on 24.11.23 by Robert Künnemann

Hi!

With the SYS part concluded, we move on to the PROTO part. The next four lectures will take place in CISPA E9.1, room 0.02 again, like the intro lecture. Of course, we will also set up zoom at the usual URL.

I've put up the full lecture script for PROTO part in the material's section. Feel… Read more

Hi!

With the SYS part concluded, we move on to the PROTO part. The next four lectures will take place in CISPA E9.1, room 0.02 again, like the intro lecture. Of course, we will also set up zoom at the usual URL.

I've put up the full lecture script for PROTO part in the material's section. Feel free to read ahead and think about questions for the lecture (if you want), but wait for questions in askbot until we covered that chapter in the lecture (one chapter = one lecture).

See you, Robert

Exercise sheet 1

Written on 17.11.23 by Hamed Nemati

Due a few requests, we have extended the deadline for the submission of exercise for the lecture 1 until tomorrow evening.

SysV's Third Lecture

Written on 15.11.23 by Faezeh Nasrabdi

Dear all,

You can find the recorded lecture and slides for the third lecture of SysV on its page.

Best,
Faezeh

Q&A Schedule Update

Written on 13.11.23 by Faezeh Nasrabdi

Dear all, 

The question and answer session will be held today at 16:30 instead of 16:00.

Best,
Faezeh

SysV's second lecture via zoom

Written on 09.11.23 by Faezeh Nasrabdi

Dear all,

The SysV's second lecture will start in about 5 minutes via zoom. 

Best,
Faezeh

SysV's Second Lecture

Written on 08.11.23 by Faezeh Nasrabdi

Dear all,

You can find the recorded lecture and slides for the second lecture of SysV on its page.

Best,
Faezeh

SysV's Lectures Schedule Update

Written on 02.11.23 (last change on 02.11.23) by Faezeh Nasrabdi

Dear all,

Hamed will give the next lectures for this part of the course (SysV) via zoom. Therefore, there will be no in-person class on the following dates:
 
- 09 November 2023
- 16 November 2023
- 23 November 2023

Best,
Faezeh

SysV's first lecture

Written on 02.11.23 by Faezeh Nasrabdi

Dear all,

You can find the recorded lecture, slides, notes on formalization of noninterference and the first assignment on SysV page.
Please check the materials, we will be present in the Q&A session to answer your questions.

Best,
Faezeh

Show all
Formal Methods in Security

Despite decades of research in computer security, security vulnerabilities still plague computer systems with an ever-growing number of new vulnerabilities discovered every day. How can we ensure that computer systems are really secure? Formal methods offer a promising approach towards this goal: they can guarantee the absence of specific security vulnerabilities with mathematical certainty and therefore help us develop mode reliable systems.

In this course, we will study how formal methods can be applied to verify that the design and implementation of computer systems respect their intended security policies. The course is structured in three independent parts, which focus on specific techniques for different domains: language-based information-flow control, security protocols, and system-level verification. As a whole, the course will give you hands-on experience in reasoning about security at different layers of abstraction through established principled techniques and a broad introduction to state-of-the-art research in the area.

Topics and Instructors

  1. Introductory Lecture (26 October 2023)  
    We'll give an overview of the three parts. Robert will give it live while Hamed and Xaver will use Zoom (find the zoom link in the calendar entry, calendar link is below -- not in the CMS timetable).
     

  2. Proof techniques for system verification (Hamed Nemati & Faezeh Nasrabadi)
    The main goal of the first part of the course main goal is to show you how we should approach verification of large scale systems like micro-kernels and hypervisors. This is a very challenging task in practice. We will study abstraction, decomposition and refinement as techniques that usually used in practice to facilitate verification of such systems. Finally, in our last lecture we see how we can combine fuzzing and formal verification to validate systems that their verification is not feasible in practice.  
  3. Protocol Verification (Robert Künnemann)
    Protocol verification assumes that the cryptography is perfect and tries to ensure that they are used correctly. It is not about defending against super smart mathematicians exploiting biases in key streams, but equally smart hackers confusing one party about the state of another party.

    We will discuss how to get from the Alice-bob notation to a minimalistic, precise specification of the protocol and its setup
    how to formulate our security requirements and how to verify that these requirements hold, using tools that have by now reached an impressive degree of automation.
  4. Language-based Information-Flow Control (Xaver Fabian

    In the last part of the course, we will study information-flow control techniques that track how data flows in a program to enforce data confidentiality and integrity. We will discuss both static and dynamic IFC techniques based on security type systems and taint tracking, as well as techniques that track data flows in a program at a different granularity (for example per program variable or per program block). Finally, we will see how programming languages principles can be applied to formally verify that these techniques enforce security. Basic knowledge of programming languages theory is preferred, but not required.

     

     

     

     

Organization

Registration: open now! (Once you are registered here, don't forget to register in the LSF.)

When: Thu 14h-16h (official starting time is 14:15)

Where: 0.02 in E9.1 (Cispa Main Building) (all links also appear in the calendar events)

Calendar & Lecture plan: link (Click "..." next to calendar for subscription link for your favorite application).

Mode:

  1. SYSV (Hamed & Faezeh): live lectures on Thursday 14-16
  2. PROTO (ROBERT): live lectures on Thursday 14-16
  3. IFC (Xaver): live lectures on Thursday 14-16

Q&A sessions: (all information also appears in the calendar events)

When: Mon 16h-18h (sharp) starting from 06.11.2023 (Exception: we start at 16:30 on 13.11.2023 and 20.11.2023)

Where: 0.05 in E9.1 (Cispa Main Building) (Exception: it will be at room 3.21 in E9.1 on 20.11.2023 and it will be via zoom on 27.11.2023)

Exam requirements: three exercise sheets per part, 50% of total points, work in groups allowed

Exam: two oral exams (first and third part), and one project (second part). Passing requirement is >4.0 on two of the three.

Official exam date: February 19, 2024.

Course Goals

  • Understand the challenges of some open problems in computer security

  • Learn state-of-the-art techniques to address these problems and how to apply them (as a programmer, protocol designer, web developer etc.)

  • By-product: a taxonomy of where things can go wrong in security on different layers

Learning Objectives

After the course, students will be able to:

  • Understand fundamental concepts in verification. 

  • Learn how to use formal techniques to find vulnerabilities in low-level systems.

  • Gain knowledge to be able to read and understand papers in system verification.

  • Model protocols and cryptographic assumptions in the applied-pi calculus.

  • Express authentication and secrecy properties via correspondence and reachability.

  • Exploit automated tools to verify protocols.

  • Apply Information-Flow Control (IFC) techniques to the design of secure programming languages.

  • Analyze the security guarantees of IFC languages through programming languages principles.

  • Discuss problems, solutions, and open challenges presented in IFC research papers.

Target Audience

Mainly M.Sc students and interested graduate students. Interested and motivated B.Sc students should contact us and argue that (a) they are particularly interested and (b) they have the necessary background in logical reasoning to follow the course.

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.