QEMU में आपका पहला सिस्टम

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

hello बूट करें

make qemu-test SYSTEM=hello

यह hello सिस्टम बिल्ड करता है, उसकी ग्रांट्स जाँचता है, QEMU में seL4 को हेडलेस बूट करता है और देखता है कि वह क्या प्रिंट करता है। यह तब पास होता है जब हर वह लाइन जो सिस्टम को प्रिंट करनी है, क्रम से आ चुकी हो, और कुछ भी वर्जित न आया हो।

इसे खुद बूट करके देखने के लिए make qemu SYSTEM=hello चलाएँ। QEMU से बाहर निकलने के लिए Ctrl-A दबाएँ, फिर x।

किसी सिस्टम को परिभाषित करने वाली तीन फ़ाइलें

हर सिस्टम systems/ में तीन फ़ाइलें है, pds/ के Rust कोड के बगल में।

hello.system Microkit सिस्टम डिस्क्रिप्शन है: सिस्टम का हर प्रोटेक्शन डोमेन, मेमोरी रीजन, चैनल और इंटरप्ट। hello में एक प्रोटेक्शन डोमेन है, और कुछ नहीं:

<system>
 <protection_domain name="hello" priority="1" stack_size="0x10000">
 <program_image path="nowayos-hello.elf" />
 </protection_domain>
</system>

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

system demo
role hello app

pd hello priority=1 budget=1000 period=1000

hello.expect उन लाइनों की सूची है जो सिस्टम को क्रम से प्रिंट करनी हैं, और, ! के बाद, वह टेक्स्ट जो कहीं भी दिखते ही टेस्ट को तुरंत फ़ेल कर देता है:

NOWAYOS: rust pd starting
NOWAYOS: hello from rust

!MON|ERROR
!seL4(CPU
!panicked

यही एक्सपेक्ट फ़ाइल Raspberry Pi 5 पर, बोर्ड के सीरियल लॉग से, सिस्टम को जाँचती है।

खुद प्रोटेक्शन डोमेन

pds/hello/src/main.rs पूरा प्रोग्राम है। यह rust-sel4 के Microkit उदाहरण के न्यूनतम ढाँचे का पालन करता है: init शुरुआत में एक बार चलता है, और अगर सिस्टम उसे कोई चैनल देता, तो हैंडलर नोटिफ़िकेशन प्राप्त करता।

#![no_std]
#![no_main]

use sel4_microkit::{Handler, Infallible, debug_println, protection_domain};

#[protection_domain]
fn init() -> HelloPd {
 debug_println!("NOWAYOS: rust pd starting");
 debug_println!("NOWAYOS: hello from rust");
 HelloPd
}

struct HelloPd;

impl Handler for HelloPd {
 type Error = Infallible;
}

इसमें कोई हीप नहीं है (कोई भी एलोकेशन लिंक ही नहीं हो पाएगा), न unsafe, न कोई डिवाइस। प्रिंटिंग सिर्फ़ इसलिए काम करती है क्योंकि यह डीबग बिल्ड है: रिलीज़ कर्नेल में कोई डीबग कंसोल नहीं होता।

seL4 को किसी हिस्से को रोकते हुए देखें

make qemu-test SYSTEM=isolation-test

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

NOWAYOS: isolation-test: 2 of 2 forbidden accesses faulted and were contained; bystander still running

आज़माने के लिए और सिस्टम

इनमें से कोई भी make qemu-test SYSTEM=NAME से चलाएँ, या हर सिस्टम make qemu-test-all से।

यूज़र इंटरफ़ेस में क्लिक करके घूमें

make qemu SYSTEM=ui-interactive VNC=1

QEMU की स्क्रीन आपकी मशीन के localhost:5900 पर VNC के ज़रिए खोली जाती है, एक ऐसे पासवर्ड के साथ जो सिर्फ़ उसी रन के लिए प्रिंट किया जाता है। macOS पर vnc://localhost:5900 खोलें (Finder में: Go, Connect to Server) और डेमो स्क्रीन में क्लिक करके घूमें।

बिल्ड हर इमेज के बगल में क्या छोड़ता है

build/BOARD/SYSTEM/ में (इनके लिए build/qemu_virt_aarch64/hello/ वग़ैरह), loader.img के बगल में:

• sel4-config.txt: इमेज का seL4 कॉन्फ़िगरेशन, और यह कि वह seL4 के प्रूफ़ के दायरे में है या नहीं। डीबग बिल्ड साफ़ कहता है कि वह नहीं है। देखें सुरक्षा।
• sbom.cdx.json: इमेज के लिए एक CycloneDX सॉफ़्टवेयर बिल ऑफ़ मटीरियल्स: कर्नेल, लोडर, हर प्रोटेक्शन डोमेन और उसके भीतर के क्रेट, हर एक अपने हैश के साथ।
• इमेज में शामिल चीज़ों की लाइसेंस फ़ाइलें, जैसे फ़ॉन्ट और आइकन के लाइसेंस।