Ein wissenschaftlicher Artikel wurde in Communications of the ACM , Oktober 2018, Band 61, Nummer 10, S. 68–77, doi: 10.1145 / 3230627, veröffentlicht

Im Februar 2017 startete ein Hubschrauber von der Landebahn der Boeing in Arizona mit der üblichen Mission: um die nächsten Hügel zu fliegen. Er flog völlig autonom. Gemäß den Sicherheitsanforderungen der US Federal Aviation Administration hat der Pilot die Bedienelemente nicht berührt. Dies war nicht der erste autonome Flug AH-6, den das Unternehmen als unbemannten kleinen Vogel (ULB) bezeichnet. Er fliegt seit vielen Jahren so. Diesmal wurde der Hubschrauber jedoch mitten im Flug einem Cyberangriff ausgesetzt. Der Bordcomputer griff die schädliche Software des Camcorders sowie den Virus an, der über das infizierte Flash-Laufwerk übertragen wurde, das während der Wartung eingesetzt wurde. Der Angriff bedrohte einige Subsysteme, konnte jedoch den sicheren Betrieb des Flugzeugs nicht beeinträchtigen.

Schlüsselideen

• Formale Beweise aus der Softwarearchitektur eines verifizierten Mikrokernels können kostengünstig auf reale Systeme skaliert werden.
• Unterschiedliche Sicherheits- und Zuverlässigkeitsniveaus innerhalb desselben Systems sind möglich und wünschenswert. Es ist nicht erforderlich, die maximale Zuverlässigkeit des gesamten Codes sicherzustellen.
• Ein moderates Redesign und Refactoring reicht aus, um vorhandene Systeme auf das Niveau eines hochzuverlässigen Codes zu heben.

Sie könnten denken, dass die militärische Luftfahrt einen solchen Cyberangriff leicht abwehren kann. In Wirklichkeit hat das von der DARPA-Agentur im Rahmen des HACMS-Programms (High Assurance Cyber ​​Military Systems) beauftragte Team professioneller Pentester 2013 erfolgreich die erste Version der ULB-Software gehackt, die ursprünglich entwickelt wurde, um Flugsicherheit und nicht Schutz zu gewährleisten von Cyberangriffen. Hacker hatten die Möglichkeit, einen Hubschrauber zum Absturz zu bringen oder ihn an einem beliebigen Ort zu landen. Daher kann das Risiko solcher Angriffe mit einem Passagier an Bord kaum überschätzt werden, und ein erfolgloser Hacking-Versuch im Februar 2017 weist auf einige grundlegende Änderungen in der Software hin.

Dieser Artikel erklärt diese Änderungen und die Technologie, die sie ermöglicht hat. Dies ist eine Technologie, die im Rahmen des HACMS-Programms entwickelt wurde, um den sicheren Betrieb kritischer Systeme in einer feindlichen Cyberumgebung zu gewährleisten - in diesem Fall mehrerer autonomer Fahrzeuge. Die Technologie basiert auf einer formalen Softwareüberprüfung - dies sind Programme mit automatisch verifizierten mathematischen Beweisen, die gemäß ihren Spezifikationen arbeiten. Obwohl der Artikel nicht den formalen Methoden selbst gewidmet ist, wird erläutert, wie die Artefaktüberprüfung zum Schutz realer Systeme in der Praxis verwendet wird.

Das vielleicht beeindruckendste Ergebnis von HACMS ist, dass die Technologie auf vorhandene reale Systeme erweitert werden kann, wodurch deren Schutz vor Cyberangriffen erheblich verbessert wird. Dieser Prozess wird als "Nachrüstung der seismischen Sicherheit" bezeichnet, ähnlich wie bei der Aufrüstung seismischer Gebäude. Darüber hinaus wurde der größte Teil des Reengineerings von Boeing-Ingenieuren und nicht von Spezialisten für formale Verifizierungen durchgeführt.


"Vogel" während eines unbemannten Testfluges

Nicht jede Hubschraubersoftware basiert auf mathematischen Modellen und Beweisen. Der Bereich der formalen Überprüfung ist für eine solche Skala noch nicht bereit. Das HACMS-Programm hat jedoch gezeigt, dass die strategische Anwendung formaler Methoden auf die wichtigsten Teile des Gesamtsystems den Schutz erheblich verbessert. Der HACMS-Ansatz funktioniert für Systeme, in denen das gewünschte Sicherheitsmerkmal durch reine Durchsetzung auf Architekturebene erreicht werden kann. Es basiert auf unserem sel4-verifizierten Mikrokernel, über den wir weiter unten sprechen werden. Es garantiert die Isolation zwischen Subsystemen mit Ausnahme klar definierter Kommunikationskanäle, die den Sicherheitsrichtlinien des Systems unterliegen. Diese Isolation wird auf Architekturebene mit dem von CAmkES verifizierten Framework für Systemkomponenten garantiert. Verwendung domänenspezifischer Sprachen von Galois Inc. CAmkES lässt sich in Architekturanalysetools von Rockwell Collins und der University of Minnesota sowie in hochzuverlässige Softwarekomponenten integrieren.

HACMS-Erfolge basieren auf dem alten treuen Freund eines Software-Ingenieurs - der Modularisierung. Die Neuerung besteht darin, dass formale Methoden die Beobachtbarkeit von Schnittstellen und die Kapselung von Modulinternalen belegen. Diese garantierte Einhaltung der Modularität ermöglicht es Ingenieuren, die keine Experten für formale Methoden sind (wie bei Boeing), neue Systeme zu erstellen oder sogar zu modernisieren und eine hohe Stabilität zu erreichen. Obwohl die Tools noch keinen vollständigen Nachweis der Systemsicherheit liefern.

Formale Überprüfung

