Formale Verifizierung Warum Tests allein nicht ausreichen: Software-Sicherheit für moderne Fahrzeuge

Anbieter zum Thema

MicroConsult Academy GmbH

emlix GmbH

Moderne Fahrzeugsoftware ist zu komplex für reine Tests. Versteckte Ausführungspfade, Speicherfehler und Multicore-Effekte bleiben oft unentdeckt. Formale Verifizierung wird hier zu einem entscheidenden Faktor.

Die meisten Fehler in Embedded-Software für Fahrzeuge werden nicht durch fehlende Funktionen verursacht. Sie resultieren aus versteckten Ausführungspfaden, die unter bestimmten Laufzeitbedingungen Sicherheits-, Timing- oder Speicherannahmen verletzen. Diese Probleme entstehen oft durch undefiniertes Verhalten, Speicherbeschädigungen oder Multicore-Interferenzen und können monatelang oder sogar jahrelang unentdeckt bleiben, bevor sie im realen Betrieb auftreten.

Die Herausforderung besteht nicht darin, dass diese Fehler unbekannt sind. Vielmehr sind sie für die herkömmliche Verifizierung von Workflows unsichtbar. Unit-Tests, Integrationstests und Hardware-in-the-Loop-Tests können Tausende von Szenarien validieren, ohne jemals die Pfade zu erreichen, die den Fehler auslösen. Statische Analysen tragen zwar zur Reduzierung von Fehlern bei, übersehen jedoch weiterhin die entscheidenden Ausführungspfade.

In moderner Fahrzeugsoftware sind diese versteckten Pfade keine Seltenheit, sondern eine inhärente Folge der Echtzeit-Multicore-Planung. Sie entstehen durch Aufgabenplanung, Interrupts, Cache-Effekte, Speicherverwaltung und komplexe Dateninteraktionen zwischen Dutzenden von Steuergeräten und zentralisierten Fahrzeugrechnerplattformen. Selbst ein einziger Fehler, der unter Milliarden möglicher Ausführungspfade verborgen ist, wird irgendwann auftauchen, sobald die Software in einer Fahrzeugflotte eingesetzt wird.

Deshalb treten auch nach der Validierung noch kritische Fahrzeugausfälle im auf. Leider war der Fehler schon immer vorhanden, er wurde nur nicht getestet.

Speicherfehler sind eine Hauptursache für diese Ausfälle. Probleme wie Pufferüberläufe, Zugriffe außerhalb der Grenzen, Verwendung nach Freigabe und Integer-Überläufe führen oft nicht sofort zum Absturz des Systems. Stattdessen beeinträchtigen sie das Systemverhalten unbemerkt, bis ein späteres Ereignis diese versteckte Beschädigung in einen sichtbaren Fehler verwandelt.

Speicherbeschädigungen sind die Hauptmethode, mit der Angreifer Embedded-Fahrzeugsysteme aus der Ferne kompromittieren. In vernetzten Fahrzeugen werden versteckte Zuverlässigkeitsfehler auch zu versteckten Cybersicherheitslücken, die sich auf ganze Flotten ausbreiten können.

Das Kernproblem ist nicht die Verfügbarkeit von Tools, sondern die Abdeckung. Moderne Fahrzeugsoftware ist zu umfangreich und zu komplex geworden, als dass stichprobenbasierte Tests beweisen könnten, dass kritische Fehler tatsächlich nicht vorhanden sind – egal wie viele Tests durchgeführt werden. Aus diesem Grund reicht eine detektionsbasierte Verifizierung nicht mehr aus, und für ASIL C- und ASIL D-Systeme wird eine mathematisch umfassende Verifizierung erforderlich.

Zunehmende Softwarekomplexität und Risiken in Fahrzeugsystemen

Moderne Fahrzeugarchitekturen haben sich zu eng integrierten, softwaredefinierten Plattformen entwickelt. Zentralisierte Recheneinheiten und Domänencontroller koordinieren nun Bremsen, Lenkung, Antrieb, Wahrnehmung, Energiemanagement und Datenanbindung. Diese Systeme führen Millionen von Softwarezeilen unter strengen Echtzeitbedingungen aus.

