الفحوص والأدلة

ما يشغّله make ci وما يُظهره كل فحص، والقواعد الأساسية التي تلتزمها كل حزمة، وكيف تقرأ سجل seL4 وقائمة المكونات لأي صورة، وكيف تبقى البوابة سريعة.

لا يقدّم NoWayOS إلا ادعاءات قليلة، ويسند كلًّا منها بفحص يمكنك تشغيله. تشرح هذه الصفحة ما يُظهره كل فحص، وما لا يُظهره.

أمر واحد لكل شيء

make ci

make ci هو البوابة كلها، تُشغَّل بالترتيب: مسح الأسرار، والتدقيق (lints)، والاختبارات، والتوثيق، والعرض التوضيحي، وبناء 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 ثوانٍ) لكل منها
`make kani`	براهين Kani المحدودة: أن كل مفكك للسجلات لا ينهار ولا يفيض ولا يقرأ خارج الحدود أبدًا لأي مدخل حتى طول أطول سجل، مع فحوص طفرات تُظهر أن كل برهان قادر على الفشل
`make unsafe-audit`	لا تظهر شيفرة `unsafe` إلا حيث تسمح القائمة المعتمدة
`make pds-miri`	يشغّل Miri اختبارات الحزم المسموح لها بـ `unsafe`، بحثًا عن السلوك غير المعرَّف
`make sbom`	قائمة مكونات بصيغة CycloneDX لكل مساحة عمل
`make image-sbom SYSTEM=NAME`	صورة وقائمة مكوناتها: النواة، والمُحمِّل، و monitor، وكل نطاق حماية، مع الحزم في كلٍّ منها وقيم التجزئة الخاصة بها
`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.