Formale Analyse von Automotive-Protokollen Wie ein mathematischer Beweis Schwachstellen identifiziert, die kein Test findet

Je mehr Schnittstellen im vernetzten Fahrzeug, desto größer die potenzielle Angriffsfläche. Ob Diagnose, Ladevorgänge oder Over-the-Air-Updates: Unsichere Kommunikation kann zur Gefahr für Daten und sicherheitskritische Fahrzeugfunktionen werden. Abhilfe kann die formale Sicherheitsanalyse bieten, die in der Kryptografie längst Standard ist. Dieser Artikel zeigt anhand konkreter Befunde, warum sie auch in der Automobilbranche sinnvoll wäre.

Moderne Fahrzeuge sind rollende Rechnernetze. Dutzende Steuergeräte tauschen über CAN, Automotive Ethernet und IP-basierte Protokolle Daten aus, kommunizieren mit Ladesäulen, Werkstatt-Testern und Backend-Systemen und öffnen sich über Vehicle-to-Everything und Over-the-Air-Updates zunehmend nach außen. Mit jeder neuen Schnittstelle wächst die Angriffsfläche, und mit ihr das Risiko, dass eine unsichere Kommunikation zum Einfallstor wird. Bei Funktionen wie Diagnose, Software-Updates oder Ladevorgängen können Sicherheitslücken nicht nur Daten, sondern im Extremfall sicherheitskritische Fahrzeugfunktionen betreffen.

Die naheliegende Antwort lautet: sichere Protokolle einsetzen. Doch der Entwurf sicherer Protokolle ist selbst für Experten schwierig und selbst dann, wenn das Ergebnis als internationaler Standard veröffentlicht wird, sind Designfehler möglich. Genau hier setzt die formale Sicherheitsanalyse an. Sie ist in der Forschung im Bereich Kryptografie fest etabliert, in der Automobilbranche aber noch wenig verbreitet.

Tests finden, was man sucht – Beweise zeigen, was man übersieht

Klassische Qualitätssicherung für Protokolle stützt sich auf Code-Reviews, Penetrationstests und Fuzzing. Diese Verfahren sind wertvoll und unverzichtbar, haben aber eine grundsätzliche Grenze: Sie können die Anwesenheit von Fehlern nachweisen, niemals deren Abwesenheit. Ein Penetrationstest, der keine Schwachstelle findet, beweist nur, dass der Tester keine gefunden hat. Gerade bei kryptografischen Protokollen sind die kritischen Angriffe oft solche, an die beim Entwurf schlicht niemand gedacht hat. Sie entstehen nicht aus einem Implementierungsfehler in einer Codezeile, sondern aus dem logischen Zusammenspiel mehrerer Nachrichten. Sie liegen bereits im Standard selbst, lange bevor die erste Zeile Code geschrieben ist.

Die formale Sicherheitsanalyse dreht die Logik um. Statt einzelne Angriffe auszuprobieren, beschreibt man das Protokoll und die gewünschten Sicherheitseigenschaften mathematisch präzise und überlässt einem Verifikations-Tool die Frage, ob ein Angreifer diese Eigenschaften unter irgendeiner denkbaren Vorgehensweise verletzen kann. Findet das Verifikationstool keinen Weg, ist das ein Beweis: Unter den modellierten Annahmen ist das Protokoll sicher. Findet es einen Weg, liefert es gleich ein konkretes Angriffsszenario mit.

Was „formal“ konkret bedeutet

Formale Analyse wird meist entweder im Symbolic oder im Computational Model durchgeführt. Letzteres wird hauptsächlich für den mathematischen Sicherheitsbeweis der kryptographischen Algorithmen genutzt. Für die Analyse von Protokollen hat sich das Symbolic Modell durchgesetzt, oft nach seinen Urhebern auch Dolev-Yao-Modell [1] bezeichnet. Es trifft eine bewusste Vereinfachung: Kryptografie wird als ideal angenommen, d.h. ein Angreifer kann eine korrekt eingesetzte Verschlüsselung nicht brechen und eine Signatur ohne den passenden Schlüssel nicht fälschen. Diese Abstraktion ist genau die Stärke des Ansatzes: Sie lenkt den Fokus weg von der Härte einzelner kryptografischer Algorithmen und hin zu der Frage, ob diese Algorithmen im Protokoll richtig zusammengesetzt sind. Denn in der Komposition liegen oft fatale Schwachstellen.

