Wie im Blogpost zum Thema formale Spezifikationen erläutert, kann es sehr herausfordernd sein, gute Spezifikationen als Grundlage für formale Analysen – wie zum Beispiel die Suche nach Heisenbugs – zu finden. Das neueste Ergebnis meiner Arbeit ist eine Methode namens Differential Property Monitoring, die es ermöglicht formale Spezifikationen in einem iterativen Prozess zu verfeinern, bis die gewünschte Genauigkeit erreicht ist.

Differential Property Monitoring für die Suche nach Backdoors

Als konkrete Anwendung für diese Methode, haben wir im ersten Schritt Spezifikationen aus dem Bereich der IT-Sicherheit betrachtet. Genauer gesagt haben wir uns Analysen gewidmet, die darauf abzielen, Backdoors in sicherheitskritischen Systemen zu identifizieren. Backdoors sind Hintertüren, die von Herstellern und Entwicklern absichtlich in Systeme eingebaut werden, um später unerlaubterweise auf Systeme zugreifen zu können.

Diese Anwendung ist besonders spannend, da eine gute Spezifikation dem möglichen Angreifer immer einen Schritt voraus sein muss. Das bringt besondere Herausforderungen mit sich. Ein Highlight unserer Arbeit war der Nachweis, dass unsere Methode geeignet ist, eine passende Spezifikation für die Suche nach einer Backdoor in der Linux XZ-Bibliothek zu entwickeln – einer Sicherheitslücke, die im Jahr 2024 die IT-Welt erschüttert hat.

Veröffentlichung auf der ICFEM 2024

Ich freue mich bekanntzugeben, dass ein Paper zu diesem Thema nach einem sorgfältigen Peer-Review-Prozess auf der International Conference on Formal Engineering Methods (ICFEM) 2024 zur Veröffentlichung akzeptiert wurde.

Titel und Abstract der Publikation sind wie folgt:

Otto Brechelmacher, Dejan Ničković, Tobias Nießen, Sarah Sallinger, Georg Weissenbacher  “Differential Property Monitoring for Backdoor Detection”.

Abstract:

A faithful characterization of backdoors is a prerequisite for an effective automated detection. Unfortunately, as we demonstrate, formalization attempts in terms of temporal safety properties prove far from trivial and may involve several revisions. Moreover, given the complexity of the task at hand, a hapless revision of a property may not only eliminate but also introduce inaccuracies in the specification. We introduce a method called differential property monitoring that addresses this challenge by monitoring discrepancies between two versions of a property, and illustrate that this technique can also be used to analyze observations of untrusted components. We demonstrate the utility of the approach using a range of case studies – including the recently discovered xz backdoor.

Ich durfte das Paper im Dezember 2024 im Zuge der Konferenz in Hiroshima, Japan präsentieren. Der Vortrag stieß beim Publikum auf reges Interesse und führte in den folgenden Tagen zu vielen spannende Diskussionen.