الإثبات الرياضي بدل الثقة
كل نظام تشغيل نستخدمه اليوم يحمل تراكمات عقود. نحن نبدأ من نقطة مختلفة جذرياً.
المشكلة في حجم الثقة
في نظام تشغيل تقليدي، مكوّن صغير مثل تعريف طابعة قد يعمل بصلاحيات النواة. ثغرة واحدة فيه تفتح الباب للسيطرة الكاملة. الحل التقليدي كان دائماً: اختبار أكثر، تدقيق أكثر. لكن الاختبار لا يستطيع إثبات غياب الخطأ، يستطيع فقط إثبات أنك لم تجده حتى الآن.
البديل: الإثبات الرياضي
هيروبان مبني على نواة seL4 — نواة صُممت بفلسفة مختلفة: النواة تفعل شيء واحد فقط: العزل. خضعت هذه النواة لإثبات رياضي شامل يُثبت أن الكود يطابق مواصفاته الأمنية بشكل قاطع ومستحيل اختراقه هيكلياً.
انعدام الثقة الافتراضية
معظم الاختراقات تحدث بسبب منح صلاحيات غير ضرورية. في هيروبان: لا ثقة افتراضية لأي مكوّن. كل شيء معزول بصلاحيات محددة جبرياً (Capabilities)، لا يمكن تجاوزها بأي حيلة برمجية.
نحن نبني بعناية، خطوة إثبات رياضي في كل مرة، لا سباقاً نحو إطلاق سريع.