Swen Jacobs

Lehre von Swen Jacobs

Winter 2021/22

Formal Methods for Finding and Fixing Information Leaks

Seminar Topic

Information leaks are a security topic that makes it to the news regularly, with side-channel attacks like Spectre showing how vulnerable much of our information infrastructure is. Systems that store and manipulate sensitive data should be secured against information leaks, but attackers keep finding more sophisticated attacks on systems that have been deemed secure thus far, exploiting side-channels and low-level behavior of the system hardware. Due to the abundance of possible leaks, it is almost impossible for a human designer to prevent them, and automatic formal methods can play a crucial role in finding and fixing such leaks.

In this seminar, students will learn to present, discuss, and summarize papers that aim at formalizing, analyzing and automatically fixing information leaks. The seminar is split into two parts. The first part will take the form of reading sessions, where we lay the foundations of the topic. For the second part, each student is assigned a recent paper from the research area. Students will present their paper and will write a seminar paper on the topic assigned to them, taking into account connections to the topics discussed in the seminar.

Important Dates

First Meeting: tba.

During our first meeting, I will present a short overview of the content and format of the seminar.

Requirements

Reading Group: In the reading group sessions, we discuss background papers that lay the foundations, or give an overview of the recent work on formal methods for security. Each paper will be presented informally by selected students, followed by a joint discussion. The list of papers for the reading group will be announced soon.

Talks: At the first reading group session, each participant will be assigned a topic. Each topic will be presented by the respective student, followed by joint discussion. For the discussions, it is important that every participant has read the paper(s) that are presented. The list of presentation topics will be announced soon.

Summary: At the end of the seminar we would like you to submit a summary of the seminar topics, including a comparison of your topic to the ones presented by other students.

Winter 2021/22

Parameterized Verification

Advanced Lecture (Vertiefungsvorlesung), Winter Term 2021/22, 6 CP

Lecture Room:	tba.
Lectures:	tba.
Tutorials:	tba.
Exams:	tba.

Topic

We consider the problem of providing correctness and security guarantees for systems that scale with some parameter, e.g., the number of nodes in a network, the number of concurrent processes in a multi-threaded program, or the size of a data structure that a program operates on. Most systems are expected to scale in one or several parameters, but correctness and security guarantees are usually only given for fixed parameter values. In contrast, parameterized verification is the problem of obtaining correctness guarantees for all parameter values. In this course, we will look at methods for parameterized verification and investigate their capabilities and limitations.

The course is aimed at students interested in the theoretical concepts behind parameterized verification, which generalize system models, specification formalisms and proof methods from standard verification approaches. The course picks up on some of the topics of the core lecture "Verification", which is highly recommended, but not a prerequisite for this course.

References

The course will be loosely based on the following textbook, supplemented by recent research results in the area:

Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
Morgan&Claypool, Synthesis Lectures on Distributed Computing Theory (2015)

(hardcopies should be available in the library, a PDF is available through CMS)

Winter 2019/20

Advanced Lecture: Reactive Synthesis

This course is aimed at students that are interested in reactive synthesis in its full breadth, ranging from its theoretical formalization as an infinite game to efficient algorithms and data structures to solve the synthesis problem, and in the implementation of state-of-the-art algorithms for practically relevant and challenging problems.

Winter 2019/20

Seminar: Formal Methods for Security

Engineering of secure systems is an arms race between attackers and system designers. In recent years, hardly a week goes by without the discovery of a new attack, and system designers scrambling to plug the holes. Formal methods are a means to break out of this arms race by ruling out entire classes of attacks once and for all.