Dyvercon
Kry10 hat sich in Zusammenarbeit mit Proofcraft zum Ziel gesetzt, eine neue Klasse von eingebetteten und cyber-physikalischen Systemen zu ermöglichen, mit formal verifizierter Unterstützung für aktualisierbare Multicore-Systeme, die auf dem verifizierten seL4-Mikrokernel basieren. Damit das System auf mehreren Rechenkernen läuft, wird eine Multikernel-Konfiguration von seL4 verwendet, mit einer separaten seL4-Kernel-Instanz pro Kern. Für Software- und Konfigurationsaktualisierungen ohne Ausfallzeiten entwickelt das Team eine privilegierte User-Space-Komponente, die eine hochrangige API für die Authentifizierung und Ausführung von Aktualisierungsbefehlen bereitstellt. Zur formalen Verifikation werden sie Theorembeweis-Frameworks entwickeln, um die Korrektheit von Multikernel-Konfigurationen auf Kernel-Ebene und die Korrektheit von privilegierten Komponenten auf User-Ebene zu überprüfen. Eine große Herausforderung bei der Verifikation ist die Parallelität zwischen mehreren Kernel-Instanzen und User-Space-Threads.
Die Projektmitglieder sind:
- Kry10
- Proofcraft
Beiträge zur formalen Verifikation
Demonstrator
Als Demonstrator wird Kry10 ein Lehrsystem für Mechatronik entwickeln. Das System wird ein kleines Robotergerät mit einer Reihe von Übungen zur Vermittlung von Steuerungstheorie und sicherer Systementwicklung umfassen. Studierende werden Übungen absolvieren, indem sie Software-Updates für das System entwickeln und die Prozesse auf mehrere Kerne verteilen. Das System soll demonstrieren, dass die Studierenden nicht die vollständige Kontrolle über das System erlangen können, obwohl sie Teile des Codes bereitstellen.
Verifizierte Teile des Systems
- Der seL4-Mikrokernel, der bereits für Single-Core-Konfigurationen verifiziert wurde und bei dessen Verifikation für Multikernel-Konfigurationen erhebliche Fortschritte erzielt wurden.
- Privilegierte Komponenten im Benutzerbereich, die für die Systemkonfiguration und Updates ohne Ausfallzeiten verantwortlich sind.
- Teile der Treiber für Peripheriegeräte, die für die Konfiguration des direkten Speicherzugriffs (DMA) verantwortlich sind.
- Eine Systemintegritätseigenschaft, die verhindert, dass nicht verifizierte Komponenten die von verifizierten Komponenten erzwungenen Invarianten verletzen können.
Arbeitsschritte
- Verifikationsframeworks auf Kernel-Ebene für die Analyse paralleler Systeme, wobei der Schwerpunkt auf der maximalen Wiederverwendung bestehender sequenzieller Verifikationen liegt.
- Verifikationsframeworks für den Benutzerbereich zur Spezifikation und Verifikation der funktionalen Sicherheit und Integrität paralleler dynamischer seL4-basierter Systemdesigns, wobei der Schwerpunkt auf Kompositionalität und Automatisierung der Verifikation liegt.
- Einen systematischen Ansatz für das Design hochsicherer dynamischer Systeme mit Unterstützung für inkrementelle Updates und Tools, die Entwicklern helfen, sichere dynamische Systeme zu spezifizieren und zu erstellen.
- Eine Multikernel-Konfiguration von seL4, die die Verwendung mehrerer CPU-Kerne ermöglicht, mit formaler Sicherheit, die im Laufe des Projekts erhöht wird und später auf vollständiges symmetrisches Multiprocessing (SMP) erweitert werden kann.
- Eine Methode zur Gewährleistung der sicheren Konfiguration von Peripheriegeräten, die Legacy-Direct Memory Access (DMA) verwenden, um die Systemintegrität bei nicht vertrauenswürdigen Gerätetreibern zu schützen.
- Eine Referenzplattform, einschließlich eines Software-Entwicklungskits und einer unterstützten Hardwarekonfiguration, die die Ergebnisse des Projekts zusammenführt.
Matt Brecknell
E-Mail: matt[at]kry10[dot]com