
إثبات المفهوم باستخدام ProVerif لهجوم التراجع على جهاز فوب للسيارة (CVE-2022-37418, CVE-2022-36945 و CVE-2022-37305)
إثبات مفهوم باستخدام ProVerif لهجوم الاسترجاع على جهاز التحكم بمفتاح السيارة (CVE-2022-37418, CVE-2022-36945 and CVE-2022-37305)، مقدَّم في [1]
ليست لي أي صلة بمؤلفي [1]. وأنا ممتن لهم لإتاحة ورقتهم البحثية للوصول المفتوح.
لتشغيل إثبات المفهوم (PoC) للتحقق الرسمي باستخدام 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:

هذا يعني أنه يجب الضغط على جهاز التحكم بالمفتاح لفتح السيارة، لكن يمكن فتح السيارة عدد مرات أكبر من عدد الضغطات على جهاز التحكم بالمفتاح.
لتوليد ملف 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