जाँचें और सबूत

make ci क्या चलाता है और हर जाँच क्या दिखाती है, वे बुनियादी नियम जिनका हर क्रेट पालन करता है, किसी इमेज का seL4 रिकॉर्ड और बिल ऑफ़ मटीरियल्स कैसे पढ़ें, और गेट तेज़ कैसे बना रहता है।

NoWayOS कम दावे करता है, और हर एक के पीछे एक ऐसी जाँच है जिसे आप चला सकते हैं। यह पेज बताता है कि हर जाँच क्या दिखाती है, और क्या नहीं।

इन सबके लिए एक कमांड

make ci

make ci पूरा गेट है, जो क्रम से चलता है: सीक्रेट्स स्कैन, लिंट, टेस्ट, डॉक्यूमेंटेशन, डेमो, no_std बिल्ड, लाइसेंस और एडवाइज़री जाँचें, ग्लिफ़ एटलस, बिल ऑफ़ मटीरियल्स, फ़ज़िंग और Kani प्रूफ़, फिर सिस्टम जाँचें और QEMU बूट। कोई बदलाव तभी पास होता है जब हर चरण पास हो।

हर जाँच क्या दिखाती है

कमांड	यह क्या दिखाता है
`make test`	यूनिट, प्रॉपर्टी, डॉक और गोल्डन-इमेज टेस्ट: कोड वही करता है जो उसके टेस्ट कहते हैं, और हर स्क्रीन ठीक वैसी ड्रॉ होती है जैसी स्वीकृत है
`make lint`	rustfmt और clippy, चेतावनियों को त्रुटि मानकर
`make nostd`	हर डिवाइस क्रेट बेयर मेटल (`aarch64-unknown-none`) के लिए, बिना स्टैंडर्ड लाइब्रेरी के, बिल्ड होता है
`make deny`	वह बेसलाइन जिसे हर वर्कस्पेस को बनाए रखना है, फिर cargo-deny: लाइसेंस, स्रोत, प्रतिबंधित क्रेट और ज्ञात एडवाइज़री
`make secrets`	पूरा ट्री और हर कमिट, कुंजियों और क्रेडेंशियल्स के लिए ऑफ़लाइन स्कैन
`make fuzz`	हर फ़ज़ टार्गेट, libFuzzer से बिल्ड करके जनरेट किए गए इनपुट पर चलाया गया, हर एक `FUZZ_SECONDS` (10 s) तक
`make kani`	Kani के बाउंडेड प्रूफ़: कि हर रिकॉर्ड डिकोडर सबसे लंबे रिकॉर्ड तक के किसी भी इनपुट के लिए कभी पैनिक, ओवरफ़्लो या सीमा के बाहर रीड नहीं करता, म्यूटेशन जाँचों के साथ, जो दिखाती हैं कि हर प्रूफ़ फ़ेल हो सकता है
`make unsafe-audit`	`unsafe` कोड सिर्फ़ वहीं है जहाँ स्वीकृत सूची इसकी अनुमति देती है
`make pds-miri`	Miri उन क्रेट के टेस्ट चलाता है जिन्हें `unsafe` की अनुमति है, अपरिभाषित व्यवहार की जाँच करते हुए
`make sbom`	हर वर्कस्पेस के लिए एक CycloneDX बिल ऑफ़ मटीरियल्स
`make image-sbom SYSTEM=NAME`	एक इमेज और उसका बिल ऑफ़ मटीरियल्स: कर्नेल, लोडर, मॉनिटर और हर प्रोटेक्शन डोमेन, हर एक के क्रेट और उनके हैश के साथ
`make sel4-config-check`	रिकॉर्ड में दर्ज seL4 वेरिफ़िकेशन स्थिति वही है जो पिन किए गए Microkit SDK के लिए है
`make qemu-test-all`	हर सिस्टम QEMU में, अपनी सूची के हर कॉन्फ़िगरेशन में, बूट होता है और वही प्रिंट करता है जो उसकी एक्सपेक्ट फ़ाइल कहती है

बाउंडेड प्रूफ़ इनपुट के एक तय आकार तक के प्रूफ़ हैं, हर उस इनपुट के लिए नहीं जो कभी भी हो सकता है। फ़ज़िंग क्रैश ढूँढ़ती है; यह नहीं दिखा सकती कि कोई क्रैश नहीं है। टेस्ट वही मामले दिखाते हैं जिन्हें वे टेस्ट करते हैं। हर एक जो दिखाता है, उसके लिए रखने लायक है।

