Dresden, July 15, 2025 – Unsere digitale Infrastruktur ist das Rückgrat der modernen Gesellschaft – und zugleich zunehmend bedroht. Um sensible Daten und sicherheitskritische Systeme besser zu schützen, hat die Agentur für Innovation in der Cybersicherheit GmbH (Cyberagentur) das Forschungsprogramm ÖVIT (Ökosystem Formal Verifizierbare IT – Beweisbare Cybersicherheit) ins Leben gerufen. Kernkonzept beteiligt sich an der Forschungsgruppe Formula-V, um IT-Systeme mit mathematisch nachweisbarer Sicherheit zu entwickeln. Mit ihrer Expertise für sichere Betriebssysteme bringt die Dresdner Firma zentrale Bausteine für eine Zukunft ein, in der Vertrauen in Technologie nicht auf Versprechen beruht, sondern auf Beweisen.
Das ÖvIT-Projekt zielt darauf ab, Cybersicherheit von Grund auf neu zu denken – durch mathematisch nachgewiesene Korrektheit von Hardware und Software. Nur so ist sichergestellt, dass ein IT-System völlig frei von sicherheitskritischen Fehlern und Schwachstellen ist. Kernkonzept bringt seine Expertise als IT-Sicherheitsspezialist ein, mit besonderem Fokus auf Betriebssysteme und Mikrokernel-basierter Virtualisierung.
Ein formal verifiziertes IT-Ökosystem hätte immense Vorteile für die Cybersicherheit, doch bis heute gibt es dieses System noch nicht. Deshalb hat die Agentur für Innovation in der Cybersicherheit GmbH (Cyberagentur), eine Bundesbehörde, die zur Förderung von Cyber-Innovationen und zur Verbesserung der IT-Sicherheit im Bereich der inneren und äußeren Sicherheit gegründet wurde, das ÖvIT-Forschungsprogramm ins Leben gerufen, um vertrauenswürdige IT durch die Weiterentwicklung formaler Methoden in die breite Anwendung zu bringen.
ÖvIT besteht aus fünf Projekten mit unterschiedlichen Schwerpunkten. In den nächsten vier Jahren wird Kernkonzept als Teil der Forschungsgruppe Formula-V arbeiten, die auf einen holistischen Ansatz für eine vertrauenswürdige IT-Hardware- und Software-Infrastruktur abzielt und vom Barkhausen Institut geleitet wird. Die Forschungsgruppe soll durch die Entwicklung einer vertrauenswürdigen, formal verifizierbaren IT-Hardware- und Software-Infrastruktur echte „Security by Design“ ermöglichen. Grundlage dieser Arbeit wird der von Kernkonzept entwickelte L4Re Secure Separation Kernel VS 1.0.1 sein, der vom BSI für den Einsatz bis GEHEIM/NATO SECRET akkreditiert und nach Common Criteria als EAL4+ zertifiziert ist.
„Formula-V ist ein bedeutender Schritt zur Stärkung der deutschen und europäischen Cybersicherheit. Die Entwicklung von Methoden für fehlerfreie Software wird hoffentlich zu einer Zukunft mit einer viel widerstandsfähigeren IT-Infrastruktur führen”, sagt Dr. Hendrik Tews, Head of Formal Methods, der das Projekt für Kernkonzept leitet. „Die Konstruktion solider Betriebssysteme wie des L4Re Operating System Framework auf einer theoretischen und mathematischen Grundlage ist ein wichtiger nächster Schritt – und wir sind mit unserem Hintergrund in theoretischer Informatik und formalen Methoden gut darauf vorbereitet.”
Kernkonzept arbeitet mit dem Barkhausen Institut, der TU Dresden, Fraunhofer AISEC, Ferrous Systems und der TU Berlin zusammen, um die Technologie für die Entwicklung sicherer Hardware, Software und insgesamt vertrauenswürdigerer Systeme voranzutreiben. Im Mittelpunkt dieser Bemühungen steht der mathematische Nachweis der Korrektheit von Hardware und Software anhand eines formalen Modells. Durch die Verbesserung sowohl der Entwicklungswerkzeuge als auch der für formale Beweise verwendeten Techniken will das Konsortium einen wichtigen Beitrag zum Ökosystem leisten.
Gemeinsam wird ein vollständig verifizierter IoT-Hardware- und Softwarestack aufgebaut, der auf der RISC-V-Hardware-Architektur und der Programmiersprache Rust basiert, wobei alle Komponenten mit dem Rocq-Theorem-Beweiser formell geprüft werden. Mehrere Arbeitsgruppen werden die Ökosysteme für Sicherheitsmechanismen und Methoden für die Softwareentwicklung verbessern.
„Vertrauenswürdigkeit in der digitalen Welt darf keine Frage des Glaubens mehr sein. Mit Formula-V setzen wir auf mathematisch gesicherte Grundlagen, um digitale Systeme von Grund auf sicher zu gestalten – nachvollziehbar, überprüfbar und belastbar. Nur so schaffen wir echte IT-Souveränität“, sagt Prof. Dr. Gerhard Fettweis, Wissenschaftlicher Leiter und Gründer des Barkhausen Instituts.
Zum offiziellen Start des ÖvIT-Projekts wurde das gesamte Forschungsprogramm an das Dresdner Projektbüro übertragen, das von Dr. Christoph Hof geleitet wird. Dresden, Deutschlands Zentrum für Betriebssysteme und Mikroelektronik, wird damit auch zum Zentrum des neuen Ökosystems der nachweisbar sicheren IT.
Kernkonzept wurde vor mehr als zehn Jahren als Spin-off der Fakultät Informatik der TU Dresden gegründet und hat seinen Sitz nach wie vor in Dresden. Die strategische Entscheidung, das Mikrokern-System L4Re nach dem Principle of Least Authority (POLA) aufzubauen und damit strikt dem Paradigma Security by Design zu folgen, war der Grundstein dafür, dass das Unternehmen heute seine Expertise einbringen kann.
„Mit dem Aufbau einer vertrauenswürdigen IT durch formale Verifikation von Hard- und Software heben wir die IT-Souveränität in Deutschland und Europa auf ein neues Niveau, insbesondere für sicherheitskritische Systeme“, sagt Dr. Michael Hohmuth, Gründer und Geschäftsführer von Kernkonzept.