Im Gegenzug ist der Angreifer in diesem Modell mächtig: Er kontrolliert das gesamte Netzwerk, kann jede Nachricht mitlesen, abfangen, verändern, neu zusammensetzen oder eigene einschleusen. Modelliert werden kann auch, dass der Angreifer einzelne Komponenten kompromittieren und an deren geheime Schlüssel gelangen kann. Wer unter diesen Voraussetzungen ein Protokoll als sicher beweisen kann, hat ein sehr belastbares Ergebnis: Es ist unabhängig von der konkreten Netzkonfiguration und deckt auch ungewöhnliche Angriffsreihenfolgen ab, die ein menschlicher Tester kaum systematisch durchspielen würde.

In der Forschung kam Tamarin-Prover [2], ein etabliertes Open-Source-Tool für die automatisierte Verifikation im Symbolic Modell, zum Einsatz. Das Protokoll wird als Regelsystem beschrieben und die Sicherheitsziele werden in einer Logik über Ereignisse und ihre zeitliche Reihenfolge formuliert. Tamarin sucht dann über eine unbegrenzte Zahl paralleler Protokollläufe entweder einen Beweis oder ein Gegenbeispiel. Verwandte Werkzeuge wie ProVerif arbeiten nach einem ähnlichen Prinzip. Darüber hinaus gibt es verschiedene Verifikationswerkzeuge [3]. Tamarin wurde in der Vergangenheit etwa für die Analyse von TLS 1.3 [4] eingesetzt. Sie ist also kein exotisches Verfahren, sondern Stand der Technik bei der Entwicklung sicherheitskritischer Protokolle.

Der Beleg: Schwachstellen im neuen UDS-Standard

Wie aussagekräftig diese Methode ist, zeigt eine Analyse der Fahrzeugdiagnose [5]. Das Protokoll Unified Diagnostic Services (UDS) nach ISO 14229 ist eine der wichtigsten Schnittstellen moderner Fahrzeuge: Über UDS werden Steuergeräte ausgelesen, konfiguriert und mit neuer Software versorgt; lokal über den Diagnosestecker, zunehmend aber auch remote über Diagnostics over IP (DoIP). Gerade die Remote-Variante erweitert die Angriffsfläche erheblich: Ein Angreifer im Werkstattnetz oder mit einem manipulierten Gerät am Fahrzeug kann diese Schnittstelle missbrauchen, um direkt auf geschützte Funktionen zuzugreifen.

Die Brisanz: Der Standard war gerade erst überarbeitet worden, um genau solche Risiken zu adressieren. Mit der 2020 veröffentlichten Fassung (ISO 14229-1:2020) wurde ein neuer Authentication-Service eingeführt, der den älteren, berüchtigt interpretationsoffenen SecurityAccess-Service ablösen sollte. Neu eingeführt wurde beidseitige Authentifizierung, feingranularer Zugriffskontrolle und optionaler Austausch von Sitzungsschlüsseln zur Verschlüsselung. Auf dem Papier ein klarer Fortschritt.

Das Team modellierte sämtliche Sicherheitsmechanismen dieses Standards im Symbolic Modell mit Tamarin nach und verifizierte sie. Zuerst fiel auf, dass der Standard immer noch eine unsichere Minimalkonfiguration für das verwendete Authentifizierungsverfahren zulässt. Doch selbst bei korrekter, nach aktuellem ISO/IEC-9798-Standard vorgeschriebener Konfiguration fand man zwei bislang unbekannte Schwachstellen im Protokolldesign selbst, die in Kombination ein ernstes Sicherheitsproblem darstellen.

