المصطلحات، بلغة عربية واضحة.

جعل جهاز عام الأغراض أكثر أمانًا بتغيير إعداداته. فالميزات تبقى موجودة، وخلل واحد قد يتجاوز كل الإعدادات.

بناء جهاز لا يستطيع فعل الأمور الخطرة لأنها لم تُبنَ فيه قط. وهذا نهج NoWayOS.

اختبار محلل بملايين المدخلات المولّدة حتى يُسقطه أحدها أو يكسر أحد فحوصه. ولكل محلل للمدخلات الخارجية في NoWayOS هدف لاختبار التشويش.

نظام يحاول الوصول إلى ما لم يُمنح له، ويجب أن يوقفه seL4. ويجب أن يفشل متغيّر وُسّع فيه إذن عمدًا، وهو ما يُثبت أن الاختبار قادر على الفشل.

خط مرسوم مسبقًا، وقت البناء، في صور لمحارفه، فيرسم الجهاز النص دون أن يحلل ملف خط أبدًا.

رفض الجهاز تشغيل أي برمجيات لم يوقّعها صانعه. مخطط له في NoWayOS على العتاد الإنتاجي؛ ولم يُبنَ بعد.

بدء التشغيل من حالة انقطاع الطاقة، بخلاف إعادة التعيين. ولا يعيد جهاز NoWayOS من حالة الأمان عند العطل إلا إقلاع بارد.

القاعدة التي تقضي بنسخ الرسالة خارج الذاكرة المشتركة قبل التحقق من صحتها، فلا يستطيع المرسل تغييرها بين الفحص والاستخدام. وهي تمنع الجلب المزدوج.

برهان على أن خاصيةً ما تصح لكل مدخل حتى حجم مُعلن. ويُثبت NoWayOS مفككات رسائله بهذه الطريقة، باستخدام Kani.

برهان رياضي، يتحقق منه الحاسوب، على أن البرمجيات تفي بمواصفاتها. ويملكه seL4 لإعدادات محددة. أما شيفرة NoWayOS الخاصة فتعتمد بدلًا من ذلك على Rust والعزل والاختبار والبراهين المحدودة.

إثبات الجهاز لخدمة بعيدة، بطريقة تشفيرية، أيَّ برمجيات بدأ تشغيلها. وهو يُظهر ما حُمِّل عند الإقلاع، لا كل ما حدث منذ ذلك الحين. مخطط له في NoWayOS على العتاد الإنتاجي؛ ولم يُبنَ بعد.

خلل تفحص فيه الشيفرة بيانات في الذاكرة المشتركة ثم تقرؤها مرة أخرى، ما يتيح للطرف الآخر تغييرها في الأثناء. وتمنعه قاعدة انسخ، ثم تحقق.

ما يدخله جهاز NoWayOS حين تتوالى الأعطال: لا يبقى قيد التشغيل إلا المشرف ومؤقت المراقبة، والعرض حيثما أمكن، حتى إقلاع بارد.

صورة الحاوية المثبّتة الإصدارات التي تحوي سلسلة أدوات NoWayOS كلها: سلاسل أدوات Rust، و Microkit SDK، و QEMU، وأدوات الفحص. ويعمل فيها كل هدف من أهداف make، فلا يحتاج جهازك إلا إلى Podman و make (و Python 3.11 للتحكم في Raspberry Pi 5).

خطأ مثل القراءة بعد نهاية مخزن مؤقت أو استخدام ذاكرة بعد تحريرها. وقد أفادت كلٌّ من Microsoft و Google بأن نحو 70% من أخطائها الأمنية الخطيرة من هذا النوع؛ و Rust الآمنة تستبعدها.

سجل ثابت الحجم ذو تخطيط صريح، يُمرَّر بين نطاقات الحماية عبر الذاكرة المشتركة ويُفحص عند استلامه. انظر انسخ، ثم تحقق.

كل ما يمكن للمهاجم أن يحاول استخدامه ضد جهاز ما: شيفرته، وخدماته، وواجهاته، ومدخلاته. والشيفرة الأقل والميزات الأقل تُبقيان منه قدرًا أقل.