Der Nachweis der mathematischen Korrektheit von Programmen reicht mindestens bis in die 1960er Jahre zurück , doch lange Zeit waren ihre tatsächlichen Vorteile für die Softwareentwicklung in Umfang und Tiefe begrenzt. In den letzten Jahren gab es jedoch eine Reihe beeindruckender Durchbrüche bei der formalen Verifizierung auf Codeebene realer Systeme, vom verifizierten C CompCert- Compiler bis zum verifizierten seL4- Mikrokernel (siehe die wissenschaftlichen Artikel dazu), dem von CoCon verifizierten Konferenzsystem, dem verifizierten CakeML ML-Compiler und verifizierten Programmen Um die Theoreme von Milawa und Candle zu beweisen, sind das FSCQ- verifizierte ausfallsichere Dateisystem, das verifizierte verteilte IronFleet-System und das verifizierte CertiKOS-Parallelkernel- Framework ebenfalls wichtig mathematische Theoreme, einschließlich der Probleme von vier Farben , des automatischen Beweises der Kepler-Hypothese und des Faith-Thompson-Theorems in ungerader Reihenfolge . All dies sind echte Systeme. Beispielsweise ist CompCert ein kommerzielles Produkt, der seL4-Mikrokernel wird in der Luft- und Raumfahrt sowie in unbemannten Flugzeugen als Plattform für das Internet der Dinge verwendet, und das CoCon-System wurde auf zahlreichen großen wissenschaftlichen Konferenzen verwendet.

Diese Verifizierungsprojekte erfordern einen erheblichen Aufwand. Um formale Methoden öffentlich zugänglich zu machen, müssen diese Anstrengungen reduziert werden. Hier zeigen wir, wie eine strategische Kombination aus formalen und informellen Methoden, eine teilweise Automatisierung formaler Methoden und eine sorgfältige Softwareentwicklung zur Maximierung der Vorteile isolierter Komponenten es uns ermöglicht haben, die Zuverlässigkeit von Systemen, deren Gesamtgröße und Komplexität um Größenordnungen höher sind als die oben genannten, erheblich zu erhöhen.

Bitte beachten Sie, dass wir die formale Überprüfung hauptsächlich für den Code anwenden, von dem die Sicherheit des Systems abhängt. Es gibt aber noch andere Vorteile. Wenn Sie beispielsweise nachweisen, dass der Code korrekt ist, werden Annahmen über den Kontext getroffen, in dem er ausgeführt wird (z. B. Hardwareverhalten und Softwarekonfiguration). Durch die formale Überprüfung werden diese Annahmen explizit, sodass sich Entwickler auf andere Überprüfungswerkzeuge wie das Testen konzentrieren können. Darüber hinaus enthält das System in vielen Fällen sowohl verifizierten als auch nicht verifizierten Code. Während der Codeüberprüfung, des Testens und des Debuggens wirkt die formale Überprüfung wie eine Linse und konzentriert sich auf kritischen, nicht verifizierten Systemcode.

seL4

Beginnen wir mit der Grundlage für den Aufbau nachweislich zuverlässiger Systeme - dem Kernel des Betriebssystems (OS). Dies ist der wichtigste Teil, der die Zuverlässigkeit des gesamten Systems auf kostengünstige Weise garantiert.

Der seL4-Mikrokernel bietet einen formal verifizierten Mindestsatz an Mechanismen zur Implementierung sicherer Systeme. Im Gegensatz zu Standardkerneln ist es zweckmäßig universell und daher zur Implementierung einer Reihe von Sicherheitsrichtlinien und Systemanforderungen geeignet.

Eines der Hauptziele bei der Entwicklung von seL4 ist die Bereitstellung einer starken Isolation zwischen gegenseitig misstrauischen Komponenten, die auf dem Kernel ausgeführt werden. Es unterstützt seine Arbeit als Hypervisor beispielsweise für ganze Linux-Betriebssysteme und hält sie gleichzeitig von sicherheitskritischen Komponenten isoliert, die zusammenarbeiten können (siehe Abbildung 1). Mit dieser Funktion können Systementwickler insbesondere ältere Komponenten mit versteckten Komponenten verwenden Schwachstellen neben hochzuverlässigen Komponenten.


Abb. 1. Isolation und kontrollierte Kommunikation in seL4

Der seL4-Kern nimmt unter Allzweck-Mikrokernen eine Sonderstellung ein. Es bietet nicht nur eine bessere Leistung in seiner Klasse , seine 10.000 Zeilen C-Code wurden einer strengeren formalen Überprüfung unterzogen als jede andere öffentlich verfügbare Software in der Geschichte der Menschheit, nicht nur hinsichtlich der Beweislinien, sondern auch hinsichtlich der Stärke der nachgewiesenen Eigenschaften. Es basiert auf dem Nachweis der „funktionalen Korrektheit“ der Kernimplementierung in C. Es stellt sicher, dass jedes Verhalten des Kernels durch seine formale abstrakte Spezifikation vorhergesagt wird: In der Online-Bewerbung finden Sie eine Vorstellung davon, wie diese Beweise aussehen. Nach dieser Garantie haben wir zusätzliche Beweise hinzugefügt, die wir nach Einführung in die grundlegenden Mechanismen des Kerns erklären werden.

seL4 API

Der seL4-Kernel bietet nur minimale Mechanismen zur Implementierung sicherer Systeme: Streams, Fähigkeitsmanagement, virtuelle Adressräume, Interprozesskommunikation (IPC), Signalisierung und Interrupt-Zustellung.

Der Kernel behält seinen Status in den "Kernelobjekten". Beispielsweise gibt es für jeden Thread im System ein „Flow-Objekt“, in dem Informationen zu Sheding, Ausführung und Zugriffskontrolle gespeichert sind. User-Space-Programme können nur indirekt über sogenannte "Fähigkeiten" oder "Fähigkeiten" auf Kernel-Objekte verweisen, die eine Verknüpfung zu einem Objekt mit einer Reihe von Zugriffsrechten darauf kombinieren. Beispielsweise kann ein Thread keinen anderen Thread starten oder stoppen, wenn er nicht über die "Fähigkeit" für das entsprechende Thread-Objekt verfügt.