Der daraus resultierende Zustandsraum ist enorm und kann durch Tests allein nicht vollständig untersucht werden. Interrupts, Task-Scheduling, Cache-Verhalten, DMA-Übertragungen und Intertask-Kommunikation erzeugen Ausführungspfade, die praktisch unmöglich zu testen sind. Die Wiederverwendung von Software über Lieferanten und Modellgenerationen hinweg verstärkt dieses Risiko. Ein latenter Fehler in einer gemeinsam genutzten Komponente kann sich auf ganze Flotten ausbreiten und jahrelang bestehen bleiben.

Over-the-Air-Updates (OTA), die funkbasierte Übertragung von Software-Updates an Fahrzeuge, beschleunigen Softwareänderungen und verkürzen die Validierungszeiten. Dies erhöht die Abhängigkeit von einer frühzeitigen Verifizierung, um zu verhindern, dass Fehler in den Produktionscode gelangen, da eine späte Entdeckung kostspielig und störend ist.

Warum Tests allein die Sicherheitslücke nicht schließen können

Tests überprüfen das funktionale Verhalten, können jedoch keine Korrektheit garantieren. Sie können zeigen, dass Fehler vorhanden sind, aber niemals beweisen, dass keine Fehler vorhanden sind. Embedded-Software läuft unter nicht deterministischen Bedingungen, die durch Scheduling, Interrupts, asynchrone I/Os und Sensoreingaben beeinflusst werden. Die Anzahl möglicher Laufzeitverhalten übersteigt bei Weitem die Möglichkeiten jeder Teststrategie.

Abdeckungsmetriken bieten nur begrenzte Sicherheit. Probleme wie Race Conditions und Speicherbeschädigungen hängen oft von seltenen Zeitsequenzen und spezifischen Datenmustern ab, die in kontrollierten Testumgebungen möglicherweise nie auftreten. Daher treten versteckte Fehler oft erst während der Integration, im Flottenbetrieb oder unter bestimmten Zeit- und Lastbedingungen zutage, wenn ihre Behebung kostspielig und unsicher wird.

Speichersicherheit als strukturelle Schwachstelle

Verletzungen der Speichersicherheit sind ein ständiges Risiko in der Fahrzeugsoftware. Probleme wie Pufferüberläufe, Zugriffe außerhalb der Grenzen, Use-After-Free-Fehler, Integer-Überläufe und Nullzeiger-Dereferenzierungen können zu undefiniertem Verhalten führen, das die Fehlererkennung beeinträchtigt und das vorhersehbare Systemverhalten gefährdet.

C und C++ dominieren die Fahrzeugentwicklung aufgrund ihrer Leistungsfähigkeit und der Anforderungen an den Hardwarezugriff. Manuelle Speicherverwaltung führt jedoch zu subtilen Fehlern, die lange Zeit unentdeckt bleiben können. Parallele Ausführung verstärkt dieses Risiko zusätzlich, da sie zu Race Conditions führt, die unvorhersehbare und schwer zu diagnostizierende Zustandsbeschädigungen zur Folge haben.

Sprachen wie Rust bieten stärkere Garantien für die Speichersicherheit, beseitigen jedoch nicht alle Risiken in sicherheitskritischen Systemen. Rust-Code interagiert häufig mit Hardware-Registern, RTOS-Kerneln, DMA-Puffern und älteren C/C++-Komponenten und verwendet unsichere Blöcke für leistungskritische Pfade. Diese Bedingungen führen erneut zu Risiken wie Speicherbeschädigungen, Datenkonflikten und Logikfehlern. Rust-Panics fügen einen weiteren Fehlermodus hinzu, der kontrolliert werden muss. Wenn das Panic-Verhalten nicht vollständig analysiert und begrenzt wird, kann es die Fehlerbehandlung umgehen, Timing-Annahmen brechen und Systemausfälle verursachen, die durch Tests nur schwer vorhersehbar sind.

Statische Analyse und das Risiko von False Negatives

Statische Analyse-Tools erkennen viele Fehler frühzeitig, stützen sich jedoch auf Annäherungen, um rechnerisch praktikabel zu bleiben. Dies führt zu False Positives, die eine manuelle Überprüfung erfordern, und zu False Negatives, die echte Fehler übersehen.

