ロールバック攻撃の形式検証

[1]で発表された、カーキーフォブに対するロールバック攻撃（CVE-2022-37418、CVE-2022-36945、CVE-2022-37305）のProVerifによる概念実証

免責事項

私は[1]の著者とは一切関係ありません。彼らが論文をオープンアクセスにしてくれたことに感謝します。

ProVerifのインストール

公式の方法

ProVerifの形式検証PoCを実行するには、まず公式ページの指示に従ってProVerifをインストールしてください。

ビルド済みバイナリ

あるいは、amd64アーキテクチャのLinux向けに事前コンパイルした静的バイナリを用意してあり、リポジトリのリリースページから入手できます。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