एक प्रूफ़ क्या वादा कर सकता है

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

प्रूफ़ दूसरे सिरे से शुरू होता है। वह स्थितियाँ नहीं आज़माता। वह गणित से दिखाता है कि कोई कथन सभी स्थितियों में सही है।

हर स्थिति, सिर्फ़ आज़माई हुई नहीं

एक छोटा वादा लीजिए: यह कोड कभी अपने बफ़र के अंत के आगे नहीं पढ़ता। एक टेस्ट उसे हज़ार इनपुट दे सकता है, या एक अरब, और बता सकता है कि किसी ने उसे नहीं तोड़ा। प्रूफ़ एक अलग क़िस्म की बात कहता है: ऐसा कोई इनपुट है ही नहीं जो उसे तोड़ दे। कोई मिला नहीं, और कोई मौजूद भी नहीं।

इसकी क़ीमत है कठोरता। प्रूफ़ को इस बात का सटीक कथन चाहिए कि कोड को क्या करना है, जिसे उसका स्पेसिफ़िकेशन कहते हैं, और एक ऐसा तर्क जो कोड की हर लाइन को उससे जोड़े। असली सॉफ़्टवेयर के लिए यह तर्क इतना लंबा होता है कि कोई इंसान उसे आँख से नहीं जाँच सकता। इसलिए उसे कंप्यूटर जाँचता है।

मशीन से जाँचा हुआ

“मशीन-जाँचा” का यही मतलब है। प्रूफ़ पूरा लिखा जाता है, ऐसी भाषा में जिसे प्रूफ़ असिस्टेंट नाम का प्रोग्राम पढ़ सकता है, और वह प्रोग्राम हर चरण को तर्कशास्त्र के नियमों से मिलाकर जाँचता है। वह नौ सौवें पन्ने पर थकता नहीं, और किसी की बात यूँ ही नहीं मान लेता।

seL4 के प्रूफ़ इसी तरह जाँचे जाते हैं, Isabelle/HOL नाम के प्रूफ़ असिस्टेंट में। वे सार्वजनिक हैं, और कोई भी उन्हें दोबारा चला सकता है।

seL4 के प्रूफ़ क्या कहते हैं

seL4 वह कर्नेल है जिस पर हर NoWayOS सिस्टम चलता है: लगभग 10,000 लाइनों का कोड, और अकेला ऐसा कोड जिसके पास डिवाइस का पूरा नियंत्रण है। उसका आकार ही असल बात है। दस हज़ार लाइनों के बारे में तर्क पूरा किया जा सकता है। करोड़ों लाइनों के बारे में अभी नहीं।

seL4 Foundation इन प्रूफ़ों को परतों में रखती है:

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

हर परत हर प्रोसेसर और हर कॉन्फ़िगरेशन के लिए पूरी नहीं हुई है। यह बात मायने रखती है, और हम इस पर लौटेंगे।

प्रूफ़ क्या मानकर चलता है

प्रूफ़ ठीक उतना ही चौड़ा होता है जितना उसका कथन, और वह अपनी मान्यताओं पर खड़ा होता है। seL4 अपनी मान्यताएँ लिखकर रखता है: कि हार्डवेयर वैसा ही व्यवहार करता है जैसा उसका मॉडल कहता है, कि सबसे निचले स्तर के कोड की कुछ सौ लाइनें सही हैं, कि कर्नेल के शुरू होने से पहले चलने वाले कोड ने अपना काम कर दिया है। गोपनीयता का प्रूफ़ टाइमिंग को कवर नहीं करता।

वह इस बारे में कुछ नहीं कहता कि स्पेसिफ़िकेशन सही चीज़ माँग रहा है या नहीं, और कर्नेल के ऊपर के सॉफ़्टवेयर के बारे में भी कुछ नहीं। सिद्ध कर्नेल उस प्रोग्राम को भी पूरी निष्ठा से अलग रखेगा जिसमें बग है। बग फिर भी वहीं है। बस वह किसी और चीज़ तक पहुँच नहीं सकता।

यह प्रूफ़ों की कमज़ोरी नहीं है। यही उन्हें काम का बनाता है: वे ठीक-ठीक बताते हैं कि वे क्या कवर करते हैं, इसलिए आप ठीक-ठीक जानते हैं कि क्या बचा है।

NoWayOS कहाँ खड़ा है

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

हर इमेज बताती है कि वह कहाँ खड़ी है। उसके साथ रखी एक फ़ाइल उसके कर्नेल का कॉन्फ़िगरेशन, एक-एक विकल्प करके, उस कॉन्फ़िगरेशन के सामने दर्ज करती है जिसे seL4 ने सिद्ध किया है। सुरक्षा पेज एक असली फ़ाइल दिखाता है।

हमारे अपने छोटे प्रूफ़

NoWayOS के कोड को भरोसा दूसरे रास्ते से मिलता है: Rust, आइसोलेशन, रिव्यू, टेस्टिंग, और ज़्यादा सीमित क़िस्म के प्रूफ़।

सिस्टम के हिस्सों के बीच चलने वाले मैसेजों के हर डिकोडर के पास बाउंडेड प्रूफ़ हैं, जो Kani नाम के मॉडल चेकर से बने हैं। बाउंडेड प्रूफ़ एक तय आकार तक के हर इनपुट को कवर करता है, यहाँ वह सबसे लंबा रिकॉर्ड जिसे डिकोडर स्वीकार करता है। उस सीमा के भीतर वह असली प्रूफ़ है: कोई भी इनपुट डिकोडर से पैनिक, ओवरफ़्लो या सीमा के बाहर रीड नहीं करा सकता। सीमा के आगे वह कुछ नहीं कहता, और इसीलिए सीमा वही रखी गई है जो सबसे लंबा संभव इनपुट है।

फिर हम डिकोडरों को जानबूझकर तोड़ते हैं, यह पक्का करने के लिए कि प्रूफ़ इसे पकड़ते हैं। जो प्रूफ़ विफल हो ही नहीं सकता, वह उस टेस्ट से बेहतर नहीं जो विफल हो ही नहीं सकता।

इसका ईमानदार आकार

प्रूफ़ किसी चीज़ को “अनहैकेबल” नहीं बनाता। वह एक कथन को सच बनाता है, हर स्थिति में, उन मान्यताओं के तहत जिन्हें आप पढ़ सकते हैं। कथन और मान्यताएँ जान लीजिए, और आप जानते हैं कि आपके पास क्या है।

इसीलिए NoWayOS उस कर्नेल पर बना है जिसके पास ये प्रूफ़ हैं, और इसीलिए वह आपको, एक-एक इमेज करके, बताता है कि वे कहाँ तक पहुँचते हैं।