Threads interagieren und synchronisieren sich, indem sie Nachrichten über „Endpunkte“ der Interprozesskommunikation senden. Ein Thread mit der Fähigkeit zum Senden an den entsprechenden Endpunkt kann eine Nachricht an einen anderen Thread senden, der die Fähigkeit zum Empfangen an diesen Endpunkt hat. Benachrichtigungsobjekte bieten eine Synchronisation über Sätze von binären Semaphoren hinweg. Die Übersetzung virtueller Adressen wird von Kernelobjekten gesteuert, die Seitenverzeichnisse, Seitentabellen und Rahmenobjekte oder subtile Abstraktionen über die entsprechenden Prozessorarchitekturobjekte darstellen. Jeder Stream verfügt über eine bestimmte VSpace-Fähigkeit, die auf die Wurzel des Baums der Stream-Adressübersetzungsobjekte verweist. Die Funktionen selbst werden vom Kernel verwaltet und in den Kernelobjekten „CNodes“ in der Struktur des Diagramms gespeichert, die Links zu Objekten mit Zugriffsrechten zuordnen, ähnlich wie beim Vergleich virtueller Seitentabellen mit physischen Adressen im Speicher. Jeder Thread hat seine eigene Fähigkeit, den Root-CNode zu identifizieren. Die Funktionen, die in diesem Stammverzeichnis verfügbar sind, werden als "CSpace Stream" bezeichnet. Fähigkeiten können über Endpunkte mit Jobübertragung übertragen und mithilfe eines gemeinsamen CSpace als gemeinsam genutzt deklariert werden. Abbildung 2 zeigt diese Kernelobjekte.


Abb. 2. Kernelobjekte in einem seL4-System mit zwei Threads, die über einen Endpunkt interagieren

Sicherheitsnachweise

Aufgrund ihrer Vielseitigkeit sind die seL4-Kernel-APIs auf niedriger Ebene und unterstützen hochdynamische Systemarchitekturen. Daher ist es schwierig, direkte Beweise für diese APIs zu erhalten.

Das übergeordnete Konzept der Zugriffssteuerungsrichtlinien abstrahiert von einzelnen Objekten und Kernelfunktionen und erfasst stattdessen die Zugriffssteuerungskonfiguration des Systems mithilfe einer Reihe abstrakter „Subjekte“ (Komponenten) und der Befugnisse, die jeder von ihnen gegenüber anderen hat (z. B. zum Lesen von Daten und zum Senden von Nachrichten). . Im Beispiel in Abb. In 2 erhielten die Komponenten A und B die Autorität über den Endpunkt.

Sewell und Kollegen haben bewiesen, dass die seL4-Zugriffssteuerungsrichtlinien sicherstellen, dass zwei grundlegende Sicherheitsfunktionen eingehalten werden: Einschränkung von Berechtigungen und Integrität.

Die Einschränkung der Berechtigung bedeutet, dass die Zugriffssteuerungsrichtlinie eine statische (unveränderte) sichere Annäherung an bestimmte Funktionen und Kernelobjekte im System für jeden zukünftigen Status ist. Diese Eigenschaft impliziert, dass unabhängig von der Entwicklung des Systems keine Komponente jemals mehr Autorität erhalten wird, als die Zugriffssteuerungsrichtlinie vorhersagt. In Abbildung 2 hat die Richtlinie für Komponente B keinen Schreibzugriff auf Komponente A. Daher kann Komponente B diesen Zugriff in Zukunft nie mehr erhalten. Diese Eigenschaft impliziert, dass das Denken auf Richtlinienebene eine sichere Annäherung an das Denken über den spezifischen Status der Zugriffskontrolle im System darstellt.

Integrität bedeutet, dass die Komponente unabhängig von ihrer Tätigkeit niemals Daten im System ändern kann (einschließlich aller Systemaufrufe, die sie ausführen kann), sodass die Zugriffssteuerungsrichtlinie eindeutig nicht geändert werden darf. Zum Beispiel in Abb. 2 ist die einzige Komponente der Autorität von A über eine andere Komponente das Recht, Daten an den Endpunkt zu senden, von dem Komponente B Informationen empfängt. Dies bedeutet, dass Komponente A nur ihren Status, den Status von Thread B und den Status des Nachrichtenpuffers ändern kann. Es kann keine anderen Teile des Systems ändern.

Ein Nebeneffekt der Integrität ist die Vertraulichkeit, wenn eine Komponente nicht in der Lage ist, Informationen von einer anderen Komponente ohne Erlaubnis zu lesen : Dies ist eine nachgewiesene starke Eigenschaft der nicht-transitiven Nicht-Interferenz von seL4. Das heißt, in einem ordnungsgemäß konfigurierten System (mit strengeren Einschränkungen als nur aus Gründen der Integrität) kann keine der Komponenten ohne Erlaubnis Informationen über eine andere Komponente oder deren Ausführung herausfinden. Der Proof drückt diese Eigenschaft in Form der Informationsflussrichtlinie aus, die aus der Zugriffssteuerungsrichtlinie extrahiert werden kann, die für den Integritätsnachweis verwendet wird. Informationen werden nur übertragen, wenn dies ausdrücklich durch die Richtlinie gestattet ist. Der Proof deckt explizite Informationsflüsse sowie potenzielle versteckte Speicherkanäle im Kernel ab. Die Synchronisationskanäle befinden sich jedoch außerhalb ihres Bereichs und müssen auf andere Weise verarbeitet werden .

Ein weiterer Beweis in seL4 ist eine Erweiterung der Funktionskorrektheit und damit der Sicherheitssätze auf eine binäre Ebene für die ARMv7-Architektur und ein Worst-Case-Laufzeitprofil für den Kernel ( 1 , 2 ), das für Echtzeitsysteme erforderlich ist. Der seL4-Kern ist für verschiedene Architekturen verfügbar: ARMv6, ARMv7, ARMv7a, ARMv8, RISC-V, Intel x86 und Intel x64. Derzeit wurden Maschinentests für die ARMv7-Architektur für den gesamten Verifizierungsstapel sowie für ARMv7a mit Hypervisor-Erweiterungen für die Funktionskorrektheit bestanden.

Architektur-Sicherheit

