⚡ electrical engineering

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs

यह शोध पत्र ESBMC-Arduino को प्रस्तुत करता है, जो एक हार्डवेयर-वफादार सत्यापन ढांचा (framework) है जो एक डिक्लेरेटिव हार्डवेयर एब्स्ट्रैक्शन लेयर और साउंड इनपुट-रेंज मॉडलिंग को एकीकृत करके ओपन-हार्डवेयर PLCs के लिए परिनियोजन अंतराल (deployment gap) को पाटता है, ताकि आदर्श पूर्णांक धारणाओं (idealized integer assumptions) के कारण होने वाली गलत सूचनाओं को समाप्त किया जा सके और संसाधन-बाधित माइक्रोकंट्रोलर्स पर चलने वाले IEC 61131-3 प्रोग्रामों में वास्तविक विड्थ-डिपेंडेंट दोषों का पता लगाया जा सके।

मूल लेखक: Pierre Dantas, Lucas Cordeiro, Waldir Junior

प्रकाशित 2026-07-10

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Pierre Dantas, Lucas Cordeiro, Waldir Junior

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक पानी के टैंक को प्रबंधित करने के लिए एक रोबोट बना रहे हैं। आप अपने निर्देश एक विशेष भाषा में लिखते हैं जिसे IEC 61131-3 कहा जाता है, जो औद्योगिक मशीनों के लिए एक सार्वभौमिक रेसिपी बुक की तरह है। वर्षों से, इंजीनियरों ने इन रेसिपीज़ को जांचने के लिए "सुपर-रोबोट" सिम्युलेटर का उपयोग किया है। ये सिम्युलेटर जादूगरों की तरह होते हैं जो अनंत संख्याओं के साथ सोच सकते हैं; वे मान लेते हैं कि रोबोट अपने दिमाग में कोई भी संख्या रख सकता है, चाहे वह ऋणात्मक अनंत हो या धनात्मक अनंत, और सेंसर कल्पना की गई किसी भी वैल्यू की रिपोर्ट कर सकते हैं।

लेकिन यहाँ एक मोड़ है: वास्तविक रोबोट जिसे आप बनाते हैं, वह जादूगर नहीं है। वह एक छोटा, सस्ता माइक्रोकंट्रोलर (जैसे कि Arduino) है जो वास्तविक दुनिया में रहता है। इस छोटे चिप के पास एक बहुत ही विशिष्ट, सीमित मस्तिष्क होता है। यह केवल 32,767 तक की संख्याएँ रख सकता है। यदि कोई गणना इससे ऊपर जाती है, तो संख्या केवल बड़ी नहीं होती; यह टूट जाती है, नीचे की ओर वापस आ जाती है, और एक ऋणात्मक संख्या बन जाती है। यह एक कार के ओडोमीटर की तरह है जो 999,999 से वापस 000,000 पर आ जाता है।

बड़ा अंतर (The Great Disconnect)
पेपर इसे "डिप्लॉयमेंट गैप" कहता है। यह जादूगर के सपनों की दुनिया और रोबोट की तंग वास्तविकता के बीच का अंतर है।

लेखकों ने पाया कि जब इंजीनियरों ने अपने कोड की सुरक्षा जांचने के लिए पुराने "जादूगर" सिम्युलेटर का उपयोग किया, तो उन्हें भारी मात्रा में गलत अलार्म (false alarms) मिले। 123 वास्तविक दुनिया के प्रोग्रामों में से, पुराने सिम्युलेटरों ने 54 बार "खतरा!" चिल्लाकर चेतावनी दी (एक 44% गलत-अलार्म दर)। लेकिन जब उन्होंने बारीकी से देखा, तो उन्हें एहसास हुआ कि ये "खतरे" असंभव थे। सिम्युलेटर -32,764 जैसी सेंसर रीडिंग की कल्पना कर रहे थे। वास्तविक दुनिया में, इस रोबोट से जुड़ा एक सेंसर केवल 0 और 1,023 के बीच की संख्या पढ़ सकता है (क्योंकि यह एक 10-बिट सेंसर है)। -32,764 की वैल्यू एक थर्मामीटर द्वारा "ऋण 32,764 डिग्री" पढ़ने जैसी है—यह संभव ही नहीं है।

