Das Projekt Ökosystem vertrauenswürdige IT (ÖvIT) hat das Ziel, Technologien, Methoden und Tools für durchgängig formal verifizierte Software- und Hardwarekomponenten ("Basis-IT") zu erforschen und zu entwickeln sowie ein Ökosystem von Entwicklerinnen und Entwicklern bei kommerziellen Anbieterinnen sowie von Nutzerinnen und Nutzern zu etablieren. Die formale Verifikation der Sicherheitseigenschaften von Hard- und Software ermöglicht es, mathematisch-logisch zu beweisen, dass ein IT-System vollständig frei von Sicherheitslücken ist, die zuvor definierte Sicherheitseigenschaften verletzen würden. Dies kann zum Beispiel die öffentliche Verwaltung und kritische Infrastrukturen vor Schadsoftware schützen. Allerdings sind die verwendeten mathematisch-logischen Verfahren selbst unter Informatikerinnen und Informatikern Spezialkenntnisse und zudem nicht einfach oder schnell anzuwenden für Hard- und Software der heutigen Komplexität. Dafür sollen Forscherinnen und Forscher die formale Verifikation für komplexere Systeme und mit größerem Automatisierungsgrad einsetzbar machen und die dafür nötigen Methoden und Software-Tools (weiter) entwickeln. Die nötige Grundlagenforschung wird sich über einen Zeitraum von fünf bis zehn Jahren erstrecken, also mindestens ein weiteres Folgeprojekt erfordern.

Viele der wichtigsten Verwundbarkeiten von IT-Systemen sind auf wenige grundsätzliche Probleme zurückzuführen, insbesondere Pufferüberläufe und andere ungewollte Speicherzugriffe oder unzureichende Eingabeüberprüfung). Die Sicherheit von IT-Systemen hängt trotzdem immer noch davon ab, ob die Hardware und Software hinreichend sorgfältig ausgelegt, programmiert und getestet wurde. Gängige Programmier- und Testmethoden können dabei viele Fehler vermeiden und finden, aber nicht alle. Das Projekt ÖvIT verfolgt einen fundamental anderen Ansatz: IT-Sicherheit soll beweisbar werden. Dafür werden die gewünschten Sicherheitseigenschaften formal niedergelegt und Hardware und Software durchgängig so erstellt, dass die Sicherheitseigenschaften mittels "formaler Verifikation" mathematisch beweisbar erfüllt sind.

Verifikationsverfahren werden nach heutigem Stand der Wissenschaft und der Technik getrennt fürHardware und Software durchgeführt, und auch nur für einzelne Aspekte (wenn überhaupt). Derzeit existiert kein holistisches Verfahren, das eine korrekte Implementierung eines gesamten IT-Systems nachweisen kann. Die Grenzen dieser Praxis sind nicht mehr handhabbare Sicherheitsrisiken in der immer komplexeren heutigen Hard- und Software, obwohl die grundlegenden Sicherheitsprobleme hinreichend bekannt sind. Eine fundamentale Grenze der formalen Verifikation ist dabei allerdings die Komplexität der Hard- und Software, die einen mathematischen Beweis zwar in der Theorie ermöglicht, aber in der Praxis zu lange dauert."

Der Ansatz von ÖvIT ist neu, weil er eine durchgängige formale Verifikation der Sicherheitseigentschaften für Hardware und Software vorsieht. Zudem ist formale Verifikation bisher ein Spezialthema der Informatik und Elektrotechnik, etwas für die Nerds unter den Nerds. Es soll dadurch größere Verbreitung finden, dass ein hohes Augenmerk auf einfacher zu nutzende, automatisierbare Methoden und Tools gelegt wird. Das gilt gerade auch für die Pflege und Weiterentwicklung bereits verifizeirter Systeme. Ein wichtiges Ziel ist auch die Kompositionalität, also die Möglichkeit, Module zunächst einzeln zu verifizieren und dann mit vergleichsweise wenig Aufwand auch die Kombination der Module zu verifizieren. Auch das aktive Community-Building als Teil des Projekts ist ein neuer Aspekt.

Das Forschungsprojekt ist aus wissenschaftlich-technologischer Perspektive als höchst ambitioniertund wagnisbehaftet zu bewerten. Ein Projekt zur holistischen Verifikation komplexer Systemebestehend aus Hardware und Software wurde auch aus internationaler Perspektive nicht erfolgreichrealisiert. Neuere technische Entwicklungen könnten jedoch die Basis für das Projekt bilden, um einen wissenschaftliche-technologischen Durchbruch zu ermöglichen.

Um den Erfolg zu messen, sind im Projekt Referenzsysteme unterschiedliche Komplexitätsklassen zu definieren und implementieren. Die Spanne reicht in drei Stufen von einem einfachen Mikroprozessor-basierten Sytsem über ein eingebettetes System bis hin zu einem Desktoprechner oder Server. Zwischenziele sind Konzepte und Implementierung der weniger komplexen Stufen; Finaltest (voraussichtlich erst in einem Folgeprojekt) die Implementierung der komplexesten Stufe.

Bei Erfolg werden die Projektergebnisse alle interessieren, die ein Interesse an Cybersicherheit haben. Gängige Sicherheitslücken könnten in vielen IT-Systemen geschlossen werden, ob Standard-Bürosysteme oder gehärtete IT für kritische Infrastrukturen oder die nationale Sicherheit.

Die Ergebnisse aus ÖvIT sollen Systeme mit beweisbarer Cybersicherheit in die breite Anwendung kommen und so eine Reihe verbreiteter Sicherheitslücken schließen. Gleichzeitig soll der Ansatz "Cybersicherheit by Design" stärker verbreitet werden. Das neue Wissen und das enstehende Ökosystem stärken die Technologische Souveränität Deutschlands unmittelbar. Eine Beschaffungspolitik des Bundes, die einen solchen Ansatz als Anforderung formuliert, wäre flankierend ein starker Anreiz für IT-Anbieter, die Ergebnisse rasch in Anwendungen und Produkte zu transferieren.

Link zu den fünf Vorstudien zur zentralen Forschungsfrage

• https://www.cyberagentur.de/oevit-vorstudien/

Abteilung und Referat

Sichere Systeme

Kontakt

oevit@cyberagentur.de | evit@cyberagentur.de

Link zur unseren aktuellen Ausschreibung