Im vorherigen Abschnitt wurden die Programmiermethoden beschrieben, mit denen der seL4-Kernel eine solide Grundlage für nachweislich zuverlässige Systeme schafft. Der Kernel bildet eine zuverlässige Computerbasis (TCB) - eine wesentliche Komponente der Software, die für eine garantierte Systemsicherheit ordnungsgemäß funktionieren muss. In realen Systemen ist diese Basis viel breiter als nur ein Mikrokernel. Es ist erforderlich, einen zusätzlichen Software-Stack zu überprüfen, um das gleiche Maß an Sicherheit wie für den Kernel zu erhalten. Es gibt jedoch Klassen von Systemen, für die eine solche Überprüfung nicht erforderlich ist: Sie benötigen Isolationssätze auf Kernelebene, um bestimmte Sicherheitseigenschaften auf Systemebene abzuleiten. Dieser Abschnitt enthält ein Beispiel für ein solches System.

Dies sind Systeme, in denen Komponentenarchitekturen bereits eine kritische Eigenschaft implementiert haben, möglicherweise zusammen mit mehreren kleinen vertrauenswürdigen Komponenten. Unser Beispiel ist die Quadcopter-Flugsteuerungssoftware, ein Demogerät im zuvor erwähnten HACMS-Programm.

Abbildung 3 zeigt die wichtigsten Hardwarekomponenten des Quadrocopters. Die Architektur ist absichtlich komplexer als die vom Quadcopter geforderte, da sie ULB darstellen sollte und auf dieser Abstraktionsebene der Architektur von ULB ähnelt.


Abb. 3. Architektur eines autonomen Flugzeugs

Die Abbildung zeigt zwei Hauptcomputer: einen Bordcomputer, der mit der Bodenstation kommuniziert und die an Bord befindliche Software (z. B. die Kamera) steuert, und einen Navigationscomputer, der den Flug des Fahrzeugs steuert, Sensordaten liest und Triebwerke steuert. Computer sind über ein internes Netzwerk oder einen CAN-Bus an einem Quadrocopter und Ethernet an der ULB verbunden. Der Quadrocopter verfügt außerdem über einen ungeschützten WLAN-Punkt, mit dem zusätzliche Schutzmethoden demonstriert werden können.

Stellen Sie sich in diesem Beispiel einen Bordcomputer vor. Dafür müssen vier grundlegende Eigenschaften erfüllt sein:

• ordnungsgemäße Authentifizierung von Befehlen von der Bodenstation;
  
• Datenschutz von kryptografischen Schlüsseln;
  
• keine zusätzlichen Nachrichten für den Navigationscomputer;
  
• Unzuverlässige Software von anderen Bordsystemen kann den Flug des Geräts nicht beeinträchtigen.

Die Arbeitshypothese lautet, dass die Kamera unzuverlässig, potenziell kompromittiert oder böswillig ist, dass ihre Treiber und veraltete Software potenziell kompromittiert sind sowie externe Kommunikationskanäle. In diesem Beispiel gehen wir von einer korrekten und starken Kryptographie aus, dh, der Schlüssel kann nicht abgeholt werden, und wir gehen über den Rahmen der Aufgabe hinaus, die Funkkommunikation des Feindes mit einer Bodenstation zu unterdrücken.

Abbildung 4 zeigt, wie die Quadrocopter-Architektur diese Eigenschaften bietet. Die virtuelle Linux-Maschine (VM) dient als Container für ältere integrierte Gerätesoftware, Kameratreiber und WLAN-Hotspots. Wir isolieren das Kryptografiesteuerungsmodul in einer eigenen Komponente mit Verbindungen zum CAN-Bus, zum Bodenstationskanal und zur virtuellen Linux-Maschine, um Daten an die Bodenstation zu senden. Die Aufgabe der kryptografischen Komponente besteht darin, (nur) autorisierte Nachrichten über die CAN-Schnittstelle des Stapels an den Bordcomputer zu senden und Diagnosedaten an die Bodenstation zurückzusenden. Die Funkkomponente sendet und empfängt Rohnachrichten, die von der kryptografischen Komponente verschlüsselt und (mit Authentifizierung) entschlüsselt werden.


Abb. 4. Vereinfachte Quadcopter-Bordcomputerarchitektur

Das Festlegen der gewünschten Eigenschaften des Systems reduziert sich ausschließlich auf die Eigenschaften der Isolation und das Verhalten der Architektur im Hinblick auf den Informationsfluss sowie auf das Verhalten einer einzelnen vertrauenswürdigen kryptografischen Komponente. Unter der Annahme des korrekten Verhaltens dieser Komponente können die Schlüssel nicht gefährdet werden, da keine andere Komponente Zugriff auf sie hat. Der Kanal zwischen Linux und der kryptografischen Komponente in Abb. 4 ist nur für Nachrichten gedacht und gewährt keinen Zugriff auf den Speicher. Nur autorisierte Nachrichten können in den CAN-Bus gelangen, da die kryptografische Komponente die einzige Kommunikation mit dem Bus ist. Unzuverlässige Software und WLAN sind als Teil der virtuellen Linux-Maschine durch Komponentenisolation gekapselt und können nur über eine vertrauenswürdige kryptografische Komponente mit dem Rest des Systems interagieren.

Es ist leicht vorstellbar, dass eine solche Analyse der Architektur weitgehend automatisiert werden kann, indem Modelle und Werkzeuge des mechanischen Denkens auf einer höheren Ebene überprüft werden. Wie für MILS-Systeme erwähnt , sind die Grenzen von Komponenten in einer solchen Architektur nicht nur ein praktisches Werkzeug für die Partitionierung und das Code-Management, sondern bieten bei erzwungener Isolation effektive Grenzen für formale Überlegungen zum Verhalten des Systems. Es hängt jedoch alles von der richtigen Anwendung der Komponentengrenzen zur Laufzeit in der endgültigen Implementierung des Binärsystems ab.

Die zuvor diskutierten Mechanismen des seL4-Kernels sind in der Lage, eine solche Implementierung bereitzustellen, aber der Abstraktionsgrad der Mechanismen steht in starkem Kontrast zu den Blöcken und Pfeilen des Architekturschemas: Eine noch abstraktere Zugriffssteuerungsrichtlinie enthält noch viel mehr Details als das Architekturschema. In einem realen System dieser Größe werden Zehntausende von Kernelobjekten und „Fähigkeiten“ von der Software erstellt, und Konfigurationsfehler können zu Sicherheitsverletzungen führen. Anschließend diskutieren wir, wie wir nicht nur die Konfiguration und Erstellung eines solchen Codes automatisieren, sondern auch automatisch die Einhaltung der Grenzen der Architektur nachweisen können.