في seL4، رمز لا يمكن تزويره يسمّي كائنًا واحدًا في النواة والحقوق الممنوحة عليه، مثل بطاقة دخول لباب واحد. ولا يستطيع نطاق الحماية أن يمسّ إلا ما تسمّيه صلاحياته.

ما يبلّغ عنه seL4 حين يفعل نطاق حماية شيئًا لا تسمح به النواة، أو ينهار. ويبقى الجزء متوقفًا حتى يتصرف معالج أعطاله.

كل ما يجب أن يكون صحيحًا كي تصح خاصية أمنية ما. وفي نظام NoWayOS: نواة seL4، ومُحمِّل Microkit و monitor الخاص به، ونطاقات الحماية التي تعتمد عليها تلك الخاصية.

في Microkit، اتصال مُعلن بين نطاقَي حماية، للإشعارات (إشارات بلا بيانات، ومنها المقاطعات) ولاستدعاءات الإجراءات المحمية.

مؤقت في العتاد يعيد تعيين اللوحة ما لم تغذّه البرمجيات. ونطاق حماية مؤقت المراقبة في NoWayOS لا يغذّيه إلا ما دام كل جزء آخر يستجيب لنبضاته.

نطاق الحماية الذي يتلقى أعطال الأجزاء الأخرى، ويبلغ عنها، ويعيد تشغيل النظام من بداية نظيفة.

systems/NAME.grants: كل ما يمنحه النظام، حقيقة واحدة في كل سطر: الأولويات، والميزانيات، والذاكرة، والأجهزة، والمقاطعات، والقنوات. ويفشل البناء إذا اختلف وصف النظام وملف الأذونات.

systems/NAME.expect: الأسطر التي يجب أن يطبعها النظام، بالترتيب، والنص الذي يُفشل الاختبار إذا ظهر في أي مكان. والملف نفسه يفحص النظام في QEMU وعلى Raspberry Pi 5.

جزء معزول واحد من نظام Microkit: برنامج له ذاكرته الخاصة، ولا يحمل إلا الصلاحيات الممنوحة له صراحةً. وهو الحجرات المعزولة في NoWayOS.

إعداد seL4 الذي يتضمن ميزانيات الجدولة وفتراتها، وهو ما يبنيه Microkit. وما زالت براهينه لمعمارية AArch64 قيد الإنجاز، ولذلك لا تقع اليوم أي صورة من صور NoWayOS ضمن براهين seL4 المكتملة.

نواة تُبقى أصغر ما يمكن، وتعمل برامج التشغيل والشبكات والشاشة خارجها، كلٌّ في حجرته الخاصة. و seL4 واحدة منها.

ملف XML في Microkit يُعلن كل نطاق حماية ومنطقة ذاكرة وقناة ومقاطعة في النظام. وهو التصميم الأمني للنظام، ويُراجَع أي تغيير عليه بوصفه كذلك.

وقت يُعدّ من الإقلاع، لا يُضبط أبدًا ولا يعود إلى الوراء أبدًا. وكل مهلة في NoWayOS تستخدمه، ولا يختلط أبدًا بـ وقت ساعة الحائط.

التاريخ والوقت من اليوم، من مصدر مُصادَق. ويُبقيه NoWayOS منفصلًا عن الوقت الرتيب، بوصفه نوعًا مختلفًا.

صيغة معيارية مفتوحة لقوائم مكونات البرمجيات. يكتب NoWayOS واحدة لكل مساحة عمل ولكل صورة نظام. انظر SBOM.

محوّل Raspberry Pi من USB إلى تسلسلي. وعلى موصل التصحيح في Raspberry Pi 5، ينقل سجل الإقلاع ويحمّل صور الاختبار.

مكتبة رسوميات ثنائية الأبعاد بلغة Rust للأجهزة التي لا تملك مكدس رسوميات من نظام تشغيل. وبها ترسم واجهة مستخدم NoWayOS.

