Формальная верификация атаки Rollback

Доказательство концепции на ProVerif атаки Rollback на автомобильный ключ-брелок (CVE-2022-37418, CVE-2022-36945 and CVE-2022-37305), представленное в [1]

Отказ от ответственности

Я не связан с авторами [1]. Я благодарен им за то, что они сделали свою статью открытой.

Установка ProVerif

Официальный способ

Чтобы запустить доказательство концепции формальной верификации ProVerif, сначала установите ProVerif, следуя инструкциям на официальной странице.

Предварительно собранный бинарный файл

В качестве альтернативы я предварительно скомпилировал статический бинарный файл для Linux на архитектуре amd64, доступный на странице релизов репозитория. Также есть исполняемый файл для Windows.

Убедитесь, что вы добавили права на выполнение для загруженного исполняемого файла:

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

Вы должны увидеть, что открытие автомобиля не означает, что была нажата кнопка на ключ-брелоке, то есть атакующий смог открыть автомобиль:

Именно так, этот запрос означает, что можно инициировать механизм открытия количество раз, превышающее количество нажатий на ключ-брелоке.

Необходимость нажатия на ключ-брелок

Можно заметить, что в то время как запрос

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

возвращает false, Proverif сообщает нам, что запрос

event(car_open) ==> event(fob_pressed)

вернул бы true:

Это означает, что брелок должен быть нажат для открытия автомобиля, но автомобиль может быть открыт количество раз, превышающее количество нажатий на ключ-брелок.

Создание графа атаки

Graphviz

Для создания PDF-файла трассы ProVerif требует, чтобы graphviz был установлен и добавлен в переменную окружения PATH.

Вы можете установить его в Linux, используя:

sudo apt update
sudo apt install graphviz

В Windows вы можете загрузить установщик по адресу https://graphviz.org/download/. Убедитесь, что вы добавили папку установки в переменную окружения PATH:

Создание графа

Чтобы создать граф, детализирующий атаку, выполните

proverif -graph . model.pv

Теперь откройте сгенерированный pdf-файл и посмотрите, как атакующий может инициировать открытие автомобиля без нажатия на ключ-брелок:

Ссылки

[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