A platform-evidence mapping for DAL-B certification planning on an AMD64 multi-core processor with Xen temporal isolation

Moderne Flugzeuge werden zunehmend komplexer und verlassen sich auf leistungsstarke Computer, um alles von der Flugsteuerung bis hin zur Navigation und Missionsplanung zu steuern. Um die Sicherheit zu gewährleisten, nutzt die Luftfahrtindustrie strenge Regeln, die vorschreiben, dass jede Software auf ein bestimmtes Vertrauensniveau getestet und verifiziert werden muss. Für die kritischsten Systeme, wie etwa jene, die ein Flugzeug in der Luft halten, ist dieses Vertrauensniveau das höchstmögliche. Doch mit der Entwicklung dieser Computer von Single-Core-Prozessoren hin zu Multi-Core-Chips – ähnlich den leistungsstarken Prozessoren, die in modernen Laptops und Servern zu finden sind – ist eine neue Herausforderung entstanden. Wenn mehrere Programme gleichzeitig auf verschiedenen Kernen desselben Chips laufen, konkurrieren sie oft um den Zugriff auf gemeinsame Ressourcen, insbesondere einen Hochgeschwindigkeits-Speicherbereich, der als Last-Level-Cache bezeichnet wird. Dieser Wettbewerb kann dazu führen, dass ein Programm ein anderes unvorhersehbar verlangsamt, was eine zeitliche Unsicherheit erzeugt, die für sicherheitskritische Luftfahrtsoftware gefährlich ist.

Um dies zu lösen, entwickeln Forscher Wege, um diese Programme zu isolieren, damit sie sich nicht gegenseitig stören. Ein vielversprechender Ansatz ist die Nutzung einer Art Software-Manager, bekannt als Hypervisor, der zwischen der Hardware und den Anwendungen sitzt und die Ressourcen des Computers in separate, sichere Kompartimente unterteilt. Es bleibt jedoch die Frage, ob diese Isolation stark genug ist, um die strengen Standards zu erfüllen, die für die kommerzielle Luftfahrt erforderlich sind. Ein Team von Forschern von Advanced Micro Devices und der Technischen Universität München hat diese Frage untersucht, indem es einen detaillierten Plan erstellt hat, wie eine spezifische Art von Multi-Core-Computer für den Einsatz in Flugzeugen zertifiziert werden kann. Ihre Arbeit konzentriert sich auf eine Konfiguration, die einen Hypervisor namens Xen auf AMD-Prozessoren verwendet, kombiniert mit einer Technik namens Cache-Coloring, um sicherzustellen, dass verschiedene Software-Partitionen sich nicht versehentlich gegenseitig in die Quere kommen.

Die Forscher begannen damit, das spezifische Problem zu identifizieren: Auf einem Multi-Core-Prozessor ist der gemeinsame Speicher-Cache der primäre Ort, an dem Interferenzen auftreten. Wenn ein Programm den Cache füllt, kann es ein anderes Programm zum Warten zwingen, was Verzögerungen verursacht, die dazu führen könnten, dass eine kritische Frist versäumt wird. Um dies zu verhindern, schlug das Team eine Methode vor, bei der der Speicher des Computers basierend auf dem Speicherort der Daten in distinkte Gruppen oder „Farben“ (Colors) unterteilt wird. Jedem Softwareprogramm wird sein eigener, einzigartiger Satz an Farben zugewiesen, und das System wird so konfiguriert, dass die Daten eines Programms niemals die Daten eines anderen im Cache ersetzen können. Entscheidend ist, dass diese Regel auch für den Hypervisor selbst gilt. Die Forscher stellten sicher, dass die eigenen Daten des Software-Managers ebenfalls in seinen eigenen exklusiven Farbsatz gesperrt sind, um zu verhindern, dass er versehentlich die Daten der von ihm verwalteten sicherheitskritischen Programme verdrängt. Dies schafft eine konstruktive Garantie, dass die Interferenz begrenzt ist, was bedeutet, dass sie mathematisch begrenzt und vorhersehbar ist, anstatt darauf zu hoffen, dass sie nicht auftritt.