Überprüfung der Komponentenansicht

Da Sicherheitsnachweise durch formale Abstraktionen von Sicherheitsrichtlinien vereinfacht werden, hilft die Abstraktion auch beim Systemdesign. Die Komponenten- Camkes- Plattform läuft auf seL4-Abstraktionen über den Kernelmechanismen auf niedriger Ebene, stellt Kommunikationsprimitive bereit und zerlegt das System in funktionale Einheiten, wie in Abb. 1 dargestellt. 5. Mithilfe dieser Plattform können Systemarchitekten Systeme auf der Basis von seL4 in Bezug auf übergeordnete Komponenten entwerfen und erstellen, die über Konnektoren wie Remote Procedure Calls (RPC), Datenports und Ereignisse miteinander und mit Hardwaregeräten interagieren.


Abb. 5. CAmkES-Workflow

Codegenerierung

Intern implementiert CAmkES diese Abstraktionen mithilfe von Kernelobjekten auf niedriger Ebene in seL4. Jede Komponente enthält (mindestens) einen Stream, CSpace und VSpace. RPC-Konnektoren verwenden Endpunktobjekte, und CAmkES generiert Zwischencode, um Nachrichten zu verarbeiten und an IPC-Endpunkte zu senden. In ähnlicher Weise wird der Datenport-Konnektor über einen gemeinsam genutzten Speicher implementiert - gemeinsame Rahmen, die in den Adressräumen zweier Komponenten vorhanden sind - und kann optional die Richtung der Datenübertragung begrenzen. Schließlich wird der Ereignis-Connector mithilfe des seL4-Benachrichtigungsmechanismus implementiert.

CAmkES generiert in capDL auch eine Low-Level-Spezifikation der Erstkonfiguration von Objekten und der Funktionen des Kernels des Systems. Diese Spezifikation wird in den seL4-Initialisierer eingegeben, derEs startet zuerst nach dem Laden und führt die erforderlichen seL4-Operationen aus, um eine Instanz zu erstellen und das System zu initialisieren .

Somit generiert die Komponentenplattform Code ohne zusätzlichen Aufwand seitens des Entwicklers. Die Komponentenarchitektur beschreibt eine Reihe von Blöcken und Pfeilen, und die Implementierungsaufgabe besteht darin, einfach die Felder auszufüllen. Die Plattform generiert den Rest und stellt die Implementierung der beschriebenen Architektur bereit.

Auf einer Plattform mit herkömmlichen Komponenten erweitert der generierte Code die vertrauenswürdige Computerbasis des Systems, da er die Funktionalität der Komponenten beeinträchtigen kann. CAmkES generiert jedoch auch Beweise.

Automatische Beweise

Beim Generieren von "Zwischen" -Code erstellt CAmkES formale Beweise in Isabelle / HOL, führt eine Validierung während der Übersetzung durch und zeigt, dass der generierte "Zwischen" -Code einer übergeordneten Spezifikation entspricht und die generierte capDL-Spezifikation eine korrekte Verfeinerung der CAmkES-Beschreibung ist . Wir haben auch bewiesen, dass der seL4-Initialisierer das System in der erforderlichen Erstkonfiguration korrekt konfiguriert. Gleichzeitig automatisieren wir den größten Teil des Systemaufbaus, ohne die vertrauenswürdige Computerbasis zu erweitern.

Entwickler befassen sich selten mit der Ausgabe von Codegeneratoren, sie interessieren sich nur für Funktionalität und Geschäftslogik. Wir gehen auch davon aus, dass Beweise für Zwischencode nicht überprüft werden müssen, dh Entwickler können sich darauf konzentrieren, die Richtigkeit ihres eigenen Codes zu beweisen. So wie der generierte CAmkES-Header dem Entwickler eine API für den generierten Code gibt, erstellen die Lemma-Operatoren der obersten Ebene eine API zum Beweis. Lemmas beschreiben das erwartete Verhalten von Steckverbindern. Im RPC-Middleware-Beispiel in Abbildung 6 generierte Funktion$$ bietet eine Möglichkeit, eine Remote-Funktion aufzurufen$f$$$ in einer anderen Komponente. Rufen Sie auf, um die Abstraktion zu speichern$g$$$ sollte gleichbedeutend mit aufrufen sein$f$$$$g$ . Das vom System erzeugte Lemma stellt dies sicher $$aus dem generierten RPC-Code verhält sich wie ein direkter Aufruf$f$$$$g$ .


Abb. 6. Generierter RPC-Code

Für die tatsächliche Verwendung von vom System generierten Beweisen müssen sie mit (fast) willkürlichen Beweisen, die der Benutzer für eine Funktion bereitstellt, zusammengesetzt werden können$$ und für Kontexte, in denen$g$$$$g$ und $$$f$.Um diese Zusammensetzbarkeit zu erreichen, wird die Steckerspezifikation durch vom Benutzer bereitgestellte Spezifikationen für Remote-Funktionen parametrisiert. Auf diese Weise können Ingenieure über ihre Architektur nachdenken, indem sie Spezifikationen und Nachweise für ihre Komponenten bereitstellen und sich auf Spezifikationen für den generierten Code verlassen.

Bisher haben wir diesen Prozess von Anfang bis Ende mit dem speziellen CAmkES RPC-Anschluss ( 1 , 2 ) demonstriert . Da Vorlagen für andere Konnektoren (Datenports und Ereignisse) viel einfacher als RPCs sind, ist es nicht schwierig, den Beweisgenerator zu erweitern, um diese Konnektoren zu unterstützen, sodass Sie vielfältigere verifizierte Systeme erstellen können.