Falsch-negative Ergebnisse stellen das größte Sicherheitsrisiko dar. Ein einziges unentdecktes Problem hinsichtlich der Speichersicherheit kann die Fehlerbehandlung beeinträchtigen und zu einer Reihe von Ausfällen in verschiedenen Subsystemen führen. Diese Ausfälle treten häufig während der Integration oder im Flottenbetrieb auf, wenn Korrekturen kostspielig sind und eine erneute Zertifizierung ein großes Risiko für Liefertermine und die Einhaltung von Vorschriften darstellt.

Wirtschaftliche Gründe für die nachweisbasierte Verifizierung

Die Anforderungen an die funktionale Sicherheit werden immer strenger. Die ISO 26262 verlangt zunehmend den Nachweis, dass ganze Klassen von Fehlermodi auf Softwareebene beseitigt und nicht nur durch Redundanz oder Überwachung gemindert werden. Gleichzeitig steigen die Kosten für Validierung und Verifizierung rapide an. Dies ist auf strengere Sicherheitsstandards und die wachsenden wirtschaftlichen Folgen verspäteter Fehlererkennung, Rezertifizierung und flottenweiten Korrekturen zurückzuführen.

Diese Trends deuten gemeinsam auf einen Wandel von detektionsbasierten Arbeitsabläufen hin zu mathematisch strengen Verifizierungsstrategien für sicherheitskritische Automobilsoftware.

Von der Erkennung zum Nachweis

Die formale Verifizierung verwendet mathematische Beweise anstelle von Stichprobenausführung. Techniken wie die abstrakte Interpretation ermöglichen eine umfassende Analyse aller möglichen Ausführungspfade und Eingaben innerhalb definierter Grenzen.

Für Fahrzeugsysteme bedeutet dies, dass das Nichtvorhandensein ganzer Fehlerklassen, wie Verstöße gegen die Speichersicherheit und undefiniertes Verhalten, nachgewiesen werden muss. Dadurch werden falsch-negative Ergebnisse eliminiert und falsch-positive Ergebnisse reduziert. Entwickler können bestätigen, ob lebensbedrohliche Fehlermodi in Brems-, Lenk-, Power-Management- und Wahrnehmungssystemen überhaupt auftreten können, anstatt sich auf wahrscheinliche Testergebnisse zu verlassen.

Auswirkungen auf Entwicklung, Sicherheit und Cybersicherheit

Eine umfassende Verifizierung verbessert die Produktivität, indem sie Fehlalarme reduziert und eine frühzeitigere Fehlerbehebung ermöglicht. Sie reduziert Nacharbeiten, Integrationsverzögerungen und Kosten für die Neuzertifizierung. Bei großen, bestehenden Codebasen und Komponenten von Drittanbietern bietet der mathematische Nachweis eine objektive Sicherheit ohne umfangreiches Überarbeiten.

Die formale Verifizierung stärkt die funktionale Sicherheit, indem sie nachweist, dass gefährliche Verhaltensweisen während der Laufzeit nicht auftreten können. In Systemen, in denen Softwarefehler direkt zum Verlust der Brems-, Lenk- oder Antriebskontrolle führen können, ist dies von entscheidender Bedeutung. Aus Sicht der Cybersicherheit verringert das Beseitigen von Speichersicherheitsmängeln eine große Angriffsfläche und verbessert so die Fahrzeugsicherheit.

Leitfaden für Software-Testmanager

Normgerechtes Software-Testmanagement in Automotive-Projekten

Fazit

Verletzungen der Speichersicherheit stellen ein ständiges Risiko in Fahrzeugsoftware dar. Probleme wie Pufferüberläufe, Zugriffe außerhalb der Grenzen, Use-After-Free-Fehler, Integer-Überläufe und Nullzeiger-Dereferenzierungen können zu undefiniertem Verhalten führen, das die Fehlererkennung beeinträchtigt und das vorhersehbare Systemverhalten gefährdet.

Eine mathematisch vollständige Verifizierung bietet einen Weg von der Erkennung zum Nachweis. Da Software zunehmend die Kernfunktionen von Fahrzeugen steuert, ist der Übergang von getesteter zu mathematisch verifizierter Software eine notwendige Weiterentwicklung im Fahrzeugbau.

 (sg)

(ID:50714905)