Theoretical Computer Science

Seminar

Winter Term 2024/2025

News

Organisation

• Weekly Talks are on Mondays, 17:00, in IZ 358. Starting from 04.11.24.
• The kickoff meeting will take place on the 21.10. at 12:00 in room IZ 358.
• To fully register for the seminar, you have to sign a document until 28.10.24. You can do so during the kickoff meeting or at our secretariat. In the latter case, please make an appointment with our secretary Andrea Soleinsky (a.soleinsky@tu-bs.de).
• We give topics to at most 10 students.
• This is a joint seminar for Bachelor's and Master's students of computer science.

Topics

• Overview paper on Side-Channels Paper
• Overview on speculative Side-Channel Attacks (Spectre) Paper
• Formal Semantics for Constant-Time Programming Paper
• Formal Semantics for speculative execution Paper
• Static Taint System to avoid Spectre Attacks Paper
• Symbolic Execution to find Spectre attacks Paper
• Formal analysis of compiler-mitigations against Spectre Paper
• Formal proofs to preserve side-channel security under compilation Paper
• A formal hardware description language to express side-channel security Paper
• Verifying Hardware description against formal side-channel semantics Paper

Presentation Schedule

• 04.11.24:
  • Anton Opaterny, nekton: a linearizability proof checker. Abstract: nekton is a new tool for checking linearizability proofs of highly complex concurrent search structures. The tool’s unique features are its parametric heap abstraction based on separation logic and the flow framework, and its sup- port for hindsight arguments about future-dependent linearization points.
  • Jakob Tepe, Logics for Program Synthesis, Abstract: This talk presents Realizability and Realization Logic. Given a search space, a precondition "Pre", and a postcondition "Post", the goal of program synthesis is to find a program "prog" in the search space which adheres to the specification, i.e. the Hoare triple {Pre} prog {Post} holds. Realizability Logic proofs whether the search space even contains such a program. Realization Logic uses the Realizability Logic proof and extracts the sought after program from it.
• 11.11.24
  • Thomas Haas CAAT: consistency as a theory Abstract: We propose a family of logical theories for capturing an abstract notion of consistency and show how to build a generic and efficient theory solver that works for all members in the family. The theories can be used to model the influence of memory consistency models on the semantics of concurrent programs. They are general enough to precisely capture important examples like TSO, Power, ARM, RISCV, RC11, IMM, and the Linux kernel memory model. To evaluate the expressiveness of our theories and the performance of our solver, we integrate them into a lazy SMT scheme that we use as a backend for a bounded model checking tool. An evaluation against related verification tools shows, besides flexibility, promising performance on challenging programs under complex memory models.
• 18.11.24
  • Eren Keskin, Separability in VASS and solving non-linear systems of inequalities, Abstract: Büchi vector addition systems with states (Büchi VASS) are finite automata that are augmented with counters, and receive infinite words as input. The regular separability problem for Büchi VASS asks whether the languages of two Büchi VASS are separable by a regular language. This problem has been shown to be decidable, but with a non-primitive recursive upper bound. Here, the bottleneck was deciding the existence of runs in the VASS with certain non-linear properties. In this talk, we observe that the non-linear equation systems that correspond to these properties are guaranteed to have short solutions, and therefore can be efficiently handled. This yields the solution to the separability problem.
  • TBD
• 25.11.24 TBD
• 02.12.24
  • Philipp Schärper, Timing Side-channel Attacks and Countermeasures in CPU Microarchitectures
  • Felix Michel, A Systematic Evaluation of Transient Execution Attacks and Defenses
• 09.12.24 Cookies und Punsch mitbringen!
  • Caroline Krebs, Constant-Time Foundations for the New Spectre Era
  • Dimitri Teguia, Spectector: Principled Detection of Speculative Information Flows
  • Oussama Dhrif, Automatic Detection of Speculative Execution Combinations
• 16.12.24
  • Julia Mühlhausen, Automatically eliminating speculative leaks from cryptographic code with blade
  • Marc Majohr, Spectre Declassified: Reading from the Right Place at the Wrong Time
• 06.01.24
  • Elias Kaiser, Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”
  • Lina Breuer, Exorcising Spectres with Secure Compilers
• 13.01.24
  • Jamal Suleiman, A Hardware Design Language for Timing-Sensitive Information-Flow Security
  • Gianluca Letizia, Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts
• 20.01.24
  • Sebastian Brunke, Datalog with Negation and Monotonicity
  • Alex Alfano, Queries with guarded Negation
  • Finn Senft, Containment of queries for graphs with data

Requirements

Requirements

• prepare and give a talk of 30 minutes (including questions) during the lecture period, and
• write a seminar paper in English or German, of maximal 10 pages using the acmart LaTeX style using the acmsmall version until 17.01.25.
• On 17.01.25, you will hand in a preliminary version of your paper, that will be peer reviewed by another student. Consequently, you will recieve a paper from another student that you will have to review until 24.01.25.

Supervision