Die zunehmende Digitalisierung und Vernetzung technischer Systeme hat die Bedeutung der IT-Sicherheit erhöht. Eingebettete Systeme, die in verschiedenen Anwendungen von der Automobiltechnik bis zur industriellen Automatisierung eine entscheidende Rolle spielen, benötigen Schutz vor sich entwickelnden Bedrohungen. Seitenkanalangriffe auf System-on-Chip (SoC)-Architekturen sind ein erhebliches Problem, da die Forschung zeigt, dass ganze SoCs, nicht nur einzelne Prozessorkerne, anfällig sein können. Diese Anfälligkeit unterstreicht die Notwendigkeit fortschrittlicher formaler Verifikationsmethoden, die das gesamte SoC und nicht nur den Prozessor berücksichtigen.

Das Projekt PROTECT (Proving Next Generation Secure Systems) begegnet diesem Bedarf, indem es neue, praktische Methoden zur umfassenden Überprüfung der Sicherheit sicherheitskritischer eingebetteter Systeme entwickelt. Das Projekt integriert etablierte Techniken aus der formalen Verifikation, dem Hardware-Software-Co-Design und der Softwareverifikation, um eine gründliche Sicherheitsanalyse zu ermöglichen. Eine auf RISC-V basierende Referenzarchitektur, die sowohl einfache als auch komplexe Systeme umfasst, wird verwendet. Diese Architektur wird die Spezifikation und Verifikation von Sicherheitseigenschaften über verschiedene Abstraktionsebenen hinweg, von der Hardware über das Betriebssystem bis zur Anwendungssoftware, erleichtern.

PROTECT zielt darauf ab, zur Entwicklung robuster und vertrauenswürdiger Hardware-Software-Plattformen der nächsten Generation beizutragen. Das Projekt fördert die Zusammenarbeit zwischen führenden akademischen und industriellen Partnern, um die Forschung voranzutreiben und eine Grundlage für zukünftige sicherheitskritische Anwendungen zu schaffen.

PROTECT begann am 20. Januar 2025 und wird von der Agentur für Innovation in der Cybersicherheit GmbH (Cyberagentur) im Rahmen des Programms "Ökosystem Vertrauenswürdige IT" (ÖvIT) finanziert. Das Deutsche Forschungszentrum für Künstliche Intelligenz (DFKI) in Bremen leitet das Projekt, an dem die Universität zu Lübeck, Forscher der RWTH Aachen und der RPTU Kaiserslautern-Landau sowie die Unternehmen Cryspen Sarl aus Paris und Lubis Eda GmbH aus Kaiserslautern und die Gesellschaft für Informatik e.V. beteiligt sind.

Das vierjährige Projekt hat ein Gesamtbudget von 9,15 Millionen Euro, wobei das Institut für IT-Sicherheit der Universität zu Lübeck 1,3 Millionen Euro für seine Forschungsbeiträge erhält (Beträge jeweils zuzüglich Umsatzsteuer).

Trustworthy Tuesday

Snackable science at 2pm CE(S)T

Date	Presenter	Title	Recording
21.10.25	Christoph Lüth	Introduction to Formal Software Verification	Link
11.11.25	Wolfgang Kunz	Introduction to Formal Hardware Verification - Designing correct and secure chips: How can formal methods help?	Link
03.12.25	Mo Fadiheh	Property Generator: Generating Formal Assertions for Trustworthy Hardware	Link
04.01.26	June Andronick	seL4: Formally Verified Software Protects from Cyber Attacks	Link
05.02.26	Pascal Sasdrich	Computer-Aided Hardware Security Verification	Link
06.03.26	Chiara Ghinami	Building Trustworthy Software with Simulation-based Testing	Link
21.04.26	Pajam Pauls	Language-Based Verification of Probabilistic Security
19.05.26	Gernot Heiser	LionOS: Performance and Security
23.06.26	Albert Rizaldi	Muncake
21.07.26	Lucas Deutschmann	Beyond Bug Hunting: Exhaustive Hardware Security Guarantees with UPEC