Ein ohrenbetäubender Piepton gellt durch den Flur im dritten Stock des Hochhauses. Nach und nach springen auch die Rauchmelder auf den übrigen Etagen an, um die Bewohner:innen vor dem Feuer zu warnen – und das schon lange bevor sich der Rauch in dicken Schwaden im gesamten Haus verbreitet hat. Denn die Melder sind verbunden und kommunizieren miteinander. CISPA-Faculty Swen Jacobs forscht an Techniken, mit deren Hilfe garantiert werden kann, dass Systeme mit mehreren kommunizierenden Komponenten fehlerfrei und sicher laufen.
Viele Systeme präsentieren sich Nutzer:innen als Ganzes, sind aber in Wahrheit ein Geflecht aus mehreren unabhängigen Prozessoren. Der Vorteil dieser sogenannten verteilten Systeme ist, dass sie mehrere Prozesse gleichzeitig ausführen können. Außerdem lässt sich ihre Leistungsfähigkeit bei Bedarf erhöhen, indem weitere Prozessoren hinzugefügt werden. Zum Einsatz kommen sie zum Beispiel beim Cloud Computing, in industriellen Steuerungsanlagen oder bei Peer-to-Peer-Anwendungen wie etwa dem Sprachchat Skype. Da die Systeme mit sensiblen Daten und sicherheitskritischen Anwendungen umgehen, ist es wichtig, dass sie vor Angriffen sicher sind und fehlerfrei laufen.
Der Aufbau verteilter Systeme ist jedoch komplex und anfällig für Fehler, da dabei viele Störfaktoren wie Hardware- oder Netzwerkausfälle sowie Cyber-Angriffe berücksichtigt werden müssen, erklärt Swen Jacobs. Je nachdem, wo die Systeme zum Einsatz kommen, können Ausfälle und Störungen ärgerlich oder sogar lebensbedrohlich sein. Deshalb ist ein wichtiger Teil des Designprozesses von Hard- und Software ihre Verifikation. Sie passiert oftmals vollautomatisch mithilfe der sogenannten Modellprüfung, bei der anhand eines Modells des untersuchten Programms oder der Hardware ein formaler Beweis geführt wird, dass dieses sich an die gemachten Vorgaben hält und seine Funktionen erfüllen wird.
Bei einem wachsenden System mit mehreren Komponenten, die interagieren und miteinander kommunizieren, kommt die Modellprüfung allerdings an ihre Grenzen. Denn was im Kleinen nachweisbar fehlerfrei läuft, muss nicht auch im Großen klappen. Jacobs Ziel ist es deshalb, formale Methoden und Tools zu entwickeln, die Sicherheitsgarantien auch für wachsende Systeme geben können, die verschiedene Prozesse gleichzeitig ausführen. „Das Thema an sich ist durchaus schon in der Praxis und bei großen Firmen wie Amazon und Google angekommen, die ja zum Beispiel auch Cloud-Dienste anbieten und deren Sicherheit garantieren müssen. Was ich mache, betrifft aber vor allem die theoretischen Grundlagen“, erklärt der 41-Jährige. Bislang sind Sicherheitsgarantien für solche Systeme abhängig von der Anzahl ihrer Komponenten, oder es kommen interaktive Verfahren zum Einsatz, bei denen Menschen an der Prüfung beteiligt sind. Das will Jacobs ändern: „Unser Traum ist, nach jeder Änderung der Komponenten eine vollautomatische Verifikation anstoßen zu können, die uns Sicherheitsgarantien für ein beliebig großes System aus diesen Komponenten gibt.“
Neben der Weiterentwicklung der Modellprüfung arbeitet seine Forschungsgruppe daran, wie Resultate aus der Modellprüfung auch auf die automatische Synthese, also die maschinelle Generierung von Systemen, die von Grund auf sicher funktionieren, übertragen werden können. Jährlich ruft Jacobs bei der Reactive Synthesis Competition Forscher:innen aus der ganzen Welt auf, neue Tools für die automatische Synthese einzureichen.
Der Saarländer hat 2010 am Max Plack Institut für Informatik (MPI-INF) in Saarbrücken promoviert und danach zunächst zwei Jahre an der École Polytechnique Fédérale (EPFL) im Schweizer Lausanne und danach zwei weitere Jahre an der TU Graz verbracht. 2014 kehrte er ins Saarland und an die Universität in Saarbrücken zurück, wo er zunächst als Postdoc an die Gruppe von Bernd Finkbeiner angegliedert war. Eine Förderung der Deutschen Forschungsgemeinschaft (DFG) verschaffte ihm allerdings schnell eine eigene Projektgruppe, die er drei Jahre lang leitete. 2019 habilitierte er schließlich an der Saar-Uni, wo er jedes Semester mehrere Vorlesungen hält. Seit dem Sommer 2018 ist er außerdem Forschungsgruppenleiter am CISPA. „Ein Glücksfall für mich.“
