الأمان
لا يعنيه إلا شأنه.
يستبعد جهاز NoWayOS ما لا تحتاجه مهمته، ويعزل ما يبقى في حجرات. تعرض هذه الصفحة ما يستند إليه ذلك، وما ثبت بالبرهان، وما لم يثبت بعد، وما يبقى عليك أن تُحسنه.
في هذه الصفحة
ما يُستبعد
تحوي صورة NoWayOS تطبيقها، وبرامج التشغيل التي يستخدمها ذلك التطبيق، والنواة المصغرة seL4. لا يوجد محرك متصفح ولا نظام نوافذ ولا صدفة أوامر ولا مدير حزم ولا حساب مستخدم: لم يُبنَ شيء منها فيه قط، فلا شيء منها موجود ليُستغل أو يُرقَّع أو يُساء ضبطه. صُمّم NoWayOS للحد من البرمجيات والخدمات غير الضرورية: إن لم تحتجها المهمة، فليست في الصورة.
هذا هو معنى الاسم: لا سبيل لاستغلال ما لم يُبنَ فيه أصلًا. إنه وصف لما هو غائب، لا وعد بأن شيئًا لن يسوء. فما بُني فيه قد يحوي أخطاء؛ والادعاء هو أن حجمه أقل بكثير، وأن الخطأ يبقى في حجرته.
تقييد نظام عام الأغراض يجعله آمنًا بحكم الإعدادات: فالميزات المحجوبة تبقى موجودة، وخلل واحد قد يتجاوز كل الإعدادات. أما NoWayOS فيسعى إلى أن يكون آمنًا بحكم البناء: فتلك الميزات لم تكن موجودة أصلًا.
كيف يُحتوى العطل
- يعمل كل جزء في نطاق حماية خاص به، بذاكرته الخاصة، ولا يحمل إلا الصلاحيات التي يمنحها وصف نظامه. ويفرضها seL4.
- كل إذن مُدرج في ملف أذونات النظام، ويفشل البناء إذا منح الوصف شيئًا لا يُدرجه الملف، أو العكس. توسيع أي إذن يُراجَع بوصفه تغييرًا أمنيًا.
- الرسائل بين الأجزاء سجلات ثابتة الحجم، تُنسخ خارج الذاكرة المشتركة قبل فحصها، فلا يستطيع المرسل تغيير السجل بعد اجتيازه الفحص.
- المدخلات عدائية حتى تُفحص. كل محلل للمدخلات الخارجية يخضع لاختبار التشويش ومبني بحيث لا ينهار أبدًا، وترى التطبيقات أحداث المفاتيح والمؤشر واللمس، ولا ترى أبدًا بروتوكولات الأجهزة.
- يوقف المشرف الجزء الذي يتعطل ويعيد تشغيل النظام من بداية نظيفة. وتكرار الأعطال يضع الجهاز في حالة الأمان عند العطل حتى إقلاع بارد.
ما تغطيه براهين seL4، وما لا تغطيه
seL4 نواة مصغرة من نحو 10,000 سطر، لها براهين متحقق منها آليًا على صحتها وأمانها. وهذه البراهين إنجاز نادر، وهي تصح على إعدادات محددة في منصات محددة. وهذا هو الموقف بدقة:
يعمل NoWayOS على النواة المصغرة seL4، التي لها براهين متحقق منها آليًا على صحتها وأمانها لإعدادات محددة على عتادنا؛ ويستخدم NoWayOS إعداد الحرجية المختلطة في seL4، الذي ما زالت براهينه قيد الإنجاز.
- المنصة: يُدرج الإعداد المتحقق منه لمعمارية AArch64 في seL4 كلًّا من Raspberry Pi 5 و i.MX8M Mini و Plus و Quad من NXP.
- الجدولة: يبني Microkit نواة الحرجية المختلطة (MCS) في seL4، التي ما زالت براهينها لمعمارية AArch64 قيد الإنجاز. ولذلك لا تقع اليوم أي صورة من صور NoWayOS ضمن براهين seL4 المكتملة.
- أنوية المعالج: البراهين مخصصة للنوى التي تعمل على نواة معالج واحدة. والصورة التي تستخدم عدة أنوية تقع خارجها، وتصرّح بذلك.
- ما فوق النواة: أدوات Microkit ونطاقات الحماية وبرامج التشغيل في NoWayOS لا تشملها براهين seL4. وتستند الثقة بها إلى Rust، والعزل، والمراجعة، والاختبار، والبراهين المحدودة الخاصة بـ NoWayOS.
تسجّل كل صورة إعدادها في ملف sel4-config.txt بجانبها. وإليك ما يقوله سجل نسخة تطوير من النظام hello عن نفسه:
system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list
وحتى الصورة التي تطابق نواتها كل خيار من خيارات الإعداد المتحقق منه لن توصف هنا بأنها “متحقق منها”. فالسجل يذكر الحقائق، والحقائق تكفي.
الأدلة، والأمر الخاص بكل منها
كل ادعاء في هذه الصفحة يأتي مع دليله، وكل دليل ينتج عن أمر يستطيع أي أحد تشغيله في حاوية التطوير. يشغّلها make ci بالترتيب، ويشغّل make ci CI_SCOPE=full كل برهان وكل هدف لاختبار التشويش؛ وتشرح صفحة الفحوص والأدلة كلًّا منها.
| الادعاء | الدليل | شغّله |
|---|---|---|
| كل إذن مدوَّن. | ملف الأذونات لكل نظام، يُفحص مقابل وصف نظامه في كل عملية بناء. | make qemu-test SYSTEM=hello |
| لا يستطيع أي جزء الوصول إلى ما لم يُمنح له. | اختبارات عزل تُجري مجساتها عمليات قراءة وكتابة غير ممنوحة، يجب أن يوقفها seL4، ومتغيّر وُسّع فيه إذن عمدًا، يجب أن يفشل. | make qemu-test SYSTEM=isolation-test |
| مفككات الرسائل تصمد أمام كل مدخل حتى حدٍّ معيّن. | براهين Kani لكل مفكك لسجلات الرسائل، مع فحوص طفرات تُظهر أن البراهين قادرة على الفشل. | make kani |
| محللات المدخلات الخارجية تصمد أمام المدخلات العدائية. | هدف لاختبار التشويش لكل محلل للمدخلات غير الموثوقة. وكل انهيار، بعد إصلاحه، يصبح اختبار تراجع. | make fuzz |
| الشيفرة غير الآمنة لا توجد إلا حيث اعتُمدت. | قائمة سماح بالحزم والملفات القليلة التي يجوز لها استخدامها، يفرضها make ci، مع تشغيل Miri على تلك الحزم. | make unsafe-audit |
| كل مكوّن معروف. | قائمة مكونات برمجيات بصيغة CycloneDX لكل مساحة عمل ولكل صورة نظام، مع قيمة التجزئة لكل مكوّن. | make image-sbom SYSTEM=hello |
| التراخيص والتحذيرات الأمنية مفحوصة. | cargo-deny على كل مساحة عمل: التراخيص، والمصادر، والحزم المحظورة، والتحذيرات الأمنية المعروفة. | make deny |
| لا أسرار في الشيفرة. | الشجرة وكل إيداع تُمسح دون اتصال بحثًا عن مفاتيح وبيانات اعتماد. | make secrets |
| إعداد seL4 لكل صورة مسجَّل. | ملف sel4-config.txt بجانب كل صورة، وفحص يتأكد من أن القيم المرجعية في السجل تطابق Microkit SDK المثبّت الإصدار. | make sel4-config-check |
اقرأ أدلة صورة واحدة
لا يلزمك بناء أي شيء لترى كيف تبدو الأدلة. هذه كلها لصورة حقيقية واحدة: ui-interactive، واجهة المستخدم القابلة للنقر، مبنية لـ QEMU في 1 نوفمبر 2026.
- قائمة مكونات برمجياتها (CycloneDX 1.5): 62 جزءًا، من نواة seL4 ومُحمِّل Microkit إلى كل حزمة في كل نطاق حماية، مع قيمة SHA-256 لكل منها.
- سجل إعداد seL4 الخاص بها: النواة التي تشغّلها، خيارًا خيارًا مقارنةً بالإعداد المتحقق منه في seL4، وبوضوح أين تقع خارج البراهين.
- وصف نظامها: كل نطاق حماية ومنطقة ذاكرة ومقاطعة وقناة، كما يبنيها Microkit.
- ملف أذوناتها: الأذونات نفسها مدوَّنة حقيقةً واحدة في كل سطر، ويفحصها البناء مقابل الوصف.
- الشاشة التي ترسمها، وتُقارن بكسلًا ببكسل بهذه الصورة المعتمدة كلما شُغّل اختبارها.
ما يبقى مسؤوليتك
NoWayOS منصة، لا منتج حاصل على شهادة. فالجهاز الآمن يعتمد أيضًا على طريقة نشره وتشغيله، وهذا الجزء يعود إلى من يبنيه ويشغّله.
- الأمن المادي. جهاز يُوصَل بمنافذه أو يد على كابل الطاقة يمكن أن يُخرج الجهاز من الخدمة. والهياكل والمنافذ والطاقة جزء من تصميم المنتج المبني على NoWayOS.
- ما يمنحه كل نظام. يتحقق NoWayOS من توافق النظام وملف أذوناته. أما ما إذا كانت تلك الأذونات مناسبة للمهمة فقرار تصميمي، وينبغي مراجعته على هذا الأساس.
- الشبكات والأنظمة الخلفية. لا يتصل الجهاز إلا بالوجهات التي يسمح بها نظامه. وما تفعله تلك الخدمات بما تتلقاه، فتأمينه مسؤوليتها.
- المفاتيح والتحديثات. التحديثات الموقّعة التي تتراجع بأمان مصمَّمة، لكنها لم تُبنَ بعد. ومن يحتفظ بمفاتيح التوقيع، وكيف يُعتمد الإصدار، قرار تشغيلي.
- الشهادات. المنتجات الخاضعة للتنظيم التي تعمل على NoWayOS تحمل شهاداتها الخاصة. صُمّم NoWayOS لتوفير الأدلة التي تحتاجها؛ لكنه هو نفسه غير حاصل على شهادة.
ما لم يُبنَ بعد
- الإقلاع الآمن والتصديق عن بعد من شأن العتاد الإنتاجي الذي يملك جذر ثقة في العتاد. ولم يُبنَ أي منهما.
- التحديثات الموقّعة التي تُطبَّق على الجهاز. سجلات التحديث وفحوصها موجودة؛ أما المسار الذي يطبّق التحديث على الجهاز فليس موجودًا بعد.
- Raspberry Pi 5 لوحة تطوير، لا جهاز معزَّز الحماية. فمن يمسك بإحداها يستطيع استبدال برمجياتها، ووصول أجهزة USB إلى الذاكرة ليس مقيَّدًا عليها بعد.
كلمات لن تجدها هنا
لا نصف NoWayOS بأنه “غير قابل للاختراق” أو “محصن ضد العبث” أو “منيع تمامًا”، ولا ندّعي أن له “سطح هجوم معدومًا”. فلا شيء كذلك، ولو قلناه لكان من حقك أن تتوقف عن القراءة. الادعاءات في هذه الصفحة أصغر من ذلك، وكلٌّ منها يأتي مع دليله.
الإبلاغ عن ثغرة
يُرجى الإبلاغ عن أي ثغرة بصورة خاصة، عبر ميزة الإبلاغ الخاص عن الثغرات في GitHub من تبويب Security في المستودع، أو بالبريد الإلكتروني إلى security@nowayos.com، كما يوضح ملف SECURITY.md في كل مستودع، لا في بلاغ علني. ولأن كل جزء يعمل في حجرته الخاصة، فقد صُمّم النظام بحيث يبقى الخلل حيث هو ريثما يُعدّ الإصلاح.