Schwachstelle 1: Die Verbindungsparameter sind nicht authentifiziert. Der Standard schreibt nicht vor, dass die ausgehandelte Kommunikationskonfiguration, darunter die Frage, ob überhaupt ein Sitzungsschlüssel und damit eine verschlüsselte Verbindung etabliert werden soll, Teil der signierten Authentifizierungsdaten sein muss. Ein Man-in-the-Middle-Angreifer kann diese Parameter folglich frei manipulieren. Er kann zum Beispiel den Wunsch des Clients nach einem Sitzungsschlüssel-Austausch unbemerkt aus der Anfrage entfernen.

Schwachstelle 2: Eingeschleuste Sitzungsschlüssel werden akzeptiert. Der Standard betont nicht hinreichend, wie der Client die Echtheit eines empfangenen Sitzungsschlüssels prüfen muss. Problem: Das Zertifikat des Clients ist öffentlich, so dass ein Angreifer es bereits aus der Verbindungsanfrage mitlesen kann. Dieser kann dann einen beliebigen, selbst gewählten Schlüssel so verpacken, dass der Client ihn als gültig annimmt.

Einzeln wirken beide Punkte überschaubar. In Kombination heben sie die gesamte Schutzwirkung aus den Angeln wie in Bild 1 dargestellt. Der Angreifer entfernt zunächst die Anforderung nach verschlüsselter Kommunikation (Schwachstelle 1), sodass der Server unverschlüsselt weiterarbeitet. Nach erfolgreicher Authentifizierung schleust er dann einen eigenen Sitzungsschlüssel ein (Schwachstelle 2). Damit sitzt er als Man-in-the-Middle zwischen Tester und Steuergerät, kann die Kommunikation entschlüsseln, beliebig verändern und Antworten fälschen. Die vom Standard angestrebte Absicherung der nachfolgenden Diagnosekommunikation ist vollständig umgangen.

Der entscheidende Punkt für die Praxis: Es handelt sich nicht um Implementierungsfehler eines einzelnen Herstellers, sondern um Lücken im Standard selbst. Jede konforme Umsetzung erbt sie. Hätte man die Protokolle vor der Veröffentlichung formal analysiert, wären diese Schwachstellen aufgefallen, bevor sie überhaupt Teil des Standards wurden und in Steuergeräten weltweit landen, deren Aktualisierung über Produktlebenszyklen von vielen Jahren ungleich aufwendiger ist als eine Korrektur im Dokument.

Reparieren statt nur diagnostizieren

Ein formales Modell ist nicht nur ein Diagnose-, sondern auch ein Konstruktionswerkzeug. Für beide Schwachstellen wurden konkrete Gegenmaßnahmen entworfen und deren Wirksamkeit anschließend wieder mit Tamarin bewiesen [5]. Schwachstelle 1 lässt sich schließen, indem die Kommunikationskonfiguration in die signierten Authentifizierungsdaten aufgenommen wird. Gegen Schwachstelle 2 hilft, dass der Server den erzeugten Sitzungsschlüssel zusammen mit einer Client-Zufallszahl und der Client-Identität signiert, bevor er ihn überträgt.

Für Hersteller, die UDS heute einsetzen, lautet die pragmatische Empfehlung: nicht die minimalen Anforderungen des Standards umsetzen, sondern ISO/IEC 9798-basierte Authentifizierung verwenden, die beschriebenen Modifikationen einbauen und, besonders im Remote- und Netzwerkfall, die Sicherheitsmechanismen der darunterliegenden Schicht nutzen, etwa TLS-gesicherte DoIP-Sitzungen, solange die Lücken im Standard bestehen. Alle unsere formalen Modelle und Beweise sind quelloffen verfügbar.

Kein Einzelfall: ein Muster über die ganze Protokolllandschaft

