PISTIs-V
Protected Integrety and Security of Transmissions Integrating seL4 and RISC-V
PISTIs-V addressiert den Mangel eines integrierten IT-Stacks mit nachweisbarer Ende-zu-Ende-Sicherheit für eingebettete/cyber-physische Systeme. Ziel ist die Entwicklung eines Referenzsystems mit Nachweisen für starke Sicherheits- und Schutzmerkmale, die Hardware und Software sowie deren Interaktion abdecken. Insbesondere wird PISTIs-V überprüfen, ob das neue Betriebssystem LionsOS die Spezifikationen erfüllt und Sicherheits- und Schutzmerkmale garantiert. Dazu zählt unter anderem die Verhinderung der unbefugten Weitergabe sensibler Daten und die Gewährleistung von Echtzeit-Fristen unter Verwendung formal verifizierter Hardwarekomponenten. Einen wertvollen Beitrag wird auch die Entwicklung von Pancake leisten, eine neue Systemprogrammiersprache mit einem verifizierten Compiler.
Die Projektmitglieder sind:
- PlanV
- UNSW Sydney
- University of Gothenburg
Beiträge zur formalen Verifikation
Demonstrationssystem
PISTIs-V wird ein FPGA-basiertes Referenzsystem für cyber-physische Systeme auf einem teilweise verifizierten RISC-V-Prozessor entwickeln, das starke Sicherheits- und Schutzgarantien bietet, darunter der Nachweis, dass es keine unbefugte Informationsflüsse gibt und da Einhalten von Echtzeit-Fristen trotz nicht vertrauenswürdiger Komponenten im System.
Verifizierte Teile des IT-Systems
- Kritische Hardwarekomponenten, darunter die Memory Management Unit, ein Krypto-Beschleuniger, die fence.t Anweisung (erforderlich zur Verhinderung von Informationslecks) und mehrere Gerätesteuerungen (einschließlich Ethernet);
- LionsOS-Gerätetreiber für die verifizierten Controller;
- Weitere LionsOS-Komponenten, die für die Steuerung des Informationsflusses entscheidend sind;
- Erweiterungen des (zuvor verifizierten) seL4-Mikrokernels zur Verhinderung unbefugter Informationsflüsse durch den Mikroarchitekturzustand (Caches usw.).
Ziele von PISTIs-V
- Ermöglicht die erstmalige Verifizierung von Controllern und Treibern für reale Geräte, wie z. B. Ethernet, durch die Entwicklung eines Formalismus zur Spezifikation der Software-Schnittstelle von Gerätecontrollern.
- Entwickelt die Programmiersprache Pancake zur Implementierung von Gerätetreibern und verifiziert, dass der vom Compiler generierte Binärcode die Semantik des Pancake-Programms beibehält.
- Verifikation von Verilog-Implementierungen von Controllern anhand der Spezifikation der Geräteschnittstelle;
- Formale Verknüpfung von Korrektheitsnachweisen (unter Verwendung interaktiver Theorembeweise in Isabelle/HOL oder HOL4 oder automatisierten Beweisern auf Basis von SMT-Solvern) von LionsOS-Komponenten mit der verifizierten seL4-Spezifikation, was zur ersten Ende-zu-Ende-Verifikation von Komponenten im Benutzermodus auf einem verifizierten Betriebssystemkern führt;
- Nachweis, dass seL4 mit Hilfe der Anweisung fence.t der erste (und einzige) Betriebssystemkern sein wird, der verdeckte Kanäle in der Mikroarchitektur verhindern kann (dies wird auf LionsOS übertragen);
- Entwicklung eines Formalismus zur Spezifikation systemweiter Sicherheitsrichtlinien und Überprüfung, dass diese von LionsOS durchgesetzt werden, wodurch LionsOS das erste Betriebssystem mit verifizierter Ende-zu-Ende-Sicherheitsdurchsetzung wird;
- Durchführung einer fundierten und vollständigen maximalen Ausführungszeit-Analyse (WCET) von seL4 auf einem RISC-V-Prozessor und Entwicklung eines Frameworks, das die Ergebnisse dieser Analyse nutzt, um die Fristen kritischer Echtzeitkomponenten zu garantieren. Dadurch wird LionsOS zum ersten Betriebssystem, das die Pünktlichkeit von Systemen mit gemischter Kritikalität garantiert.
