Interview mit BI Forschungsgruppe Verified System Design Automation
In diesem Interview gibt die Forschungsgruppe Verified System Design Automation des Barkhausen Instituts Einblicke in ihre aktuelle Arbeit und ihre Forschungsschwerpunkte. Ergänzend dazu teilen einzelne Gruppenmitglieder ihre persönlichen Perspektiven und Erfahrungen.
“Ich habe Korrektheit schon immer der Leistung vorgezogen. Denn was nützt ein System, das in manchen Fällen besonders gut funktioniert, aber in allen anderen versagt? Außerdem sehe ich eine besondere Schönheit in Beweisen. Ein Algorithmus mit beeindruckenden Leistungswerten wird oft schon nach wenigen Monaten durch einen anderen ersetzt. Ein Beweis hingegen bleibt gültig.”
- Sebastian Ertel (Research Group Leader)
Was ist das Forschungsthema eurer Gruppe?
Das Team Verified System Design Automation wendet formale Verifikation an, ein mathematisches Verfahren zur nachweisbaren Absicherung von Systemeigenschaften. Dabei werden häufig Theorembeweiser eingesetzt, also Softwarewerkzeuge, die mathematische Beweise erstellen und deren Korrektheit überprüfen. Diese Methoden unterstützen den Entwurf, die Spezifikation und die Implementierung von Programmiersprachen, Betriebssystemen und Hardware.
An welchem Projekt arbeitet ihr derzeit?
Derzeit ist das Team stark in das Projekt Formula-V eingebunden. Ziel dieses Projekts ist es, eine nahezu lückenlose Verifikation eines Unikernels bereitzustellen, der auf einem RISC-V-Prozessor läuft.
"Gegen Ende meines Bachelorstudiums habe ich an einem Seminar des Turing-Preisträgers Silvio Micali mit dem Titel „Proofs, Secrets and Computations“ teilgenommen. Dieses Ereignis hat mich dazu inspiriert, mich intensiver mit den Bereichen Logik und Kryptographie zu beschäftigen."
- Carmine Abate (Senior Researcher)
Wie hängt eure Forschung mit dem Alltag zusammen? Welche Probleme und Herausforderungen versucht ihr zu lösen?
Unser zentrales Ziel ist es, digitale Systeme vertrauenswürdiger zu machen. Da solche Systeme unseren Alltag immer stärker durchdringen, betrifft unsere Forschung nicht nur unser eigenes Leben, sondern auch das vieler anderer Menschen. Formale Verifikation ist jedoch keineswegs so einfach wie das Zählen von 1, 2, 3. Die Erstellung einer Spezifikation für ein System und der anschließende Beweis, dass dieses System tatsächlich dieser Spezifikation entspricht, ist ein anspruchsvoller Prozess. Wir versuchen, diese Herausforderung zu erleichtern, indem wir Compiler und Automatisierung in unsere Verifikationswerkzeuge integrieren.
“Formale Verifikation ist definitiv nicht einfach. Es gibt Momente, in denen es sich anfühlt, als würde sich jeder Beweis gegen einen stellen. Aber die Zufriedenheit, ein schwieriges Problem schließlich gelöst zu haben und zu wissen, dass man damit die Grundlagen kryptographischer Sicherheit stärkt, macht den gesamten Aufwand lohnenswert. Es ist eine anspruchsvolle, aber zutiefst erfüllende Arbeit.”
- Sara Zain (Senior Researcher)