वे बुनियादी नियम जिनका हर क्रेट पालन करता है

ये हर वर्कस्पेस में लिंट और जाँचें हैं, दिशानिर्देश नहीं:

कोई unsafe नहीं, सिवाय क्रेट और फ़ाइलों की एक छोटी, स्वीकृत सूची के, जो सीधे हार्डवेयर या मेमोरी तक पहुँचती हैं। सूची में कुछ जोड़ने के लिए एक स्पष्ट कारण और रिव्यू ज़रूरी है।
बाहरी इनपुट पर कोई पैनिक नहीं: लाइब्रेरी कोड में न unwrap, न expect, न panic!, न बिना जाँच की इंडेक्सिंग या अंकगणित, और किसी लिंट का हर अपवाद अपना कारण बताता है।
डिवाइस क्रेट no_std हैं और कोई मेमोरी एलोकेट नहीं करते। रिलीज़ बिल्ड ओवरफ़्लो जाँचें बनाए रखते हैं, और पैनिक होने पर हिस्सा चलता रहने के बजाय रुक जाता है।
पार्सर बहुत बड़े इनपुट को कॉपी करने से पहले ही ठुकरा देते हैं, टाइप्ड त्रुटियाँ लौटाते हैं, और उनके प्रॉपर्टी टेस्ट और एक फ़ज़ टार्गेट होता है।
कहीं भी कोई सीक्रेट नहीं, डेवलपमेंट कुंजियाँ भी नहीं। टेस्ट कुंजियाँ टेस्ट चलते समय बनाई जाती हैं, और कभी स्टोर नहीं की जातीं।

किसी इमेज के रिकॉर्ड पढ़ना

हर इमेज build/BOARD/SYSTEM/ में लिखी जाती है, अपने बगल में दो रिकॉर्ड के साथ।

sel4-config.txt इमेज, उसके हैश, बोर्ड, Microkit SDK और कर्नेल का नाम बताता है, फिर बताता है कि seL4 के प्रूफ़ के मुक़ाबले इमेज कहाँ खड़ी है, हर कारण के लिए एक status: लाइन, और हर उस कर्नेल विकल्प की सूची देता है जो इसे तय करता है, सत्यापित कॉन्फ़िगरेशन के मान के बगल में। डीबग कर्नेल एक डेवलपमेंट बिल्ड है। मल्टी-कोर या मिक्स्ड-क्रिटिकैलिटी कर्नेल, या ऐसा बोर्ड जो seL4 की सूची में नहीं, seL4 के प्रूफ़ के दायरे से बाहर है। जो कर्नेल हर विकल्प से मेल खाता है, उसे भी कभी “सत्यापित” नहीं कहा जाता: रिकॉर्ड तथ्य देता है और बात वहीं छोड़ देता है।

sbom.cdx.json इमेज का CycloneDX सॉफ़्टवेयर बिल ऑफ़ मटीरियल्स है: इमेज किन चीज़ों से बनी है, हर प्रोटेक्शन डोमेन के हर क्रेट तक, हर एक अपने sha256 के साथ।

गेट को तेज़ बनाए रखना

प्रूफ़ और फ़ज़िंग के पूरे सेट में लंबा समय लगता है, इसलिए रोज़ का make ci Kani, फ़ज़िंग और Miri सिर्फ़ वहीं चलाता है जहाँ तक कोई बदलाव पहुँचता है। यह बदलाव को उस पर निर्भर हर क्रेट तक फ़ॉलो करता है, और हर वह जाँच छोड़ देता है जिसके इनपुट उसके पिछली बार पास होने के बाद से नहीं बदले। make ci CI_SCOPE=full इनमें से हर एक चलाता है, बिना किसी कैश के; make kani, make fuzz और make pds-miri हमेशा पूरे चलते हैं।

Kani सबसे ज़्यादा संसाधन खाने वाला चरण है: हर प्रूफ़ जॉब को लगभग 10 GB मेमोरी दी जाती है, और KANI_JOBS तय करता है कि एक साथ कितने चलें। अगर make kani की मेमोरी ख़त्म हो जाए, तो Podman की वर्चुअल मशीन को ज़्यादा मेमोरी दें, या KANI_JOBS=1 सेट करें।