Verificação formal do ataque de rollback

Prova de conceito em ProVerif do ataque de rollback em chaves de carro (CVE-2022-37418, CVE-2022-36945 e CVE-2022-37305), apresentado em [1]

Aviso legal

Não tenho nenhuma ligação com os autores de [1]. Sou grato a eles por disponibilizarem o artigo em acesso aberto.

Instalação do ProVerif

Método oficial

Para executar a PoC de verificação formal com ProVerif, primeiro instale o ProVerif seguindo as instruções na página oficial.

Binário pré-compilado

Alternativamente, compilei previamente um binário estático para Linux em arquitetura amd64, disponível na página de releases do repositório. Também há o executável para Windows.

Certifique-se de adicionar permissão de execução ao executável baixado:

chmod +x proverif_linux_amd64_static

Utilização

Clonar o repositório

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

Executar a verificação no modelo

proverif model.pv

Você deve ver que a abertura do carro não implica que a chave tenha sido pressionada, ou seja, o atacante conseguiu abrir o carro:

Exatamente, esta consulta significa que é possível acionar o mecanismo de abertura um número de vezes maior do que o número de pressionamentos na chave.

Necessidade de pressionar a chave

Podemos notar que, enquanto a consulta

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

retorna false, o ProVerif nos diz que a consulta

event(car_open) ==> event(fob_pressed)

teria retornado true:

Isso significa que a chave precisa ser pressionada para abrir o carro, mas o carro pode ser aberto um número de vezes maior do que o número de pressionamentos da chave.

Gerando o gráfico do ataque

Graphviz

Para gerar o pdf da trilha, o ProVerif precisa que o graphviz esteja instalado e adicionado à variável de ambiente PATH.

Você pode instalá-lo no Linux usando:

sudo apt update
sudo apt install graphviz

No Windows, você pode baixar o instalador em https://graphviz.org/download/ . Certifique-se de adicionar a pasta de instalação à variável de ambiente PATH:

Geração do gráfico

Para gerar o gráfico que detalha o ataque, execute

proverif -graph . model.pv

Agora abra o arquivo pdf gerado e veja como o atacante pode acionar a abertura do carro sem que a chave seja pressionada:

Referências

[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