Verifica formale dell'attacco Rollback

Prova di concetto in ProVerif dell'attacco Rollback sul keyfob dell'auto (CVE-2022-37418, CVE-2022-36945 e CVE-2022-37305), presentata in [1]

Dichiarazione di non responsabilità

Non ho alcun legame con gli autori di [1]. Sono loro grato per aver reso il loro articolo ad accesso aperto.

Installazione di ProVerif

Metodo ufficiale

Per eseguire la PoC di verifica formale con ProVerif, installa prima ProVerif seguendo le istruzioni sulla pagina ufficiale.

Binario precompilato

In alternativa, ho precompilato un binario statico per Linux su architettura amd64, disponibile nella pagina delle release del repository. È disponibile anche l'eseguibile per Windows.

Assicurati di aggiungere il permesso di esecuzione all'eseguibile scaricato:

chmod +x proverif_linux_amd64_static

Utilizzo

Clona il repository

git clone https://github.com/thomasarmel/rollback_car_attack_proverif.git
cd rollback_car_attack_proverif/

Esegui la verifica sul modello

proverif model.pv

Dovresti vedere che l'apertura dell'auto non implica che il key fob sia stato premuto, il che significa che l'attaccante è riuscito ad aprire l'auto:

Esattamente, questa query significa che è possibile attivare il meccanismo di apertura un numero di volte maggiore del numero di pressioni sul key fob.

È necessario premere il key fob

Possiamo notare che mentre la query

inj-event(car_open) ==> inj-event(fob_pressed)

restituisce false, Proverif ci dice che la query

event(car_open) ==> event(fob_pressed)

avrebbe restituito true:

Significa che il fob deve essere premuto per aprire l'auto, ma l'auto può essere aperta un numero di volte maggiore del numero di pressioni del key fob.

Generazione del grafico dell'attacco

Graphviz

Per generare il pdf della traccia, ProVerif richiede che graphviz sia installato e aggiunto alla variabile d'ambiente PATH.

Puoi installarlo su Linux usando:

sudo apt update
sudo apt install graphviz

Su Windows, puoi scaricare il programma di installazione da https://graphviz.org/download/. Assicurati di aggiungere la cartella di installazione alla variabile d'ambiente PATH:

Generazione del grafico

Per generare il grafico che descrive l'attacco, esegui

proverif -graph . model.pv

Ora apri il file pdf generato e osserva come l'attaccante può attivare l'apertura dell'auto senza che il key fob venga premuto:

Riferimenti

[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