
प्रोवेरिफ (ProVerif) द्वारा कार की रिमोट चाबी (कीफोब) पर रोलबैक हमले का प्रूफ ऑफ कॉन्सेप्ट (CVE-2022-37418, CVE-2022-36945 और CVE-2022-37305)
कार कीफोब पर रोलबैक हमले का ProVerif प्रूफ ऑफ कॉन्सेप्ट (CVE-2022-37418, CVE-2022-36945 और CVE-2022-37305), [1] में प्रस्तुत
मेरा [1] के लेखकों से कोई संबंध नहीं है। मैं उनके आभारी हूँ कि उन्होंने अपने पेपर को ओपन एक्सेस बनाया।
ProVerif औपचारिक सत्यापन PoC चलाने के लिए, पहले आधिकारिक पृष्ठ पर दिए गए निर्देशों का पालन करके ProVerif स्थापित करें।
वैकल्पिक रूप से, मैंने amd64 आर्किटेक्चर पर लिनक्स के लिए एक स्टैटिक बाइनरी पूर्व-संकलित की है, जो रिपॉजिटरी के रिलीज़ पृष्ठ पर उपलब्ध है। विंडोज के लिए भी एक निष्पादन योग्य है।
डाउनलोड किए गए निष्पादन योग्य में निष्पादन अनुमति जोड़ना सुनिश्चित करें:
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 एन्व वेरिएबल में जोड़े जाने की आवश्यकता है।
आप इसे लिनक्स पर निम्नलिखित का उपयोग करके स्थापित कर सकते हैं:
sudo apt update
sudo apt install graphviz
विंडोज पर, आप 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