Rollback 攻击形式化验证

ProVerif 对汽车遥控钥匙上 Rollback 攻击的概念验证（CVE-2022-37418、CVE-2022-36945 和 CVE-2022-37305），详见 [1]

免责声明

我与 [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