thomasarmel/rollback_car_attack_proverifPreuve de concept ProVerif de l'attaque par rollback sur la clé de voiture (CVE-2022-37418, CVE-2022-36945 et CVE-2022-37305)
Preuve de concept ProVerif de l'attaque par rollback sur la télécommande de voiture (CVE-2022-37418, CVE-2022-36945 et CVE-2022-37305), présentée dans [1]
Je n'ai aucun lien avec les auteurs de [1]. Je leur suis reconnaissant d'avoir rendu leur article en accès libre.
Pour exécuter la preuve de concept de vérification formelle ProVerif, installez d'abord ProVerif en suivant les instructions sur la page officielle.
Alternativement, j'ai précompilé un binaire statique pour Linux sur architecture amd64, disponible sur la page des versions du dépôt. Il existe également l'exécutable pour Windows.
Assurez-vous d'ajouter la permission d'exécution à l'exécutable téléchargé :
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
Vous devriez constater que l'ouverture de la voiture n'implique pas que la télécommande a été pressée, ce qui signifie que l'attaquant a réussi à ouvrir la voiture :
Exactement, cette requête signifie qu'il est possible de déclencher le mécanisme d'ouverture un nombre de fois supérieur au nombre de pressions sur la télécommande.
On peut remarquer que tandis que la requête
inj-event(car_open) ==> inj-event(fob_pressed)
renvoie false, Proverif nous indique que la requête
event(car_open) ==> event(fob_pressed)
aurait renvoyé true :
Cela signifie que la télécommande doit être pressée pour ouvrir la voiture, mais que la voiture peut être ouverte un nombre de fois supérieur au nombre de pressions sur la télécommande.
Afin de générer le pdf de trace, ProVerif nécessite que graphviz soit installé et ajouté à la variable d'environnement PATH.
Vous pouvez l'installer sur Linux en utilisant :
sudo apt update
sudo apt install graphviz
Sur Windows, vous pouvez télécharger l'installateur sur https://graphviz.org/download/ . Assurez-vous d'ajouter le dossier d'installation à la variable d'environnement PATH :
Pour générer le graphique détaillant l'attaque, exécutez
proverif -graph . model.pv
Ouvrez maintenant le fichier pdf généré et voyez comment l'attaquant peut déclencher l'ouverture de la voiture sans que la télécommande ne soit pressée :
[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