Nach dem Kommunikationscode erstellt CAmkES die anfängliche Zugriffssteuerungskonfiguration, um die Grenzen der Architektur anzuwenden. Um zu beweisen, dass diese beiden Systembeschreibungen - capDL und CAmkES - miteinander übereinstimmen, betrachten Sie die CAmkES-Beschreibung als Abstraktion für die capDL-Beschreibung. Wir verwenden das zuvor getestete Framework , um die Autorität eines Objekts gegenüber einem anderen Objekt aus der capDL-Beschreibung abzuleiten. Wir werden also die Beweise auf die Ebene der Politik bringen. Darüber hinaus haben wir in der CAmkES-Beschreibung Regeln für den Entzug der Berechtigung zwischen Komponenten definiert. Dieser Beweis stellt sicher, dass capDL-Objekte, die als Berechtigungsdiagramm mit nach Komponenten gruppierten Objekten dargestellt werden, dieselben Grenzen zwischen Gruppen aufweisen wie im entsprechenden CAmkES-Komponentendiagramm. Intuitiv bedeutet diese Entsprechung von Grenzen, dass die Analyse der Richtlinienarchitektur aus der CAmkES-Beschreibung die Richtlinie aus der von capDL generierten Beschreibung speichert, die wiederum garantiert die Anforderungen der Einschränkung der Autorität, Integrität und Vertraulichkeit erfüllt, wie bereits erwähnt.

Um die korrekte Initialisierung zu beweisen, verwendet CAmkES einen universellen Initialisierer, der als erste Benutzeraufgabe nach dem Laden startet. In seL4 hat diese erste (und eindeutige) Benutzeraufgabe Zugriff auf den gesamten verfügbaren Speicher, um Objekte und „Fähigkeiten“ gemäß der detaillierten Beschreibung von capDL zu erstellen, die sie als Eingabe akzeptiert. Es ist bewiesen, dassZustand nach Ausführung des Initialisierers erfüllt den in der angegebenen Spezifikation beschriebenen Zustand . Dieser Beweis gilt für das genaue Initialisierungsmodell, jedoch noch nicht auf Implementierungsebene. Im Vergleich zur Tiefe der restlichen Evidenzkette mag diese Einschränkung schwach erscheinen, es handelt sich jedoch bereits um formellere Evidenz, als dies auf der höchsten Ebene (EAL7) der allgemeinen Sicherheitsbewertungskriterien erforderlich ist.

Seismic Security Upgrade

In der Praxis ist es aus Sicherheitsgründen schwierig, die Entwicklung eines Systems von Grund auf sicherzustellen. Daher ist die Möglichkeit, alte Software zu aktualisieren, für die Entwicklung sicherer Systeme von entscheidender Bedeutung. Unser seL4-basiertes Framework unterstützt einen iterativen Prozess, den wir als "seismische Sicherheitsupgrades" bezeichnen, da ein regulärer Architekt vorhandene Gebäude für eine größere seismische Stabilität upgraden wird. Wir veranschaulichen den Prozess am Beispiel einer schrittweisen Anpassung der vorhandenen Softwarearchitektur eines unbemannten Hubschraubers, wobei wir vom traditionellen Testschema zu einem hochzuverlässigen System mit Theoremen übergehen, die durch formale Methoden unterstützt werden. Obwohl dieses Beispiel auf einem echten ULB-Projekt basiert, wird es hier vereinfacht und enthält nicht alle Details.

Die ursprüngliche Architektur des Hubschraubers stimmt mit der in Abb. 3. Seine Funktionalität wird von zwei separaten Computern bereitgestellt: Der Navigationscomputer steuert den tatsächlichen Flug, und der Bordcomputer führt Aufgaben auf hoher Ebene aus (z. B. Kommunikation mit einer Bodenstation und Navigation des Bildes von der Kamera aus). Die ursprüngliche Version des Bordcomputers war eine monolithische Anwendung für Linux. Während des Modernisierungsprozesses verwendeten die Boeing-Ingenieure die von HACMS-Partnern bereitgestellten Methoden, Werkzeuge und Komponenten.

Schritt 1. Virtualisierung

Der erste Schritt bestand darin, das System so zu nehmen, wie es ist, und es in einer virtuellen Maschine auf einem sicheren Hypervisor auszuführen (siehe Abbildung 7). In der Metapher der seismischen Modernisierung entspricht dies einer mobilen Aufstellung des Systems. Eine virtuelle Maschine über seL4 in diesem System besteht aus einer CAmkES-Komponente, zu der ein Virtual Machine Monitor (VMM) und ein Gastbetriebssystem gehören, in diesem Fall Linux. Der Kernel stellt Virtualisierungshardware-Abstraktionen bereit, und VMM verwaltet diese Abstraktionen für die virtuelle Maschine. Der seL4-Kernel beschränkt nicht nur das Gastbetriebssystem, sondern auch VMM, sodass Sie der VMM-Implementierung nicht vertrauen müssen, um eine erzwungene Isolation bereitzustellen. Ein VMM-Fehler führt zu einem Ausfall des Gastbetriebssystems, jedoch nicht zu einem Ausfall des gesamten Systems.


Abb. 7. Alle Funktionen in einer virtuellen Maschine

Abhängig von der Systemkonfiguration kann die virtuelle Maschine über paravirtualisierte Treiber, Pass-Through-Treiber oder beides auf Geräte zugreifen. Bei Pass-Through-Treibern können Entwickler die System-MMU oder -IOMMU verwenden, um eine Verletzung der Isolationsgrenzen durch Hardwaregeräte und Treiber im Gastsystem zu verhindern. Beachten Sie, dass das einfache Starten des Systems in einer virtuellen Maschine keine zusätzlichen Sicherheits- oder Zuverlässigkeitsvorteile bietet. Schritt 1 wird nur benötigt, um sich auf Schritt 2 vorzubereiten.

Schritt 2. Mehrere virtuelle Maschinen

Der zweite Schritt der seismischen Modernisierung stärkt bestehende Mauern. In der Software kann ein Entwickler die Sicherheit und Zuverlässigkeit erhöhen, indem er das Quellsystem in mehrere Subsysteme unterteilt, von denen jedes aus einer virtuellen Maschine besteht, auf der nur ein Teil des Quellsystemcodes ausgeführt wird. Jede VM / VMM-Kombination wird in einer separaten CAmkES-Komponente ausgeführt, die die Isolation zwischen verschiedenen Subsystemen einführt, ohne dass diese sich gegenseitig beeinflussen können, und dann die Koexistenz verschiedener Sicherheitsstufen ermöglicht.