عائلة معالجات Arm الصناعية من NXP، والعتاد المزمع استخدامه في إنتاج NoWayOS. غير مدعومة بعد.

مدقق نماذج للغة Rust يُثبت الخصائص لكل مدخل حتى حدٍّ معيّن. ويستخدمه NoWayOS لإثبات أن مفككات رسائله لا تنهار ولا تفيض ولا تقرأ خارج الحدود أبدًا.

إطار عمل مؤسسة seL4 لأنظمة seL4 الثابتة المبنية من نطاقات حماية مُعلنة في وصف النظام.

مفسّر للغة Rust يكشف السلوك غير المعرَّف. ويشغّله NoWayOS على الحزم القليلة المسموح لها بشيفرة unsafe.

محاكي أجهزة مفتوح المصدر. يُقلع فيه كل نظام من أنظمة NoWayOS، ويتحقق من مخرجاته، قبل أن يلمس العتاد.

اللوحة منخفضة التكلفة التي يستخدمها NoWayOS عتادًا مرجعيًا.

لغة برمجة تستبعد شيفرتها الآمنة أخطاء سلامة الذاكرة. وشيفرة NoWayOS الخاصة مكتوبة بلغة Rust بالكامل.

دعم Rust الذي تقدمه مؤسسة seL4، بما فيه الحزمة الخاصة بكتابة نطاقات حماية Microkit.

مكتبة TLS مكتوبة بلغة Rust. وعميل TLS 1.3 في NoWayOS مبني عليها، مع RustCrypto.

قائمة مكونات البرمجيات: قائمة بكل مكوّن وإصداره في برنامج ما. ويكتب NoWayOS واحدة بصيغة CycloneDX لكل مساحة عمل ولكل صورة نظام.

أداة NoWayOS التي تعمل وقت البناء وتحوّل شاشات React، المكتوبة بـ TSX ضمن مجموعة جزئية مدعومة، إلى Rust لواجهة مستخدم NoWayOS. وترفض كل ما يقع خارج المجموعة الجزئية بدلًا من تقريبه.

إطار seL4 لبرامج تشغيل الأجهزة (seL4 Device Driver Framework): تصميم مرجعي لبرامج التشغيل على Microkit، يستخدم طوابير في الذاكرة المشتركة. وطوابير الشبكة في NoWayOS تتبعه.

نواة مصغرة من نحو 10,000 سطر، تتولى صيانتها مؤسسة seL4، ولها براهين متحقق منها آليًا على صحتها وأمانها لإعدادات محددة. ويعمل NoWayOS عليها.

السجل المكتوب بجانب كل صورة من صور NoWayOS: إعداد seL4 الخاص بها، وما إذا كان ذلك الإعداد يقع ضمن براهين seL4 المكتملة.

نظام تشغيل مبني لمهمة واحدة يؤديها جهاز واحد، بدلًا من نظام مبني لتشغيل أي شيء ثم يُقيَّد بشيء واحد. وثلاثة أمور تجعله كذلك: أنه مبني لمهمة واحدة (تحوي صورته التطبيق، وبرامج التشغيل التي يستخدمها، والنواة، ولا شيء غير ذلك)؛ وأنه معزول من الداخل (كل جزء في حجرته الخاصة، لا يصل إلا إلى ما مُنح له)؛ وأنه يُظهر أدلّته (تأتي معه الأدلة على ما بداخله). وهو ليس وضع الكشك، الذي يقيّد نظامًا آمنًا بحكم الإعدادات بتطبيق واحد. NoWayOS هو Single Purpose OS: حاسوب لا يشغله شيء آخر.

مكدس TCP/IP بلغة Rust لا يحجز أي ذاكرة أثناء عمله. ومكدس الشبكة في NoWayOS مبني عليه.

شيفرة Rust لا يستطيع المترجم فحص سلامة ذاكرتها. وهي محظورة في كل حزمة من حزم NoWayOS باستثناء قائمة قصيرة مراجَعة تفرضها الفحوص.