एक सिस्टम के हिस्से कैसे जुड़ते हैं

हर NoWayOS डिवाइस एक सिस्टम है: हिस्सों का एक तय समूह, जिसे बिल्ड होने से पहले घोषित किया जाता है, और जिसका हर हिस्सा seL4 के ज़रिए बाकी हिस्सों से अलग सील किया जाता है। रन टाइम पर कुछ भी नहीं जोड़ा जाता। यह पेज इसके टुकड़ों को, और उनके आपस में जुड़ने के तरीके को समझाता है।

प्रोटेक्शन डोमेन

प्रोटेक्शन डोमेन किसी सिस्टम का एक हिस्सा है: अपनी मेमोरी वाला एक प्रोग्राम, जिसके पास सिर्फ़ वही कैपेबिलिटी होती हैं जो उसे दी गई हैं। seL4 में कैपेबिलिटी एक ऐसा टोकन है जिसकी जालसाज़ी नहीं की जा सकती, जो एक कर्नेल ऑब्जेक्ट और उस पर मिले अधिकारों को नामित करता है, जैसे किसी एक दरवाज़े का कीकार्ड। कोई प्रोटेक्शन डोमेन ऐसी किसी भी चीज़ को नहीं छू सकता जिसे उसकी कैपेबिलिटी नामित नहीं करतीं, और seL4 इसे लागू करता है।

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

सिस्टम डिस्क्रिप्शन

Microkit सिस्टम डिस्क्रिप्शन (systems/NAME.system, एक XML फ़ाइल) पूरे सिस्टम को घोषित करता है: हर प्रोटेक्शन डोमेन, उसकी प्रायोरिटी, बजट और स्टैक के साथ; हर मेमोरी रीजन और यह कि उसे कौन मैप करता है; हर चैनल; हर इंटरप्ट।

• डिस्क्रिप्शन डिवाइसों के नाम लेते हैं, कभी पते नहीं: phys_addr="@NAME"। पते platforms/ में बोर्ड की फ़ाइल से आते हैं, हर एक अपने स्रोत के साथ, इसलिए वही डिस्क्रिप्शन QEMU के लिए भी बिल्ड होता है और Raspberry Pi 5 के लिए भी।
• चैनल दो प्रोटेक्शन डोमेन को जोड़ते हैं, नोटिफ़िकेशन (बिना डेटा के सिग्नल, जिनमें इंटरप्ट भी शामिल हैं) और प्रोटेक्टेड प्रोसीजर कॉल (ज़्यादा प्रायोरिटी वाले हिस्से में सिंक्रोनस कॉल) के लिए।

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

ग्रांट्स फ़ाइल

हर डिस्क्रिप्शन के बगल में, systems/NAME.grants वह सब कुछ सूचीबद्ध करती है जो सिस्टम देता है, प्रति लाइन एक तथ्य: प्रायोरिटी, बजट, मेमोरी, डिवाइस, इंटरप्ट और चैनल। अगर दोनों किसी भी दिशा में मेल न खाएँ, तो बिल्ड फ़ेल हो जाता है।

हर प्रोटेक्शन डोमेन का एक रोल भी होता है (ui, input, broker, display, driver, network, security, storage, update, app, supervisor, watchdog, clock या test), और बिल्ड ऐसी ग्रांट ठुकरा देता है जो उसके रोल को कभी नहीं मिलनी चाहिए। किसी यूज़र इंटरफ़ेस को ग़लती से नेटवर्क डिवाइस नहीं थमाया जा सकता, और कोई टेस्ट उपकरण चुपके से किसी प्रोडक्ट में नहीं घुस सकता।

टाइप्ड मैसेज

प्रोटेक्शन डोमेन टाइप्ड मैसेज के ज़रिए बात करते हैं: फ़िक्स्ड-साइज़, वर्शन वाले रिकॉर्ड, जिनका लेआउट स्पष्ट होता है, और जो शेयर्ड मेमोरी पर सिंगल-प्रोड्यूसर, सिंगल-कंज़्यूमर रिंग से भेजे जाते हैं।

