Über das Internet kommunizieren täglich Milliarden Rechner weltweit miteinander. Das globale Datenvolumen liegt jährlich laut Schätzungen längst im vielfachen Zettabyte-Bereich. Ein Zettabyte besteht aus einer Trilliarde Bytes. Damit all diese produzierten Daten, sei es beim Ablauf eines Programms auf einem einzelnen Rechner oder bei der Kommunikation über das Internet, sicher sind, müssen Computersysteme bestimmte Anforderungen erfüllen und Protokolle genauestens festlegen, welche Regeln bei der Kommunikation gelten.
Neue Forschungsansätze zu finden, um die Sicherheit und Funktionalität von Protokollen und Hardware beweisen und garantieren zu können, treibt Forscher:innen des CISPA in Saarbrücken sowie des lothringischen Forschungsverbundes Loria in Nancy gleichermaßen um. Seit 2020 bündeln sie ihre Kompetenzen im Rahmen des Deutsch-Französischen Zentrums für Cybersicherheit. Dessen Organisator:innen, Prof. Dr. Antoine Joux vom CISPA und Prof. Dr. Marine Minier vom Loria, hatten Forscher:innen und Interessierte am Donnerstag zum neuerlichen grenzüberschreitenden Austausch eigeladen.
Nach einleitenden Worten sprachen die Forscher:innen unter anderem über die neuesten Entwicklungen im Bereich von automatischen Analysetools für Sicherheitsprotokolle beschäftigten sich mit der Frage, wie auch komplexe Korrektheitseigenschaften für Computersysteme formuliert werden können.
CISPA-Faculty Prof. Dr. Cas Cremers eröffnete den Tag mit seinem Vortrag „That nagging thing in the back of your mind: Rethinking how symbolic analysis tools model cryptographic primitives”, in dem er sich mit neuen Forschungsansätzen zu den Grundlagen automatisierter Analysetools beschäftigte, welche die Korrektheit von Sicherheitsprotokollen beweisen oder mögliche Angriffe auf diese finden sollen.
Welche Ergebnisse automatisierte Analysetools bislang schon liefern, zeigte Dr. Steve Kremer vom Institut national de recherche en sciences et technologies du numérique (INRIA) mit seinem Vortrag “Formal verification in action: an in-depth case study of LAKE-EDHOC”. Zusammen mit CISPA- und weiteren Loria-Forscher:innen hat Kremer das neuartige Schlüsselaustausch-Protokoll EDHOC (Ephemeral Diffie-Hellman Over COSE) untersucht. Die Forscher:innen konnten mit ihrer Analyse gegebene Sicherheitsversprechen bestätigen ebenso und Schwachstellen aufzeigen. Sie machten Vorschläge, wie das Protokoll weiter gestärkt werden kann.
Tim Würtele und Pedram Hosseyni studieren am Lehrstuhl von Prof. Dr. Ralf Küsters an der Universität Stuttgart. Sie waren als externe Gäste geladen und stellten in ihrem Vortrag „A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code“ ihr neues Verifikations-Tool DY* vor, das zur Sicherheitsanalyse von kryptografischen Protollcodes eingesetzt wird.
Dr. Stephan Merz sprach in seinem Vortrag „Prophecy Made Simple“ über einen neuen praktischen Ansatz zum Finden von Verfeinerungsabbildungen für Spezifikationen, für die es – zumindest auf den ersten Blick – keine Verfeinerungsabbildungen zu geben scheint.
CISPA-PhD-Studentin Jana Hofmann zeigte in ihrem Vortrag „Logics for the Specification of Hyperproperties“ auf, welche Logiken sich für welche Klassen von sogenannten Hyperproperties am besten eignen. Zudem stellte sie einen Logikansatz für Systeme mit unendlichen Zuständen vor und zeigte dessen Aussagekraft am Beispiel von Smart Contracts.
CISPA-Faculty Dr. Rayna Dimitrova bildete mit ihrem Vortrag „Logics for the Specification of Hyperproperties” den Abschluss der Vortragsreihe an diesem Tag. Sie sprach über die Möglichkeiten und Limitierungen des kürzlich vorgestellten logischen Ansatzes Probabilistic Hyper Logic (PHL), der für die Spezifikation von Hyperproperties in sogenannten Markov-Entscheidungsprozessen eingesetzt werden kann.
Im Anschluss an die Vorträge fand bei bestem Wetter ein gemeinsames Brainstorming draußen in lockerer Atmosphäre statt. Der nächste Workshop ist für den Herbst in Saarbrücken geplant.
Über das Deutsch-Französische Zentrum für Cybersicherheit
Das Zentrum ist ein Zusammenschluss der größten und renommiertesten Forschungszentren für Cybersicherheit in Europa. Das CISPA Helmholtz Center for Information Security und das INRIA/Loria in Nancy gehen seit dem Jahr 2020 gemeinsame Wege in der Cybersicherheitsforschung und widmen sich der Stärkung der Transfer- und Innovationsaktivitäten zwischen Frankreich und Deutschland. Federführend sind auf deutscher Seite Prof. Dr. Dr. h. c. Michael Backes und Prof. Dr. Antoine Joux und auf französischer Seite Prof. Dr. Jean-Yves Marion und Prof. Dr. Marine Minier.
Über Loria
Loria ist die französische Abkürzung für "Lorraine Research Laboratory in Computer Science and its Applications" (Lothringisches Forschungslabor für Informatik und ihre Anwendungen) und ist eine gemeinsame Forschungseinheit des CNRS, der Universität Lothringen und des INRIA. Diese Einheit wurde 1997 offiziell gegründet. Die Aufgaben von Loria bestehen hauptsächlich in der Grundlagenforschung und der angewandten Forschung in den Computerwissenschaften. Das Labor ist Mitglied der Fédération Charles Hermite, in der die vier wichtigsten Forschungslabors in den Bereichen Mathematik, Informations- und Kommunikationswissenschaften sowie Steuerung und Automatisierung zusammengeschlossen sind. Die wissenschaftliche Arbeit wird von den 400 Mitarbeiter:innen des Labors in 28 Teams geleistet, von denen 15 gemeinsam mit dem INRIA arbeiten. LORIA ist heute eines der größten lothringischen Forschungslabors.