Im Allgemeinen folgen die Abschnitte der vorhandenen Softwarearchitektur. Wenn die Architektur für eine effektive Isolierung nicht ausreicht, ist möglicherweise eine Neugestaltung erforderlich.

In der Regel sollten Abschnitte miteinander interagieren, daher werden an dieser Stelle auch Kommunikationskanäle hinzugefügt. Um die Sicherheit zu gewährleisten, müssen diese Schnittstellen unbedingt eng sein, sodass die Verbindung zwischen Partitionen nur auf das absolut Notwendige beschränkt ist. Darüber hinaus müssen Schnittstellenprotokolle mit einer Mindestanzahl von Nachrichten oder Datenvolumen effizient sein. Es ist wichtig, dass Sie mit seL4 den Speicheraustausch zwischen Partitionen steuern und begrenzen können, um die Datenmenge zu minimieren.

Zusätzlich zu den virtuellen Maschinen, die die Subsysteme des Quellsystems darstellen, extrahieren und implementieren wir auch Komponenten für alle gemeinsam genutzten Ressourcen (z. B. eine Netzwerkschnittstelle).

Sie können Schritt 2 wiederholen, bis wir das gewünschte Detail der Abschnitte erreicht haben. Die korrekte Detaillierung ist ein Kompromiss zwischen der Isolationsfestigkeit einerseits und dem erhöhten Kommunikationsaufwand und den Rekonstruktionskosten andererseits.

In unserem Beispiel haben wir drei Abschnitte: eine virtuelle Maschine, die die Kommunikationsfunktionen einer Bodenstation unter Linux implementiert; eine andere virtuelle Maschine, die kamerabasierte Navigationsfunktionen implementiert (auch unter Linux); und eine native Netzwerkfreigabekomponente, wie in Abb. 8.


Abb. 8. Funktionalität in mehrere virtuelle Maschinen unterteilt

Schritt 3. Native Komponenten

Wenn ein System in separate Abschnitte einer virtuellen Maschine zerlegt wird, können einige oder alle einzelnen Abschnitte als native Komponenten und nicht als virtuelle Maschinen erneut implementiert werden. Dadurch wird die Angriffsfläche bei gleicher Funktionalität erheblich reduziert. Ein zusätzlicher Vorteil der Konvertierung einer Komponente in Maschinencode besteht darin, die Last zu reduzieren und die Produktivität zu steigern, das Gastbetriebssystem zu entfernen und den Aufwand für die Codeausführung und die VMM-Kommunikation zu verringern.

Native Komponenten erhöhen auch das Potenzial für die Anwendung formaler Verifizierungen und anderer Methoden, um die Zuverlässigkeit einer Komponente zu erhöhen. Die Optionen sind unterschiedlich: von der vollständigen Funktionsüberprüfung des nativen Codes bis zur gemeinsamen Generierung von Code und Beweisen, der Modellüberprüfung, der Verwendung typsicherer Programmiersprachen, der statischen Analyse oder dem traditionellen strengen Testen einer kleineren Codebasis.

Dank der Isolation von seL4 und der Komponentenarchitektur ist es möglich, in einem System von Komponenten mit unterschiedlichen Zuverlässigkeitsstufen zusammenzuarbeiten. In diesem Fall verringern Komponenten mit geringer Zuverlässigkeit nicht die allgemeine Zuverlässigkeit des Systems, und Entwickler profitieren von der Tatsache, dass Sie keine Anstrengungen zur Überprüfung dieses Codes unternehmen müssen.

In unserem Beispiel analysieren wir die virtuelle Maschine für den Kommunikationskanal zwischen dem Bordcomputer und der Bodenstation in native Module. In den nativen Komponenten sind die Kommunikations-, Kryptographie- und Kontrollfunktionen (Mission-Manager) implementiert. Wir werden die Kamera und das WLAN in der virtuellen Maschine als unzuverlässige veraltete Komponente belassen (siehe Abb. 9). Diese Trennung ist zu einem Kompromiss zwischen den Bemühungen um die Neugestaltung von Subsystemen und den Vorteilen der Verwendung nativer Komponenten in Bezug auf Leistung und Zuverlässigkeit geworden.


Abb. 9. In nativen Komponenten implementierte Funktionalität

Schritt 4. Zuverlässigkeit des Gesamtsystems

Nachdem wir alle erforderlichen Module erhalten haben, machen wir den letzten Schritt: Analyse des gesamten Systems auf der Grundlage der Zuverlässigkeit der Architektur und der einzelnen Komponenten.

Im Rahmen von HACMS werden Kommunikation, Kryptographie und ein Steuermodul in der nachweislich typsicheren objektorientierten Sprache Ivory implementiert , wobei eine feste Speichermenge auf dem Heap zugewiesen wird. Ohne zusätzliche Überprüfung gibt uns Ivory keine Garantie für die Funktionsrichtigkeit, sondern Vertrauen in Fehlertoleranz und Notfallzuverlässigkeit. Angesichts der Isolation von Komponenten glauben wir, dass diese Garantien auch bei unzuverlässigen Komponenten (wie der virtuellen Kamera-Maschine) bestehen bleiben.

Die Netzwerkkomponente ist in Standard-C-Code implementiert, der aus Benutzercode für die Plattform und vorhandenem Bibliothekscode besteht. Sein Zuverlässigkeitsgrad entspricht dem Grad, der durch sorgfältige Implementierung bekannten Codes erreicht wird. Die Zuverlässigkeit kann ohne große Kosten verbessert werden, indem Methoden wie die Treibersynthese sowie typsichere Sprachen wie Ivory verwendet werden. Bei einer allgemeinen Analyse der Systemsicherheit wirkt sich ein Kompromiss einer Netzwerkkomponente nur auf Netzwerkpakete aus. Da der Datenverkehr verschlüsselt ist, gefährdet ein solcher Angriff nicht den Zustand der Spezifikationen, dass nur autorisierte Befehle in den Bordcomputer gelangen.

