शब्दावली
शब्द, सरल हिंदी में।
NoWayOS ऑपरेटिंग सिस्टम, सुरक्षा और Rust की दुनिया से शब्द उधार लेता है, और कुछ को एक ख़ास अर्थ में इस्तेमाल करता है। हर एक यहाँ एक-दो पंक्तियों में है।
शब्द वर्णानुक्रम में हैं। किसी परिभाषा के भीतर तिरछे अक्षरों में लिखे शब्द की अपनी अलग प्रविष्टि है।
- अटेस्टेशन
किसी डिवाइस का किसी रिमोट सर्विस के सामने, क्रिप्टोग्राफ़िक तरीके से, यह साबित करना कि उसने कौन-सा सॉफ़्टवेयर शुरू किया। यह दिखाता है कि बूट के समय क्या लोड हुआ, न कि उसके बाद जो कुछ भी हुआ। प्रोडक्शन हार्डवेयर पर NoWayOS के लिए नियोजित; अभी बना नहीं है।
- अटैक सरफ़ेस
वह सब कुछ, जिसे कोई हमलावर किसी डिवाइस के ख़िलाफ़ इस्तेमाल करने की कोशिश कर सकता है: उसका कोड, सर्विस, इंटरफ़ेस और इनपुट। कम कोड और कम फ़ीचर का मतलब है कम अटैक सरफ़ेस।
- आइसोलेशन टेस्ट
एक सिस्टम, जो उस तक पहुँचने की कोशिश करता है जो उसे दिया नहीं गया, और जिसे seL4 को रोकना ही होता है। जान-बूझकर चौड़ी की गई ग्रांट वाला एक वेरिएंट फ़ेल होना ही चाहिए, जिससे पता चलता है कि टेस्ट फ़ेल हो सकता है।
- एक्सपेक्ट फ़ाइल
systems/NAME.expect: वे लाइनें जो किसी सिस्टम को क्रम से प्रिंट करनी ही हैं, और वह टेक्स्ट जो कहीं भी दिख जाए तो टेस्ट फ़ेल हो जाता है। यही फ़ाइल किसी सिस्टम को QEMU में और Raspberry Pi 5 पर जाँचती है।- कैपेबिलिटी
seL4 में, एक ऐसा टोकन जिसकी जालसाज़ी नहीं की जा सकती, जो एक कर्नेल ऑब्जेक्ट और उस पर मिले अधिकारों को नामित करता है, जैसे किसी एक दरवाज़े का कीकार्ड। कोई प्रोटेक्शन डोमेन सिर्फ़ उसी को छू सकता है जिसे उसकी कैपेबिलिटी नामित करती हैं।
- कॉन्फ़िगरेशन से सुरक्षित
किसी जनरल-पर्पज़ डिवाइस की सेटिंग्स बदलकर उसे ज़्यादा सुरक्षित बनाना। फ़ीचर फिर भी वहीं रहते हैं, और एक बग हर सेटिंग को दरकिनार कर सकता है।
- कोल्ड स्टार्ट
पावर बंद होने की स्थिति से शुरुआत, रीसेट के उलट। सिर्फ़ कोल्ड स्टार्ट ही NoWayOS डिवाइस को उसकी फ़ेल-सेफ़ स्थिति से वापस लाता है।
- ग्रांट्स फ़ाइल
systems/NAME.grants: वह सब कुछ जो एक सिस्टम देता है, प्रति लाइन एक तथ्य: प्रायोरिटी, बजट, मेमोरी, डिवाइस, इंटरप्ट और चैनल। अगर सिस्टम डिस्क्रिप्शन और ग्रांट्स फ़ाइल मेल न खाएँ, तो बिल्ड फ़ेल हो जाता है।- ग्लिफ़ एटलस
बिल्ड के समय पहले से ही उसके अक्षरों की इमेज के रूप में ड्रॉ किया गया फ़ॉन्ट, ताकि डिवाइस कभी कोई फ़ॉन्ट फ़ाइल पार्स किए बिना टेक्स्ट ड्रॉ कर सके।
- चैनल
Microkit में, दो प्रोटेक्शन डोमेन के बीच घोषित एक कनेक्शन, नोटिफ़िकेशन (बिना डेटा के सिग्नल, जिनमें इंटरप्ट भी शामिल हैं) और प्रोटेक्टेड प्रोसीजर कॉल के लिए।
- टाइप्ड मैसेज
स्पष्ट लेआउट वाला एक फ़िक्स्ड-साइज़ रिकॉर्ड, जो प्रोटेक्शन डोमेन के बीच शेयर्ड मेमोरी से भेजा जाता है और मिलने पर जाँचा जाता है। देखें पहले कॉपी, फिर जाँच।
- ट्रस्टेड कंप्यूटिंग बेस (TCB)
वह सब कुछ, जिसके सही होने पर कोई सुरक्षा गुण निर्भर करता है। किसी NoWayOS सिस्टम के लिए: seL4 कर्नेल, Microkit लोडर और मॉनिटर, और वे प्रोटेक्शन डोमेन जिन पर वह गुण टिका है।
- डबल-फ़ेच
एक बग, जिसमें कोड शेयर्ड मेमोरी में डेटा जाँचता है और फिर उसे दोबारा पढ़ता है, जिससे दूसरी तरफ़ को बीच में उसे बदलने का मौक़ा मिल जाता है। पहले कॉपी, फिर जाँच इसे रोकता है।
- डेव कंटेनर
पिन की गई कंटेनर इमेज, जिसमें NoWayOS की पूरी टूलचेन है: Rust टूलचेन, Microkit SDK, QEMU और जाँच के टूल। हर
makeटार्गेट इसी में चलता है, इसलिए आपकी मशीन को सिर्फ़ Podman और make चाहिए (और Raspberry Pi 5 चलाने के लिए Python 3.11)।- पहले कॉपी, फिर जाँच
यह नियम कि किसी मैसेज को वैलिडेट करने से पहले शेयर्ड मेमोरी से बाहर कॉपी किया जाता है, ताकि भेजने वाला जाँच और इस्तेमाल के बीच उसे बदल न सके। यह डबल-फ़ेच को रोकता है।
- प्रोटेक्शन डोमेन (PD)
Microkit सिस्टम का एक अलग-थलग हिस्सा: अपनी मेमोरी वाला एक प्रोग्राम, जिसके पास सिर्फ़ वही कैपेबिलिटी होती हैं जो उसे स्पष्ट रूप से दी गई हैं। NoWayOS के सील किए गए कम्पार्टमेंट।
- फ़ज़िंग
किसी पार्सर को लाखों जनरेट किए गए इनपुट से तब तक टेस्ट करना, जब तक कोई इनपुट उसे क्रैश न कर दे या कोई जाँच न तोड़ दे। बाहरी इनपुट के हर NoWayOS पार्सर का एक फ़ज़ टार्गेट है।
- फ़ेल-सेफ़ स्थिति
जहाँ NoWayOS डिवाइस तब जाता है जब फ़ॉल्ट आते ही रहते हैं: कोल्ड स्टार्ट तक सिर्फ़ सुपरवाइज़र, वॉचडॉग और, जहाँ संभव हो, डिस्प्ले चलते रहते हैं।
- फ़ॉर्मल वेरिफ़िकेशन
गणितीय प्रूफ़, जिसे कंप्यूटर जाँचता है, कि सॉफ़्टवेयर अपने स्पेसिफ़िकेशन पर खरा उतरता है। seL4 के पास यह विशिष्ट कॉन्फ़िगरेशन के लिए है। NoWayOS का अपना कोड इसके बजाय Rust, आइसोलेशन, टेस्टिंग और बाउंडेड प्रूफ़ पर निर्भर करता है।
- फ़ॉल्ट
seL4 तब जो रिपोर्ट करता है, जब कोई प्रोटेक्शन डोमेन ऐसा कुछ करता है जिसकी कर्नेल अनुमति नहीं देता, या पैनिक करता है। वह हिस्सा तब तक रुका रहता है, जब तक उसका फ़ॉल्ट हैंडलर कोई कार्रवाई न करे।
- बनावट से सुरक्षित
ऐसा डिवाइस बनाना जो जोखिम भरे काम कर ही नहीं सकता, क्योंकि वे कभी भीतर बनाए ही नहीं गए। NoWayOS का तरीका।
- बाउंडेड प्रूफ़
यह प्रूफ़ कि कोई गुण एक तय आकार तक के हर इनपुट के लिए सही है। NoWayOS अपने मैसेज डिकोडर इसी तरह, Kani से, साबित करता है।
- माइक्रोकर्नेल
जितना हो सके उतना छोटा रखा गया कर्नेल, जिसमें ड्राइवर, नेटवर्किंग और स्क्रीन उसके बाहर, हर एक अपने कम्पार्टमेंट में चलते हैं। seL4 ऐसा ही एक कर्नेल है।
- मिक्स्ड-क्रिटिकैलिटी (MCS) कर्नेल
seL4 का शेड्यूलिंग बजट और पीरियड वाला कॉन्फ़िगरेशन, जिसे Microkit बिल्ड करता है। इसके AArch64 प्रूफ़ पर काम जारी है, इसलिए आज कोई भी NoWayOS इमेज seL4 के पूरे हो चुके प्रूफ़ के दायरे में नहीं है।
- मेमोरी-सेफ़्टी बग
बफ़र के अंत के आगे पढ़ लेना या मेमोरी के फ़्री होने के बाद भी उसे इस्तेमाल करना जैसी ग़लती। Microsoft और Google, दोनों ने बताया है कि उनके गंभीर सुरक्षा बगों में से लगभग 70% इसी तरह के होते हैं; सेफ़ Rust इनकी गुंजाइश ही ख़त्म कर देता है।
- मोनोटोनिक टाइम
बूट से गिना जाने वाला समय, जिसे कभी सेट नहीं किया जाता और जो कभी पीछे नहीं जाता। NoWayOS का हर टाइमआउट इसी का इस्तेमाल करता है, और यह कभी वॉल-क्लॉक टाइम से नहीं मिलता।
- वॉचडॉग
एक हार्डवेयर टाइमर, जो बोर्ड को रीसेट कर देता है, जब तक सॉफ़्टवेयर उसे सर्विस न करे। NoWayOS का वॉचडॉग प्रोटेक्शन डोमेन इसे तभी तक सर्विस करता है, जब तक बाकी हर हिस्सा उसकी हार्टबीट का जवाब देता है।
- वॉल-क्लॉक टाइम
तारीख़ और दिन का समय, किसी प्रमाणीकृत स्रोत से। NoWayOS इसे मोनोटोनिक टाइम से अलग, एक अलग टाइप के रूप में रखता है।
- सिक्योर बूट
किसी डिवाइस का ऐसे सॉफ़्टवेयर को शुरू करने से इनकार करना, जिस पर उसके निर्माता के हस्ताक्षर न हों। प्रोडक्शन हार्डवेयर पर NoWayOS के लिए नियोजित; अभी बना नहीं है।
- सिस्टम डिस्क्रिप्शन
Microkit की XML फ़ाइल, जो किसी सिस्टम के हर प्रोटेक्शन डोमेन, मेमोरी रीजन, चैनल और इंटरप्ट को घोषित करती है। यही सिस्टम का सुरक्षा डिज़ाइन है, और इसमें किसी भी बदलाव का रिव्यू उसी तरह होता है।
- सुपरवाइज़र
वह प्रोटेक्शन डोमेन, जो बाकी हिस्सों के फ़ॉल्ट प्राप्त करता है, उनकी रिपोर्ट करता है और सिस्टम को साफ़ तरीके से दोबारा शुरू करता है।
- CycloneDX
सॉफ़्टवेयर बिल ऑफ़ मटीरियल्स के लिए एक खुला मानक फ़ॉर्मैट। NoWayOS हर वर्कस्पेस और हर सिस्टम इमेज के लिए एक बनाता है। देखें SBOM।
- Debug Probe
Raspberry Pi का USB-से-सीरियल एडैप्टर। Raspberry Pi 5 के डीबग कनेक्टर पर यह बूट लॉग लाता है और टेस्ट इमेज लोड करता है।
- embedded-graphics
उन डिवाइसों के लिए एक Rust 2D ग्राफ़िक्स लाइब्रेरी, जिनमें ऑपरेटिंग सिस्टम का ग्राफ़िक्स स्टैक नहीं होता। NoWayOS का यूज़र इंटरफ़ेस इसी से ड्रॉ करता है।
- i.MX8
NXP का इंडस्ट्रियल Arm प्रोसेसर का परिवार, और NoWayOS का इच्छित प्रोडक्शन हार्डवेयर। अभी समर्थित नहीं।
- Kani
Rust के लिए एक मॉडल चेकर, जो एक सीमा तक के हर इनपुट के लिए गुणों को साबित करता है। NoWayOS इससे यह साबित करता है कि उसके मैसेज डिकोडर कभी पैनिक, ओवरफ़्लो या सीमा के बाहर रीड नहीं करते।
- Microkit
स्टैटिक seL4 सिस्टम के लिए seL4 Foundation का फ़्रेमवर्क, जो सिस्टम डिस्क्रिप्शन में घोषित प्रोटेक्शन डोमेन से बने होते हैं।
- Miri
Rust का एक इंटरप्रेटर, जो अपरिभाषित व्यवहार (undefined behaviour) पकड़ता है। NoWayOS इसे उन गिने-चुने क्रेट पर चलाता है जिन्हें
unsafeकोड की अनुमति है।- QEMU
एक ओपन सोर्स मशीन एमुलेटर। हर NoWayOS सिस्टम हार्डवेयर को छूने से पहले इसमें बूट होता है, और अपना आउटपुट खुद जाँचता है।
- Raspberry Pi 5
कम लागत वाला बोर्ड, जिसे NoWayOS अपने रेफ़रेंस हार्डवेयर के रूप में इस्तेमाल करता है।
- Rust
एक प्रोग्रामिंग भाषा, जिसका सेफ़ कोड मेमोरी-सेफ़्टी बग की गुंजाइश ख़त्म कर देता है। NoWayOS का अपना कोड पूरी तरह Rust में है।
- rust-sel4
seL4 Foundation का Rust सपोर्ट, जिसमें Microkit प्रोटेक्शन डोमेन लिखने का क्रेट भी शामिल है।
- rustls
Rust में लिखी एक TLS लाइब्रेरी। NoWayOS का TLS 1.3 क्लाइंट इसी पर, RustCrypto के साथ, बना है।
- SBOM
सॉफ़्टवेयर बिल ऑफ़ मटीरियल्स: किसी सॉफ़्टवेयर के हर कंपोनेंट और वर्शन की सूची। NoWayOS हर वर्कस्पेस और हर सिस्टम इमेज के लिए CycloneDX में एक SBOM बनाता है।
- Screen Compiler
NoWayOS का बिल्ड-टाइम टूल, जो समर्थित सबसेट में TSX में लिखी React स्क्रीन को NoWayOS के यूज़र इंटरफ़ेस के लिए Rust में बदलता है। सबसेट से बाहर की किसी भी चीज़ का अनुमान लगाने के बजाय यह उसे ठुकरा देता है।
- sDDF
seL4 Device Driver Framework: Microkit पर ड्राइवरों के लिए एक रेफ़रेंस डिज़ाइन, जो शेयर्ड-मेमोरी क्यू का इस्तेमाल करता है। NoWayOS की नेटवर्क क्यू इसी का पालन करती हैं।
- seL4
लगभग 10,000 लाइनों का एक माइक्रोकर्नेल, जिसकी देखरेख seL4 Foundation करता है, और जिसके पास विशिष्ट कॉन्फ़िगरेशन के लिए शुद्धता और सुरक्षा के मशीन-जाँचे प्रूफ़ हैं। NoWayOS इसी पर चलता है।
- sel4-config.txt
हर NoWayOS इमेज के बगल में लिखा जाने वाला रिकॉर्ड: उसका seL4 कॉन्फ़िगरेशन, और यह कि वह कॉन्फ़िगरेशन seL4 के पूरे हो चुके प्रूफ़ के दायरे में है या नहीं।
- Single Purpose OS
एक ऑपरेटिंग सिस्टम, जो एक डिवाइस के एक काम के लिए बना है, न कि कुछ भी चलाने के लिए बनाकर फिर एक चीज़ तक लॉक किया गया। तीन बातें इसे यह बनाती हैं: यह एक काम के लिए बना है (इसकी इमेज में एप्लिकेशन, उसके इस्तेमाल किए ड्राइवर और कर्नेल होते हैं, और कुछ नहीं); यह भीतर से सील है (हर हिस्सा अपने कम्पार्टमेंट में, सिर्फ़ उसी तक पहुँचता है जो उसे दिया गया है); और यह अपना हिसाब दिखाता है (भीतर क्या है, इसका सबूत साथ आता है)। यह कियोस्क मोड नहीं है, जो किसी कॉन्फ़िगरेशन से सुरक्षित सिस्टम को एक ऐप तक लॉक करता है। NoWayOS एक Single Purpose OS है: एक कंप्यूटर, जिसे और कुछ नहीं करना।
- smoltcp
Rust में एक TCP/IP स्टैक, जो चलते समय कोई मेमोरी एलोकेट नहीं करता। NoWayOS का नेटवर्क स्टैक इसी पर बना है।
- unsafe
Rust कोड, जिसकी मेमोरी सेफ़्टी कंपाइलर नहीं जाँच सकता। हर NoWayOS क्रेट में वर्जित है, सिवाय एक छोटी, रिव्यू की गई सूची के, जिसे जाँचें लागू करती हैं।