पेपर तर्क देता है कि इन पुराने सिम्युलेटरों पर भरोसा करना एक सुरक्षा गार्ड के "घुसपैठिया!" चिल्लाने जैसा है क्योंकि उसने एक भूत देखा। गार्ड तकनीकी रूप से भूत के बारे में "सही" है, लेकिन वह बेकार है क्योंकि भूत अस्तित्व में ही नहीं हैं। लेखक स्पष्ट रूप से इस विचार को खारिज करते हैं कि आप केवल गणितीय त्रुटियों की जांच करके बिना यह देखे कि सेंसर वास्तव में क्या देख सकते हैं, जांच कर सकते हैं। वे दिखाते हैं कि ऐसा करने से सत्यापन (verification) व्यवहार में "अनसाउंड" (अविश्वसनीय) हो जाता है।

जादुई समाधान: HAL डिस्क्रिप्टर (The Magic Fix: The HAL Descriptor)
इसे ठीक करने के लिए, लेखकों ने ESBMC-Arduino नामक एक नया टूल बनाया। इस टूल को एक "रियलिटी चेक" फ़िल्टर के रूप में समझें।

इससे पहले कि जादूगर सिम्युलेटर कोड को देखे, यह नया टूल स्वचालित रूप से हर सेंसर के साथ एक छोटा सा नोट जोड़ देता है। यह कहता है, "हे, याद रखना, यह सेंसर केवल 0 और 1,023 के बीच की संख्या दे सकता है।" यह सिम्युलेटर को यह भी याद दिलाता है, "और याद रखें, रोबोट का दिमाग केवल 32,767 तक की संख्या रख सकता है।"

जब सिम्युलेटर इन नियमों के साथ चलता है, तो जादू होता है:

54 गलत अलार्म तुरंत गायब हो जाते हैं। -32,764 का भूत चला जाता है क्योंकि सिम्युलेटर अब जानता है कि यह संख्या असंभव है।
जो 32 प्रोग्राम पहले से ही सुरक्षित सिद्ध हुए थे, वे सुरक्षित रहते हैं।
सबसे महत्वपूर्ण बात यह है कि इस टूल ने कोई वास्तविक बग मिस नहीं किया। इसने पाया कि पुराने सिम्युलेटर एक विशिष्ट प्रकार के वास्तविक खतरे को छिपा रहे थे: जब एक सेंसर रीडिंग को एक बड़ी संख्या से गुणा किया जाता है (जैसे कि कच्ची सेंसर वैल्यू को प्रतिशत में बदलना), तो गणित उस छोटे रोबोट के दिमाग को ओवरफ्लो कर सकता है।

वास्तविक खतरा (और यह कितना दुर्लभ है)
पेपर ने पाया कि जबकि "भूतिया अलार्म" आम थे, परीक्षण किए गए सार्वजनिक कोड में वास्तविक बग वास्तव में काफी दुर्लभ थे। उन्हें केवल उन विशिष्ट परिदृश्यों में वास्तविक दोष मिले जहाँ एक सेंसर रीडिंग को एक बड़ी स्थिरांक (constant) (जैसे कि 100) से गुणा किया गया था।

उदाहरण के लिए, यदि एक सेंसर 898 पढ़ता है (जो एक सामान्य, वास्तविक वैल्यू है), और कोड इसे 100 से गुणा करता है, तो परिणाम 89,800 होता है। यह 16-बिट रोबोट के दिमाग के लिए बहुत बड़ा है (अधिकतम 32,767)। संख्या वापस घूम जाती है, ऋणात्मक संख्या बन जाती है, और रोबोट सोचता है कि पानी का टैंक खाली है जबकि वास्तव में वह भर रहा है। नए टूल ने इस सटीक परिदृश्य को पकड़ा और इंजीनियरों को उस सेंसर रीडिंग का वास्तविक, भौतिक उदाहरण दिया जो क्रैश का कारण बनेगा।

वह जो पेपर दावा नहीं करता
लेखक इस बारे में बहुत ईमानदार हैं कि उन्होंने क्या नहीं किया। उन्होंने यह साबित नहीं किया कि अब हर प्रोग्राम सुरक्षित है। 123 प्रोग्रामों में से, 91 का परिणाम "अज्ञात" (unknown) रहा। ऐसा इसलिए नहीं है कि टूल टूटा हुआ है; बल्कि इसलिए है क्योंकि उन विशिष्ट प्रोग्रामों को सुरक्षित साबित करने के लिए वर्तमान इंजन के लिए गणित बहुत कठिन है। टूल ने शोर (गलत अलार्म) को सफलतापूर्वक हटा दिया और सिग्नल (वास्तविक प्रमाण) को बनाए रखा, लेकिन यह अभी भी सबसे कठिन पहेलियों को हल नहीं कर सका।

साथ ही, उन्होंने फ्लोटिंग-पॉइंट नंबरों (जैसे 3.14 जैसे दशमलव) या जटिल भौतिकी सिमुलेशन पर इसका परीक्षण नहीं किया। उन्होंने पूरी तरह से पूर्णांकों (integers) और बूलियन लॉजिक (ऑन/ऑफ स्विच) पर ध्यान केंद्रित किया।

मुख्य निष्कर्ष (The Bottom Line)
पेपर यह प्रदर्शित करता है कि ओपन-हार्डवेयर PLC (जैसे कि स्कूलों और छोटी फैक्ट्रियों में उपयोग किए जाने वाले) को सत्यापित करने के लिए, आप केवल गणित की जांच नहीं कर सकते; आपको हार्डवेयर की सीमाओं की भी जांच करनी होगी। स्वचालित रूप से एक "रियलिटी चेक" जोड़कर जो सिम्युलेटर को बताता है कि उसके सेंसर वास्तव में क्या कर सकते हैं, उन्होंने एक शोर भरे, अविश्वसनीय उपकरण को एक भरोसेमंद उपकरण में बदल दिया। उन्होंने लाखों नए बग नहीं खोजे, लेकिन उन्होंने टूल को "गलत चेतावनी" देने से रोक दिया, जिससे इंजीनियरों के लिए सुरक्षा जांच पर फिर से भरोसा करना संभव हो गया।

तकनीकी सारांश: ESBMC-ARDUINO

समस्या: ओपन-हार्डवेयर PLCs में परिनियोजन अंतराल (Deployment Gap)
ओपन-हार्डवेयर प्रोग्रामेबल लॉजिक कंट्रोलर्स (PLCs), जैसे कि Arduino OPTA, CONTROLLINO और Industrial Shields M-Duino पर चलने वाले OpenPLC, कम लागत वाले माइक्रोकंट्रोलर-श्रेणी के उपकरणों के लिए IEC 61131-3 प्रोग्रामिंग को सुलभ बना रहे हैं। ये प्लेटफॉर्म शिक्षा, लघु-स्तरीय स्वचालन और औद्योगिक नियंत्रण प्रणाली (ICS) सुरक्षा अनुसंधान के लिए रनटाइम सबस्ट्रेट के रूप में तेजी से उपयोग किए जा रहे हैं। हालांकि, मौजूदा ओपन-सोर्स वेरीफायर (जैसे, ESBMC-PLC, PLCverif) द्वारा उपयोग किए जाने वाले अमूर्त मॉडलों (abstract models) और वास्तविक हार्डवेयर निष्पादन वातावरण के बीच एक महत्वपूर्ण "परिनियोजन अंतराल" (deployment gap) मौजूद है।

वर्तमान वेरीफायर एक अमूर्त स्कैन-साइकिल मॉडल पर कार्य करते हैं जो आदर्श, असीमित पूर्णांकों (unbounded integers) और अप्रतिबंधित इनपुट्स की धारणा रखता है। इसके विपरीत, तैनात किए गए आर्टिफैक्ट्स विशिष्ट मशीन वर्ड विड्थ (जैसे, 8-बिट AVR बोर्डों पर 16-बिट int) और सीमित-रिज़ॉल्यूशन एनालॉग-टू-डिजिटल कन्वर्टर्स (ADCs, आमतौर पर 10-बिट, जो $[0, 1023]$ मान देते हैं) वाले संसाधन-बाधित माइक्रोकंट्रोलर यूनिट्स (MCUs) पर चलते हैं। यह विसंगति दो प्रकार की विफलताओं को जन्म देती है:

छूटे हुए दोष (Missed Defects): एक प्रोग्राम अमूर्त मॉडल में सुरक्षित सिद्ध हो सकता है, लेकिन संकीर्ण वर्ड विड्थ (जैसे, 16-बिट बोर्ड पर स्केलिंग गणना का रैप-अराउंड होना) के कारण होने वाले इंटीजर ओवरफ्लो के कारण डिवाइस पर असुरक्षित हो सकता है।
फैंटम अलार्म (Phantom Alalarms - काल्पनिक अलार्म): अधिक महत्वपूर्ण रूप से, एक नाईव (naive) विड्थ-अवेयर वेरिफिकेशन, जो वर्ड विड्थ तो ध्यान में रखता है लेकिन हार्डवेयर इनपुट सीमाओं को अनदेखा करता है, उन सेंसर मानों की खोज करता है जिन्हें कोई भौतिक ADC उत्पन्न नहीं कर सकता (जैसे, ऋणात्मक मान या 1023 से अधिक मान)। यह स्प्यूरियस (spurious) ओवरफ्लो रिपोर्टों का परिणाम है। 123 वास्तविक थर्ड-पार्टी प्रोग्रामों के संग्रह पर मूल्यांकन ने दिखाया कि नाईव 16-बिट ओवरफ्लो चेकिंग 44% गलत-अलार्म दर (54/123) देती है जबकि शून्य वास्तविक दोष पाती है।

कार्यप्रणाली: हार्डवेयर-फिथफुल वेरिफिकेशन (Hardware-Faithful Verification)
यह शोध पत्र एक "डिप्लॉयमेंट मॉडल" ( $M_{dev}$ ) का निर्माण करके इस अंतराल को पाटने के लिए एक विधि प्रस्तावित करता है जो लक्षित हार्डवेयर का सटीक प्रतिनिधित्व करता है। इस दृष्टिकोण का मूल आधार एक हार्डवेयर एब्स्ट्रैक्शन लेयर (HAL) डिस्क्रिप्टर और एक साउंड लोअरिंग (sound lowering) प्रक्रिया है।

HAL डिस्क्रिप्टर ( $H$ ): एक डिक्लेरेटिव टुपल $H = \langle w, b_{adc}, b_{pwm}, \mu \rangle$ $H = ⟨ w, b_{a d c}, b_{pw m}, μ ⟩$ जो निम्नलिखित को कैप्चर करता है:
- $w$ : मशीन वर्ड विड्थ (जैसे, AVR के लिए 16-बिट, ARM के लिए 32-बिट)।
- $b_{adc}$ और $b_{pwm}$ : एनालॉग-टू-डिजिटल कन्वर्टर्स और पल्स-विड्थ मॉड्यूलेशन आउटपुट का रिज़ॉल्यूशन।
- $\mu$ : IEC 61131-3 डायरेक्ट-एड्रेसिंग स्कीम से स्वचालित रूप से प्राप्त एक I/O बाइंडिंग मैप (जैसे, %IW एड्रेस विशिष्ट ADC रेंज के साथ एनालॉग इनपुट्स से मैप होते हैं)।
फिथफुल लोअरिंग (Faithful Lowering): यह विधि PLC प्रोग्राम ( $P$ $P$ ) को एक डिप्लॉयमेंट मॉडल ( $M_{dev}(P, H)$ $M_{d e v} (P, H)$ ) में बदलने के लिए निम्नलिखित करती है:
- लक्षित वर्ड विड्थ $w$ पर अंकगणित की व्याख्या करना (दो'स-कंपलीमेंट रैप-अराउंड को सटीक रूप से पुनरुत्पादित करना)।
- इनपुट सैंपलिंग के तुरंत बाद assume बाधाओं (constraints) को इंजेक्ट करना ताकि वेरिएबल्स को उनके हार्डवेयर-रियलाइजेबल रेंज (जैसे, $0 \leq adc \leq 1023$ ) तक सीमित किया जा सके।
- नॉन-लीनियर फंक्शन ब्लॉक्स (जैसे, PID) को नॉन-डिटरमिनिस्टिक आउटपुट के साथ ओवर-एप्रोक्सिमेट करना ताकि ट्रैक्टेबिलिटी बनी रहे।
वेरिफिकेशन इंजन: यह विधि बिना किसी संशोधन के ESBMC बैकएंड (SMT-आधारित बाउंडेड मॉडल चेकिंग और $k$ -इंडक्शन) का पुन: उपयोग करती है। लोअरिंग लैडर डायग्राम (LD) फ्रंटएंड में होती है, जिसमें एक हल्का हुक (लगभग 40 लाइनें) जोड़ा जाता है जो इनपुट बाउंड्स को लागू करता है और आर्किटेक्चर वर्ड विड्थ सेट करता है।

प्रमुख योगदान

हार्डवेयर-फिथफुल वेरिफिकेशन विधि: एक औपचारिक दृष्टिकोण जो सुरक्षा-महत्वपूर्ण एम्बेडेड C (Frama-C और Astrée जैसे टूल्स द्वारा स्थापित) के टार्गेट-मॉडल अनुशासन को PLC डोमेन में स्थानांतरित करता है। उन टूल्स के विपरीत, जिन्हें मैनुअल इनपुट कॉन्ट्रैक्ट्स की आवश्यकता होती है, यह विधि स्वचालित रूप से इनपुट बाउंड्स को मानक IEC 61131-3 एड्रेसिंग स्कीम और बोर्ड डिस्क्रिप्टर्स से प्राप्त करती है।
ESBMC-Arduino इंस्टेंशिएशन: Arduino-क्लास लक्ष्यों के लिए एक ठोस कार्यान्वयन, जो आधिकारिक Arduino कोर्स से HAL पैरामीटर्स प्राप्त करता है। यह 16-बिट (AVR) और 32-बिट (ARM) लक्ष्यों दोनों का समर्थन करता है।
अनुभवजन्य मूल्यांकन (Empirical Evaluation): 123 वास्तविक-विश्व प्रोग्रामों और 20 पैटर्न के एक नियंत्रित संग्रह पर एक कठोर मूल्यांकन।

परिणाम

गलत अलार्मों का उन्मूलन: 123-प्रोग्राम के संग्रह पर, HAL एनोटेटर को सक्षम करने से सभी 54 गलत अलार्म समाप्त हो गए (असुरक्षित काउंट को 54 से घटाकर 0 कर दिया गया) जबकि प्रत्येक रोबस्टनेस प्रूफ को सुरक्षित रखा गया (32 प्रोग्राम सुरक्षित सिद्ध रहे)।
वास्तविक दोषों का पता लगाना: एक नियंत्रित संग्रह ने प्रदर्शित किया कि यह विधि भौतिक रूप से संभव साक्ष्यों (witnesses) के साथ वास्तविक, विड्थ-डिपेंडेंट दोषों (जैसे, 16-बिट बोर्डों पर ADC-टू-परसेंटेज स्केलिंग में ओवरफ्लो) का पता लगाती है।
क्रॉस-टूल वैलिडेशन: "फैंटम अलार्म" की घटना को लॉजिक के C मिरर्स पर स्वतंत्र टूल्स (CBMC और Frama-C/EVA) का उपयोग करके पुन: उत्पन्न किया गया, जो पुष्टि करता है कि यह मुद्दा इनपुट मॉडलिंग के बिना नाईव विड्थ-अवेयर वेरिफिकेशन की अंतर्निहित समस्या है, न कि केवल ESBMC की।
प्रदर्शन: HAL एनोटेटर का ओवरहेड नगण्य है; वेरिफिकेशन समय एक सेकंड प्रति प्रोग्राम से कम रहता है।
सीमाएँ: जबकि गलत अलार्म समाप्त हो गए हैं, 91 प्रोग्रामों ने इंटरनल स्टेट वाले फंक्शन ब्लॉक्स पर $k$ -इंडक्शन अपूर्णता के कारण "अननोन" (unknown) वर्डिक्ट दिए। यह प्रोवर की इंडक्टिव स्टेप्स को क्लोज करने की क्षमता की एक सीमा है, न कि इनपुट मॉडल की।

महत्व
यह शोध पत्र तर्क देता है कि इस कार्य का प्राथमिक मूल्य खोजे गए बगों की संख्या में नहीं है (जो विशेष रूप से सर्वेक्षण किए गए सार्वजनिक संग्रहों में दुर्लभ हैं, जो कि Boolean और टाइमर लॉजिक द्वारा प्रधान हैं), बल्कि सत्यता की बहाली (restoration of soundness) में है। लेखक प्रदर्शित करते हैं कि नाईव विड्थ-अवेयर वेरिफिकेशन, 44% गलत-अलार्म दर के कारण, आश्वासन के लिए अनुपयोगी है जो वास्तविक निष्कर्षों को दबा देती है। हार्डवेयर-रियलाइजेबल इनपुट रेंज को स्वचालित रूप से प्राप्त करके, यह विधि एक अविश्वसनीय टूल को एक ऐसे टूल में बदल देती है जो केवल रियलाइजेबल रिपोर्ट जारी करता है, जिससे इंजीनियर ओपन-हार्डवेयर PLCs के लिए वेरिफिकेशन परिणामों पर भरोसा कर सकते हैं। इस दृष्टिकोण को एक यथार्थवादी, कम लागत वाली एडॉप्शन रणनीति के रूप में प्रस्तुत किया गया है (एक 4-फील्ड डिस्क्रिप्टर और एक 40-लाइन हुक) जो क्लीन-स्लेट प्रस्ताव के बजाय परिपक्व वेरिफिकेशन इंफ्रास्ट्रक्चर के साथ एकीकृत होता है।

इसी तरह के और पेपर