Die virtuelle Maschine des Camcorders ist der schwächste Teil des Systems, da sie auf dem Linux-System ausgeführt wird und Schwachstellen enthalten soll. Die VM ist jedoch isoliert. Wenn Angreifer sie knacken, können sie nicht zu anderen Komponenten wechseln. Das Schlimmste, was ein Angreifer tun kann, ist, die falschen Daten an die Steuerungskomponente zu senden. Wie beim Quadrocopter überprüft diese Komponente die von der Kamera empfangenen Daten. Und er hat den am Anfang des Artikels erwähnten Cyber-Angriff erfolgreich überstanden. Es war ein „White-Box“ -Angriff, bei dem das Pentesters-Team Zugriff auf den gesamten Code und die gesamte Dokumentation sowie auf alle externen Kommunikationskanäle erhielt. Sie erhielt absichtlich Root-Zugriff auf die virtuelle Maschine der Kamera, um einen erfolgreichen Angriff auf veraltete Software zu simulieren. Die Eindämmung des Angriffs und die Fähigkeit, sich gegen dieses sehr mächtige Szenario zu verteidigen, wurden zu einem würdigen Test unserer Sicherheitsanforderungen und zur Identifizierung fehlender Annahmen, Schnittstellenprobleme oder anderer Sicherheitsprobleme, die das Forschungsteam möglicherweise nicht erkennt.

Einschränkungen und zukünftige Arbeit

Dieser Artikel bietet einen Überblick über die Methode zum Erreichen eines sehr hohen Sicherheitsniveaus für Systeme, in denen die Sicherheitsfunktion über die Komponentenarchitektur anwendbar ist. Wir haben Theoreme für die Kernelebene und ihre korrekte Konfiguration sowie Theoreme bewiesen, die gewährleisten, dass die Komponentenplattform die Sicherheitsgrenzen gemäß der Beschreibung ihrer Architektur korrekt festlegt und den richtigen Code für Remoteprozeduraufrufe generiert. Die Verbindung mit der Sicherheitsanalyse des Systems auf hoher Ebene bleibt informell, und die Kommunikationscodesätze decken nicht alle von der Plattform bereitgestellten Kommunikationsprimitive ab. Um automatisch einen Satz zu erhalten, der das gesamte System von Anfang bis Ende abdeckt, sind zusätzliche Arbeiten erforderlich. Zum gegenwärtigen Zeitpunkt ist jedoch klar, dass dies eine machbare Aufgabe ist.

Das Hauptziel der vorgestellten Arbeit ist es, den Verifizierungsaufwand für bestimmte Systemklassen drastisch zu reduzieren. Der hier beschriebene rein architektonische Ansatz kann auf andere Systeme als ULB ausgedehnt werden, ist jedoch eindeutig dadurch begrenzt, dass nur Eigenschaften ausgedrückt werden können, die von der Komponentenarchitektur des Systems bestimmt werden. Die Rückgabe verringert sich, wenn sich diese Architektur während der Programmausführung ändert und wenn die Eigenschaften entscheidend vom Verhalten zu vieler vertrauenswürdiger Komponenten oder Komponenten mit zu großer Größe abhängen.

Der erste Schritt zur Lockerung dieser Einschränkungen besteht darin, eine Bibliothek vorab getesteter Komponenten mit einem hohen Maß an Zuverlässigkeit zu erstellen, die als zuverlässige Bausteine ​​in solchen Architekturen verwendet werden können. Diese Bibliothek kann Sicherheitsmuster (wie Desinfektion von Eingabedaten, Ausgabefiltern, Datenschutz- und Laufzeitmonitoren) enthalten, die möglicherweise aus übergeordneten Spezifikationen generiert wurden, sowie Infrastrukturkomponenten wie wiederverwendbare Kryptomodule, Schlüsselspeicher, Dateisysteme, Hochzuverlässige Netzwerkstacks und Treiber. Wenn die Sicherheit von mehr als einer solchen Komponente abhängt, muss die Zuverlässigkeit ihrer Interaktion und gemeinsamen Nutzung gerechtfertigt werden. Die wichtigsten technischen Probleme sind hier Diskussionen über Parallelität und Protokolle sowie den Informationsfluss bei Vorhandensein vertrauenswürdiger Komponenten. Trotz dieser Einschränkungen zeigt die Arbeit die rasche Entwicklung realer hochzuverlässiger Systeme auf Basis von seL4. Derzeit ist die Erstellung solcher Systeme zu geringeren Kosten als bei herkömmlichen Tests möglich.

Anwendung: Arbeitskosten

Die Entwicklung des Designs und des Codes für seL4 dauerte zwei Mannjahre. Wenn wir alle serotypspezifischen Nachweise hinzufügen, werden für 8700 Codezeilen für C insgesamt 18 Personenjahre erhalten. Zum Vergleich: Die Entwicklung eines Mikrokerns L4Ka :: Pistachio vergleichbarer Größe aus der seL4-Familie dauerte sechs Mannjahre und lieferte kein signifikantes Maß an Zuverlässigkeit. Dies bedeutet einen nur 3,3-fachen Unterschied in der Entwicklungsgeschwindigkeit zwischen verifizierter und herkömmlicher Software. Nach der Bewertungsmethode von Colbert und Bohm dauert die Zertifizierung nach traditionellen EAL7-Kriterien für 8700 Zeilen C-Code mehr als 45,9 Personenjahre. Dies bedeutet, dass die formale Überprüfung der Implementierung auf Binärebene bereits 2,3-mal billiger ist als die höchste Zertifizierungsstufe nach allgemeinen Kriterien und gleichzeitig eine deutlich höhere Zuverlässigkeit bietet.

Zum Vergleich verwendet der hier beschriebene HACMS-Ansatz nur vorhandene Beweise für jedes neue System, einschließlich der von den Tools generierten Beweise. Daher beträgt der allgemeine Beweisaufwand für ein System, das diesem Ansatz entspricht, Mannwochen und nicht Jahre, und Tests werden nur durchgeführt, um Annahmen zu validieren.