thomasarmel/rollback_car_attack_proverifProVerif Proof of Concept des Rollback-Angriffs auf Auto-Funkschlüssel (CVE-2022-37418, CVE-2022-36945 und CVE-2022-37305)
ProVerif-Proof-of-Concept des Rollback-Angriffs auf Autoschlüsselanhänger (CVE-2022-37418, CVE-2022-36945 und CVE-2022-37305), vorgestellt in [1]
Ich habe keine Verbindung zu den Autoren von [1]. Ich bin ihnen dankbar, dass sie ihre Arbeit als Open Access zugänglich gemacht haben.
Um den ProVerif-Proof-of-Concept zur formellen Verifikation auszuführen, installieren Sie zuerst ProVerif, indem Sie den Anweisungen auf der offiziellen Seite folgen.
Alternativ habe ich eine statische Binärdatei für Linux auf amd64-Architektur vorkompiliert, die auf der Release-Seite des Repositorys verfügbar ist. Es gibt auch die ausführbare Datei für Windows.
Stellen Sie sicher, dass Sie der heruntergeladenen ausführbaren Datei die Ausführungsberechtigung hinzufügen:
chmod +x proverif_linux_amd64_static
git clone https://github.com/thomasarmel/rollback_car_attack_proverif.git
cd rollback_car_attack_proverif/
proverif model.pv
Sie sollten sehen, dass das Öffnen des Autos nicht impliziert, dass der Schlüsselanhänger gedrückt wurde – der Angreifer hat das Auto also erfolgreich geöffnet:
Genau genommen bedeutet diese Abfrage, dass es möglich ist, den Öffnungsmechanismus öfter auszulösen, als der Schlüsselanhänger gedrückt wurde.
Wir können feststellen, dass die Abfrage
inj-event(car_open) ==> inj-event(fob_pressed)
false zurückgibt, ProVerif uns jedoch mitteilt, dass die Abfrage
event(car_open) ==> event(fob_pressed)
true zurückgegeben hätte:
Das bedeutet, dass der Schlüsselanhänger gedrückt werden muss, um das Auto zu öffnen, das Auto jedoch öfter geöffnet werden kann, als der Schlüsselanhänger gedrückt wurde.
Um das Trace-PDF zu erzeugen, benötigt ProVerif, dass Graphviz installiert und zur Umgebungsvariable PATH hinzugefügt ist.
Sie können es unter Linux mit folgendem Befehl installieren:
sudo apt update
sudo apt install graphviz
Unter Windows können Sie das Installationsprogramm unter https://graphviz.org/download/ herunterladen. Stellen Sie sicher, dass Sie den Installationsordner zur Umgebungsvariable PATH hinzufügen:
Um den Graphen zu erzeugen, der den Angriff detailliert darstellt, führen Sie folgenden Befehl aus:
proverif -graph . model.pv
Öffnen Sie nun die erzeugte PDF-Datei und sehen Sie, wie der Angreifer das Öffnen des Autos auslösen kann, ohne dass der Schlüsselanhänger gedrückt wird:
[1] Csikor, Levente and Lim, Hoon Wei and Wong, Jun Wen and Ramesh, Soundarya and Parameswarath, Rohini Poolat and Chan, Mun Choon, Rollback: A new time-agnostic replay attack against the automotive remote keyless entry systems, ACM Transactions on Cyber-Physical Systems, 2024, https://doi.org/10.1145/3627827