Die Arbeit präsentiert eine Abbildung dieses technischen Aufbaus auf die offiziellen Zertifizierungsregeln, die von Luftfahrtbehörden in den USA und Europa verwendet werden. Diese Regeln, bekannt als DO-178C und AC 20-193, verlangen von Antragstellern den Nachweis, dass gemeinsam genutzte Ressourcen sicher verwaltet werden. Die Autoren zeigen auf, wie ihre spezifische Konfiguration diese Anforderungen erfüllt, indem sie nachweisen, dass der Cache-Coloring-Mechanismus den Last-Level-Cache effektiv isoliert. Sie zeigen auch, wie der Sicherheitsnachweis des Hypervisers selbst, der durch die Open-Source-Community separat dokumentiert wird, als Beleg für den Flugzeughersteller wiederverwendet werden kann. Dies ermöglicht es dem Hersteller, sich darauf zu konzentieren, den Nachweis zu erbringen, dass seine spezifischen Anwendungen innerhalb dieser isolierten Umgebung korrekt funktionieren, anstatt die Sicherheit der zugrunde liegenden Computerhardware von Grund auf neu beweisen zu müssen. Die Forscher skizzieren einen klaren Weg, wie ein Flugzeughersteller diesen Aufbau nutzen kann, um eine mittlere Sicherheitszertifizierung, bekannt als DAL-B, zu erreichen, die für viele wichtige, aber nicht lebenskritische Funktionen geeignet ist.

Die Autoren definieren jedoch vorsichtig die Grenzen ihrer Arbeit. Sie stellen ausdrücklich klar, dass dieser Plan noch nicht beweist, dass das System sicher genug für die absolut höchste Zertifizierungsstufe ist, die als DAL-A bekannt ist und für die kritischsten Flugsteuerungen erforderlich ist. Um dieses höhere Niveau zu erreichen, wären zusätzliche Schritte erforderlich, wie etwa der mathematische formale Beweis, dass das Speicherzuweisungstool niemals einen Fehler macht, sowie das Sammeln umfangreicherer Praxiserfahrung mit dem spezifischen Prozessor. Das Paper stellt zudem klar, dass es keine KI-Workloads oder Grafikverarbeitung abdeckt, welche Bereiche sind, die aufkommende Technologien darstellen und unterschiedliche Lösungen erfordern würden. Darüber hinaus betonen die Autoren, dass es sich hierbei um ein Methodik-Paper handelt und nicht um eine endgültige Zertifizierung; es liefert ein strukturiertes Argument und ein Set an Werkzeugen, aber die tatsächliche Genehmigung muss dennoch durch die Luftfahrtbehörden erfolgen, die die spezifischen Details jedes einzelnen Flugprogramms prüfen werden.

Der Kern der Forschung ist eine praktische Demonstration dessen, wie diese abstrakten Sicherheitsregeln auf eine reale Computerplattform angewendet werden können. Das Team beschrieb eine spezifische Konfiguration, bei der ein Computer mit vier Kernen in separate Partitionen für verschiedene Aufgaben unterteilt wird, wie etwa Flugsteuerung, Wahrnehmung und Missionsmanagement. Sie zeigten auf, wie jeder Partition ein dedizierter Kern und ein spezifischer Teil des Speicher-Caches zugewiesen werden kann, um sicherzustellen, dass die Flugsteuerungssoftware stets die Ressourcen erhält, die sie benötigt, ohne durch andere Aufgaben verlangsamt zu werden. Sie erläuterten zudem, wie das System bei der Inbetriebnahme auf Fehler prüft, um sicherzustellen, dass die Speicherisolation korrekt funktioniert, bevor das Flugzeug überhaupt abhebt. Dieser Ansatz bietet eine Möglichkeit, leistungsstarke, kommerziell erhältliche Computerchips in der Luftfahrt einzusetzen, ohne die Vorhersehbarkeit und Sicherheit zu opfern, die die Branche fordert.

Letztendlich bietet das Paper eine Brücke zwischen der schnellen Evolution kommerzieller Computerhardware und dem langsamen, bedachten Tempo der Luftfahrt-Sicherheitszertifizierung. Es zeigt, dass es mit der richtigen Konfiguration – speziell durch den Einsatz von Cache-Coloring und einem statisch partitionierenden Hypervisor – möglich ist, eine Computing-Umgebung zu schaffen, in der Interferenzen kontrolliert und vorhersehbar sind. Obwohl der Weg zur höchsten Zertifizierungsstufe noch weitere Arbeit erfordert, bietet diese Forschung eine solide Grundlage, damit Hersteller beginnen können, diese fortschrittlichen Prozessoren in ihre Flugzeuge zu integrieren. Die Arbeit dient als Blaupause und demonstriert, dass die technischen Mechanismen existieren, um eine sichere Multi-Core-Integration zu unterstützen, sofern die spezifischen Regeln und Nachweise, die von den Regulierungsbehörden gefordert werden, sorgfältig befolgt und verifiziert werden.