• पहले कॉपी, फिर जाँच। रिसीवर हर रिकॉर्ड को वैलिडेट करने से पहले शेयर्ड मेमोरी से बाहर कॉपी करता है, ताकि भेजने वाला जाँच और इस्तेमाल के बीच उसे बदल न सके (वह बग जिसे डबल-फ़ेच कहते हैं)।
• डिकोडर पैनिक नहीं कर सकते। हर डिकोडर किसी भी ग़लत बने इनपुट के लिए टाइप्ड त्रुटि लौटाता है, और उसके बाउंडेड Kani प्रूफ़ और एक फ़ज़ टार्गेट हैं।
• हर पक्ष का अपना व्यू है। प्रोड्यूसर और कंज़्यूमर रिंग को अलग-अलग मेमोरी व्यू से देखते हैं, और साझा इंडेक्स acquire और release ऑर्डरिंग का इस्तेमाल करते हैं।

इनपुट

एप्लिकेशन को कैनॉनिकल इनपुट इवेंट दिखते हैं, यानी की, पॉइंटर की हलचल और टच, जो स्क्रीन के हिसाब से जाँचे जाते हैं और जिनकी दर सीमित होती है। उन्हें कभी USB या कोई और डिवाइस प्रोटोकॉल नहीं दिखता; इनपुट पाथ उन्हें अपने अलग प्रोटेक्शन डोमेन में पार्स करता है, हर बाइट को शत्रु मानकर।

फ़ॉल्ट, सुपरवाइज़र और फ़ेल-सेफ़ स्थिति

जब कोई प्रोटेक्शन डोमेन ऐसा कुछ करता है जिसकी seL4 अनुमति नहीं देता, या पैनिक करता है, तो seL4 उसे रोक देता है और उसके पैरेंट को फ़ॉल्ट की रिपोर्ट करता है।

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

मेमोरी और समय

• मेमोरी इमेज बिल्ड होते समय ही तय हो जाती है। डिवाइस कोड कोई मेमोरी एलोकेट नहीं करता: हर बफ़र और क्यू का एक तय आकार है, nowayos-bounded से। एकमात्र अपवाद, TLS क्लाइंट, अपने ख़ुद के एक तय एरीना में काम करता है।
• दो तरह का समय, जो कभी आपस में नहीं मिलता। मोनोटोनिक टाइम बूट से गिना जाता है और कभी पीछे नहीं जाता; हर टाइमआउट इसी का इस्तेमाल करता है। वॉल-क्लॉक टाइम, यानी तारीख़ और दिन का समय, एक प्रमाणीकृत स्रोत से आता है। ये अलग-अलग Rust टाइप हैं, इसलिए जहाँ एक चाहिए, वहाँ दूसरा पास नहीं किया जा सकता।

अपने सिस्टम बनाना

आपके प्रोडक्ट के अपने सिस्टम और प्रोटेक्शन डोमेन उनकी अपनी रिपॉज़िटरी में रहते हैं, nowayos के बगल में, कभी उसके भीतर नहीं। उस रिपॉज़िटरी की Makefile SYSTEM_REPO := $(CURDIR) सेट करती है और NoWayOS के make फ़्रैगमेंट शामिल करती है:

SYSTEM_REPO := $(CURDIR)
include ../nowayos/tools/make/container.mk
include ../nowayos/tools/make/system.mk

इसके बाद make image, make qemu-test, make qemu-test-all और जाँचें उसके systems/ और pds/ पर काम करती हैं, NoWayOS के डेव कंटेनर, बोर्ड फ़ाइलों, ग्रांट नियमों और जाँचों के साथ। वेरिएबल tools/make/system.mk की शुरुआत में दर्ज हैं। Showcase ठीक इसी तरह बिल्ड होता है।