فلسفة الأمان (User Space Flow)
seL4 مُثبتة رياضياً (Mathematically Proven) بأنها آمنة تماماً وخالية من الثغرات. لذلك، إضافة أي منطق لإدارة صلاحيات الملفات داخل النواة سيزيد من تعقيدها ويُهدد هذا الإثبات الرياضي. بدلاً من ذلك، نستخدم النواة فقط لتمرير الرسائل (IPC)، ونبني نظام الصلاحيات بالكامل كحاوية معزولة في User Space! نواة مثبتة رياضياً: دورها يقتصر على تأمين قنوات الاتصال (IPC) بصرامة، ولا تفهم معنى "ملف" أو "صلاحية".
مخرجات الحاوية الحية
تشريح تذكرة الأمان (PolicyBadge)
كيف يتم دمج (Packing) هوية التطبيق، الصلاحيات، وهاش المسار في 64-bit واحدة لتسريع التحقق (O(1) Verification).
0x04B20200A59F123Cimpl PolicyBadge {
pub fn new(app_id: u16, permission: Permission, path_hash: u32) -> Self {
Self { app_id, permission, path_hash }
}
// ضغط البيانات في كلمة 64-bit واحدة
pub fn to_badge_word(&self) -> u64 {
((self.app_id as u64) << 48) |
((self.permission as u8 as u64) << 32) |
(self.path_hash as u64)
}
}أوامر الاستدعاء (Message Tags)
الوظائف والمهام الأساسية
مصدر الثقة الأمني الوحيد (Single Trusted Authority)
تعمل كـ Trusted Authority مركزي — المصدر الوحيد في النظام المخوّل بإصدار تذاكر الأمان. لا يمكن لأي تطبيق الوصول لـ FS_Vault بدون الحصول على Badge صادر منها أولاً.
إدارة الصلاحيات في الـ User Space
نظراً لأن نواة seL4 مثبتة رياضياً (Mathematically Proven) بأنها آمنة، فلا حاجة لتعقيد النواة بإدارة الصلاحيات. تتم إدارة جميع السياسات في الـ User Space عبر هذه الحاوية.
توليد تذاكر الأمان (Security Token Generation)
تُولّد PolicyBadge مُشفَّرة تحمل هوية التطبيق (app_id) وصلاحياته (Permission) وهاش المسار المسموح به (FNV-1a). تُعاد كرقم 64-bit واحد يحمل كل هذه المعلومات مضغوطة.
ترميز الصلاحيات في 64-bit (Badge Word Encoding)
تُرمّز كل صلاحية في كلمة 64-bit واحدة: الـ 16 bit العليا = app_id | الـ 8 bits التالية = نوع الصلاحية | الـ 32 bit السفلى = hash المسار. هذا يجعل التحقق من الـ Badge عملية بسيطة وسريعة جداً.
تشفير المسارات بخوارزمية FNV-1a
تستخدم خوارزمية FNV-1a 32-bit لتحويل مسارات الملفات (مثل /home/user) إلى أرقام hash ثابتة وفريدة. يجب أن يتطابق الـ hash بين ما تُصدره auth وما تتحقق منه FS_Vault لقبول أي طلب.
إدارة الذاكرة المتقدمة عبر Talc Allocator
تستخدم مكتبة talc و spin لتوفير Global Allocator بذاكرة ثابتة حجمها 256KB. يوفر Talc أداء عالي واستهلاك قليل جداً بدون الحاجة إلى نظام تشغيل، مما يناسب بيئة الـ User Space بشكل مثالي.
إدارة Capability Slots الأمنية
تعتمد على استقبال الطلبات مباشرة من التطبيقات وتتخاطب مع FS_Vault ضمن دورة تأمين Capability Slots لتمرير التوثيق.
رفض الطلبات المجهولة (Unknown Request Rejection)
أي أمر خارج النطاق المعروف (عدا 0x100) يُرفض فوراً بـ MessageTag::Err. هذا يحمي النظام من أي محاولة للوصول عبر أوامر غير موثقة أو هجمات.
توثيق الملفات البرمجية
الملف الرئيسي لحاوية Auth_Vault. يحتوي على نقطة الدخول _start التي تُفوّض إلى rust_main، وحلقة الخدمة التي تستقبل طلبات التوثيق وتُولّد PolicyBadge مُشفَّرة.
Talc::new(...) مخصص لـ VAULT_HEAP (256KB)0x100 (Request Token)reply.mr[1] = badge.to_badge_word()ملف إعداد حزمة auth. يُعرّف 5 اعتماديات أساسية — تشمل talc و spin لتخصيص الذاكرة، و security-policy لسياسات الأمان.
auth (v0.1.0)لتخصيص الـ Heap بفعالية في بيئة no_stdpath = "../../libs/security-policy"المكتبات والاعتمادات (Dependencies)
sel4-sys
ربط المستوى المنخفض مع نواة seL4. تُوفر نداءات النظام اللازمة للتواصل مع الـ Kernel فقط للمهام الأساسية.
ipc-sync
مكتبة داخلية لتوحيد بناء هياكل IpcMessage ولف عمليات Receiver.serve().
talc
مكتبة OOM-safe، عالية الأداء وفعالة للـ Memory Allocation في بيئات الأنظمة المدمجة بدون قيود.
spin
تستخدم لتوفير أقفال آمنة بدون الحاجة لخيوط النواة (Thread OS)، مما يسمح باستخدام Talc بأمان.
security-policy
تُعرّف هيكل PolicyBadge ودالة hash_path() بخوارزمية FNV-1a 32-bit.