Internationale Software-Konferenz in Lübeck
Vom 6. bis 10. März 2023 findet die „Formal Methods 2023“ (FM 2023) an der Universität zu Lübeck statt. Die Agentur für Innovation in der Cybersicherheit GmbH (Cyberagentur) trägt inhaltlich zum 25. internationalen Symposium „Formal Methods Europe” bei und ist ideeller Partner der Konferenz.
Von der Cyberagentur werden Dr. Sebastian Jester, Leiter Sichere Hardware und Lieferketten und Dr. Daniel Gille, Leiter Künstliche Intelligenz, auf dem Industrietag einen Einblick in die aktuellen Forschungstrends zum Thema Cybersicherheit geben. Wir sprachen mit Beiden über das Engagement der Cyberagentur, die inhaltlichen Ziele ihrer Teilnahme und ihre Erwartungen an das Symposium.
Warum engagiert sich die Cyberagentur auf der FM 2023 in Lübeck?
Dr. Sebastian Jester (SJ): Formale Methoden sind Techniken aus der Mathematik und Logik, mit denen sich beweisen lässt, ob Software oder Hardware bestimmte Sicherheitsanforderungen einhält oder nicht. Sie bieten riesige Chancen für beweisbare IT-Sicherheit. Zum Beispiel, dass eine bestimmte Sicherheitslücke geschlossen ist.
Dr. Daniel Gille (DG): Formale Methoden können auch die Grundlage dafür schaffen, dass sich Anwendungen mit Bestandteilen aus der Künstlichen Intelligenz nachweisbar robust verhalten – beispielsweise eine Bilderkennung auch unter schwierigen visuellen Bedingungen oder gar bei gezielt manipulierten Eingabedaten korrekte Ergebnisse produziert.
Worüber werdet Ihr auf dem Industrietag in Lübeck sprechen?
SJ: Es ist leider ein komplexes Unterfangen, Cybersicherheits-Anforderungen so zu formulieren und insbesondere Software so zu schreiben, dass sich formale Methoden überhaupt einsetzen lassen, und dann auch noch möglichst automatisiert. Das ist umso schwieriger, je komplexer Software und Hardware sind. Deswegen ist es zum Beispiel eine große Herausforderung, solche Beweise für Systeme mit mehreren Prozessoren oder Prozessorkernen zu führen, was heute absoluter Standard ist für Laptops, Bürocomputer und Server.
DG: Im Bereich der neuronalen Künstlichen Intelligenz ist zudem seit Jahren eine starke Zunahme der Modellgrößen zu beobachten. Bei großen Sprachmodellen und darauf basierenden Applikationen wie ChatGPT sehen wir inzwischen Parameterzahlen im zwei- bis dreistelligen Milliardenbereich. Schon bei deutlich kleineren Modellen stoßen formale Methoden derzeit an die Grenzen ihrer Skalierbarkeit, weil die Gesamtheit der angelernten und zu verifizierenden Eigenschaften extrem groß ist. Deswegen haben wir einen großen Forschungsbedarf, wie sich formale Methoden effektiv und Programmierer-freundlich einsetzen lassen – sowohl bei der Weiterentwicklung von Methoden als auch bei der Definition gut verifizierbarer System- und (KI-)Modelleigenschaften.
SJ: Auf der FM 2023 werden wir deswegen unsere Pläne für künftige Forschungsausschreibungen vorstellen, mit denen wir diese Herausforderungen angehen.
Welche Erwartungen sind mit der FM 2023 hinsichtlich der Forschungsprojekte für die Cyberagentur verbunden?
SJ: Die FM 2023 versammelt Forscherinnen und Forscher aus ganz Europa und darüber hinaus. Wir werden dort nicht nur mit einem Vortrag die Werbetrommel für unsere geplanten Forschungsprojekte rühren, sondern uns persönlich über den Stand der Forschung informieren und das Netzwerk der Cyberagentur in diese Fachcommunity ausbauen. Denn gute Ideen entstehen im Austausch, Innovation braucht Miteinander!
Weitere Informationen zur FM 2023: