क्लॉड ने 18 करोड़ लाइन के गणितीय प्रमाण लिखकर दिखाया, 123 ओपन-सोर्स लाइब्रेरी क्रैश नहीं होंगी

एंथ्रोपिक का कहना है कि उसके क्लॉड मॉडल ने गणितीय प्रमाण लिखकर साबित किया है कि बड़े पैमाने पर इस्तेमाल होने वाली 123 ओपन-सोर्स सॉफ्टवेयर लाइब्रेरी मेमोरी की गड़बड़ी से क्रैश नहीं होंगी, और यह जांच सीधे मशीन कोड तक की गई है। कंपनी ने इसे “असेंबली कोड स्तर पर प्रोडक्शन सॉफ्टवेयर पर औपचारिक सत्यापन लागू करने के लिए एआई के इस्तेमाल का पहला बड़े पैमाने का प्रयास” बताया है।

एंथ्रोपिक की फ्रंटियर रेड टीम ने वेरिफिकेशन स्टार्टअप थियोरम के साथ यह काम प्रकाशित किया है। इसमें OSS-Fuzz में परखी जाने वाली लाइब्रेरी के 239 फज़-टेस्ट एंट्री पॉइंट शामिल थे। OSS-Fuzz गूगल का कार्यक्रम है जो ओपन-सोर्स कोड पर लगातार बेतरतीब इनपुट की बौछार करता है। कुछ हफ्तों में क्लॉड ने रॉक (Rocq) में करीब 18 करोड़ लाइन के प्रमाण तैयार किए। रॉक एक प्रूफ असिस्टेंट है जो हर कदम को यांत्रिक रूप से जांचता है। औसतन 18,000 RISC-V निर्देशों वाले प्रोग्राम का एक आम प्रमाण करीब 6 लाख लाइन का रहा।

जो साबित हुआ उसका दायरा संकरा है, पर बात पक्की है। पोस्ट के मुताबिक हर प्रोग्राम 64 MB से कम के किसी भी इनपुट पर “मेमोरी-सुरक्षा की गलती या असफल असर्शन के बिना हमेशा सामान्य रूप से बंद होगा।” शर्त यह है कि प्रोग्राम सिंगल-थ्रेडेड स्टैटिक बाइनरी हो और लिनक्स के तहत RISC-V प्रोसेसर पर चले।

टेस्टिंग से छूटे बग

वहां तक पहुंचने के लिए पहले कोड ठीक करना पड़ा। क्लॉड ने जो खामियां पाईं उन्हें पैच किया और फिर पैच हुए संस्करण का प्रमाण बनाया। टीम का कहना है कि इस दौरान सैकड़ों बग सामने आए, जिनमें से कुछ खरबों स्वचालित टेस्ट के बाद भी बचे रह गए थे।

इनमें एक डीकंप्रेसर में काउंटर अंडरफ्लो था, जो सीमा से बाहर लिखने की वजह बन सकता था, लेकिन सिर्फ करीब 20 MB के एक दुर्लभ इनपुट पर। एक इमेज डिकोडर की खामी सामने आने के लिए 64 MB इनपुट और 2 GB से ज़्यादा मेमोरी चाहिए थी। एक और सीमा से बाहर पढ़ने की गलती तभी दिखती थी जब एक ही फाइल के दो हैंडल पर खास क्रम में कॉल हों। क्लॉड ने XML पार्सर libexpat की एक ज्ञात कमज़ोरी भी दोबारा खोज निकाली, जिसके लिए गहराई तक नेस्टेड इनपुट चाहिए था।

हर समस्या क्रैश वाली नहीं थी। एक लाइब्रेरी में यह तय करने वाला फीचर कि कोई ऐप्लिकेशन कौन सी फाइलें लोड कर सकता है, हमेशा लागू नहीं होता था। एक पीडीएफ रीडर पर अलग प्रयास में टीम का कहना है कि उसे एक हफ्ते में उतने सुरक्षा बग मिले जितने आम तौर पर साल भर में रिपोर्ट होते हैं।

इस काम में यह प्रमाण भी शामिल है कि लिनक्स कर्नेल का zlib कंप्रेशन कोड x86 बाइनरी स्तर पर इस फॉर्मेट के औपचारिक मानक से मेल खाता है।

इसका मतलब क्या नहीं है

एंथ्रोपिक साफ कहती है कि “औपचारिक रूप से सत्यापित” का मतलब बग-मुक्त नहीं है। प्रमाण उतना ही अच्छा है जितना उसका स्पेसिफिकेशन और मशीन का मॉडल। ये प्रमाण RISC-V पर musl libc मानकर चलते हैं, जबकि दुनिया के ज़्यादातर सर्वर और फोन glibc के साथ x86 या ARM पर चलते हैं। हर एंट्री पॉइंट सत्यापित नहीं हुआ, और बेकार पड़ा कोड तथा कॉल करने वालों का गलत इस्तेमाल इस गारंटी से बाहर है।

टीम ने एआई की एक जानी-पहचानी गड़बड़ी पर भी नज़र रखी: क्लॉड किसी प्रोग्राम को ऐसा बदलकर भी प्रमाण पूरा कर सकता था कि वह कभी क्रैश ही न हो, क्योंकि वह कुछ करता ही नहीं। इसे रोकने के लिए पैच पर दंड लगाया गया, उन्हें दर्ज किया गया और उनका ऑडिट हुआ।

सबसे बड़ी सीमा लागत है, क्योंकि एक प्रमाण में करोड़ों टोकन खर्च हो सकते हैं। एंथ्रोपिक को उम्मीद है कि बेहतर मॉडल और दोबारा इस्तेमाल होने वाले प्रमाण यह लागत घटाएंगे।

प्रमाणों का एक हिस्सा और थियोरम की RISC-V व लिनक्स सिमैंटिक्स गिटहब पर जारी कर दी गई हैं। जिन प्रमाणों से हमलावरों को अभी तक पैच न हुए बगों का सुराग मिल सकता है, उन्हें रोक लिया गया है। यह रिलीज़ उस हफ्ते आई है जब PHP की खामियों के चलते कई सरकारों को अपनी वेबसाइटें बंद करनी पड़ीं।