Die Diagnose ist nur ein Beispiel. Quer durch die automobile Protokollwelt deckt die formale Analyse reale Probleme auf, die zuvor unentdeckt blieben. Bei SOME/IP, dem Service-orientierten Middleware-Protokoll über Automotive Ethernet, traten Man-in-the-Middle-Angriffe auf, bei dem ein kompromittiertes Steuergerät ein fremdes Service-Angebot imitiert, die selbst dann möglich sind, wenn darunter ein Sicherungsmechanismus auf der Verbindungsschicht aktiv ist; aus der Analyse heraus entstanden zwei verifizierte Schutzerweiterungen [6]. Beim Elektrofahrzeug-Laden nach ISO 15118 (Plug-and-Charge) erhalten die beteiligten Akteure heute mehr personenbezogene Daten als nötig, was Bewegungsprofile ermöglicht. Hier wurde eine datenschutzfreundliche Erweiterung entworfen und ihre Eigenschaften formal belegt [7]. Eine weitere Arbeit überträgt dieselbe Infrastruktur in das Post-Quantum-Zeitalter und weist die Sicherheit der quantensicheren Erweiterung formal nach [8]. Beim Vergleich der Kandidaten zur Absicherung der fahrzeuginternen Ethernet-Kommunikation (SecOC, MACsec, IPsec und TLS) zeigte die Verifikation, dass MACsec allein für Service-orientierte Kommunikation nicht ausreicht, in Kombination mit Zugriffskontrolle aber abgesichert werden kann [9]. Und bei DDS Security, das im Fahrzeug als sichere Alternative zu SOME/IP gehandelt wird, deckte die Tamarin-Analyse einen neuartigen Replay-Angriff auf, den anschließend praktisch nachstellt wurde [10].

Das wiederkehrende Muster ist aufschlussreich: In nahezu jedem untersuchten, standardisierten Protokoll förderte die formale Analyse Schwachstellen zutage, die informellen Prüfungen entgangen waren. Dies ist kein Zufall, sondern eine systematische Eigenschaft des Ansatzes.

Was das für die Entwicklungspraxis bedeutet

Für Entwicklungsteams im Automotive-Umfeld ergeben sich daraus mehrere praktische Konsequenzen. Erstens lohnt sich „shift left“ auch bei der Protokollsicherheit. Eine formale Analyse in der Entwurfsphase ist um Größenordnungen günstiger als die Behebung einer Schwachstelle, die erst im Feld über Rückrufe oder Update-Kampagnen korrigiert werden muss; falls die Steuergeräte überhaupt aktualisierbar sind. Zweitens ersetzt die formale Verifikation weder Code-Review noch Penetrationstest, sondern ergänzt sie. Sie sichert die Logik des Protokoll-Designs ab, während Tests prüfen, ob die Implementierung dieses Design korrekt umsetzt. Drittens richtet sich die deutlichste Botschaft an die Normungsgremien: Sicherheitsrelevante Protokolle sollten formal verifiziert sein, bevor sie als Standard erscheinen.

Die gute Nachricht ist, dass die Einstiegshürde sinkt. Die Werkzeuge sind ausgereift, quelloffen und werden aktiv weiterentwickelt, und veröffentlichte Modelle bieten eine Basis, sodass niemand bei null beginnen muss. Das Beispiel der UDS-Diagnose bringt den Kern in einem Satz auf den Punkt: Eine formale Analyse vor der Standardisierung hätte zwei gravierende Schwachstellen verhindert. Genau diese Reihenfolge „erst beweisen, dann veröffentlichen“ sollte in der Automobilbranche zum Standard werden. (se)

Vergleichsanalyse

Programmiersprachen für Cybersecurity im Automotive-Kontext

Elektromobilität

Security-Tests für die Ladekommunikation

* Chrisoph Kraus ist Head of Automotive Security Research bei Incyde und Professor an der Hochschule Darmstadt. Dr. Daniel Zelle arbeitet als Cybersecurity Senior Expert Automotive bei Incyde. Im Bereich Cybersecurity Automotive ist Timm Lauser bei Incyde tätig.

(ID:50935201)