Verificación formal del ataque Rollback

Prueba de concepto en ProVerif del ataque Rollback en el llavero de coche (CVE-2022-37418, CVE-2022-36945 y CVE-2022-37305), presentado en [1]

Aviso legal

No tengo ninguna relación con los autores de [1]. Les agradezco que hayan hecho su artículo de acceso abierto.

Instalación de ProVerif

Método oficial

Para ejecutar la PoC de verificación formal con ProVerif, primero instala ProVerif siguiendo las instrucciones de la página oficial.

Binario precompilado

Alternativamente, he precompilado un binario estático para Linux en arquitectura amd64, disponible en la página de lanzamientos del repositorio. También está el ejecutable para Windows.

Asegúrate de añadir permiso de ejecución al ejecutable descargado:

chmod +x proverif_linux_amd64_static

Uso

Clonar el repositorio

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

Ejecutar la verificación en el modelo

proverif model.pv

Deberías ver que la apertura del coche no implica que se haya pulsado el llavero, lo que significa que el atacante ha conseguido abrir el coche:

Exactamente, esta consulta significa que es posible activar el mecanismo de apertura un número de veces mayor que el número de pulsaciones del llavero.

Es necesario pulsar el llavero

Podemos observar que mientras la consulta

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

devuelve false, Proverif nos dice que la consulta

event(car_open) ==> event(fob_pressed)

habría devuelto true:

Significa que el llavero debe ser pulsado para abrir el coche, pero el coche puede abrirse un número de veces mayor que el número de pulsaciones del llavero.

Generación del gráfico del ataque

Graphviz

Para generar el pdf de la traza, ProVerif necesita que Graphviz esté instalado y añadido a la variable de entorno PATH.

Puedes instalarlo en Linux usando:

sudo apt update
sudo apt install graphviz

En Windows, puedes descargar el instalador desde https://graphviz.org/download/ . Asegúrate de añadir la carpeta de instalación a la variable de entorno PATH:

Generación del gráfico

Para generar el gráfico que detalla el ataque, ejecuta

proverif -graph . model.pv

Ahora abre el archivo pdf generado y observa cómo el atacante puede provocar la apertura del coche sin que se haya pulsado el llavero:

Referencias

[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