PROTECT - Proving Next Generation Secure Systems
PROTECT möchte mit innovativen Methoden der formalen Verifikation die IT-Sicherheit auf ein neues Niveau heben und das Vertrauen in digitale Systeme nachhaltig stärken.
Die Projektmitglieder sind:
- Deutsche Forschungszentrum für Künstliche Intelligenz (DFKI)
- RWTH Aachen Universität,
- Cryspen SARL,
- Gesellschaft für Informatik e.V. ,
- RPTU Kaiserslautern,
- LUBIS EDA GmbH,
- Universität zu Lübeck
Gemeinsam entwickeln die PROTECT-Partner Lösungen, um IT-Systeme widerstandsfähiger gegen Cyberangriffe auf Unternehmen und öffentliche Einrichtungen zu machen. Der Ansatz setzt dabei auf drei Stärken der beteiligten Partner:
Bottom-up statt top-down. Wir kombinieren die existierenden Ansätze der beteiligten Partner, und kombinieren damit existierende Stärken, anstatt Projektpartner in ein vorgegebenes Korsett existierender Methoden zu zwingen. Gleichzeitig erlaubt dieser Ansatz Anwendern, aus den so kombinierten Methoden die für den Anwendungsfall passenden auszuwählen.
Open Source und Open Science. Unsere Arbeiten werden quelloffen oder als open access veröffentlicht, und sind damit möglichst breit verfügbar.
Forschungsgetrieben. Alle wissenschaftlichen Partner sind auf ihrem jeweiligen Anwendungsgebiet exzellent etabliert, und bringen diese Forschungsstärke in das Projekt gewinnbringend ein. Technisch nutzen wir fortschrittliche Technologien und Sprachen: fortgeschrittene Verifikationstechniken, SAIL für die ISA-Spezifikation, eine Reihe von Referenzsystemarchitekturen auf der Basis von RISC-V, und Rust als Implementierungssprache.
Beiträge zur formalen Verifikation
Der Schwerpunkt des PROTECT-Projekts liegt auf der Sicherheit an der Schnittstelle zwischen Hardware und Software. Die wichtigsten Beiträge sind:
- Unser Partner Cryspen entwickelt Tools zur Verifikation von Rust-Programmen, darunter die Hax-Toolchain und eine verifizierte kryptografische Bibliothek für Rust.
- Die Partner RWTH Aachen und DFKI entwickeln virtuelle Prototypen für die frühe Entwicklung und Verifikation von Software. Sie stellen virtuelle Prototypen aller Referenzsysteme bereit und untersuchen Methoden zur nahtlosen Generierung und Verifizierung von Sicherheitseigenschaften unter Verwendung von SAIL als ISA-Spezifikationssprache.
- Die Partner RPTU Kaiserslautern, Universität zu Lübeck und Lubis EDA entwickeln Methoden zur Etablierung einer sicheren Mikroarchitektur als Vertrauensbasis. Unter Verwendung von formalisierten Bedrohungsmodellen entwickeln sie Sicherheitsmechanismen über die HW/SW-Schnittstelle hinweg für ein sicheres Design.
Demonstrationssysteme
PROTECT wird virtuelle Prototypen von Referenzsystemen mit zunehmender Komplexität liefern, die auf der Open-Source-RISC-V-Architektur basieren, um die Methoden zu demonstrieren. Ausgehend von einem Basissystem (RISC-V 32 Bit ohne Erweiterungen) ohne Betriebssystem entwickeln die Projektpartner ein mittleres System (RISC-V 32 Bit mit Erweiterungen) mit einem Mikrokernel (wie seL4) und Basisbibliotheken (z. B. einer in Rust entwickelten Krypto-Bibliothek), die in eingebetteten Umgebungen zu finden sind, sowie ein großes System (RISC-V 64 Bit) mit einem vollständigen Betriebssystem (wie Linux), das z. B. als Server verwendet wird. Mit der Skalierung der Systeme skalieren sie auch ihre Verifikationsmethoden, sodass sie auch große Systeme verifizieren können, wobei die Verifikationsabdeckung bei Bedarf verringert werden kann.
Community Building
PROTECT und ÖvIT haben das Ziel, die Anwendbarkeit formaler Verifikation zu verbessern. Dafür ist eine Vernetzung für Forschung und Entwicklung unerlässlich. Die Gesellschaft für Informatik betreibt hierzu Vernetzungs- und Kooperationsangebote, um Synergien zwischen den Projektpartnern hervorzuheben. ZIel soll der Aufbau eines Ökosystems für Anwender*innen und Entwickler*innen sein.
