KataOS ، نظام تشغيل موجه نحو الأمان للأجهزة.
صدر الخبر أن أعلنت Google عن إصدار الكود المصدري لـ التطورات المتعلقة بالمشروع نظام كاتا، هدفه الخلق نظام تشغيل آمن للأجهزة المدمجة.
النظام يوفر الدعم للمنصات القائمة على معماريات RISC-V و ARM64. لمحاكاة تشغيل seL4 وبيئة KataOS على الأجهزة أثناء التطوير ، يتم استخدام إطار عمل Renode.
كتطبيق مرجعي ، تم اقتراح مجمع Sparrow للبرامج والأجهزة ، والذي يجمع بين KataOS والرقائق الآمنة القائمة على منصة OpenTitan. الحل المقترح حمن الممكن الجمع بين النواة نظام تشغيل تم التحقق منه منطقيًا مع مكونات أجهزة Root of Trust (RoT) التي تم إنشاؤها باستخدام منصة OpenTitan وبنية RISC-V.
بالإضافة إلى كود KataOS ، من المخطط فتح جميع مكونات Sparrow الأخرى ، بما في ذلك مكون الأجهزة ، في المستقبل.
كأساس لنظام التشغيل الجديد هذا ، اخترنا seL4 باعتباره microkernel لأنه يضع الأمان في المقدمة ومركزًا ؛ ثبت رياضيًا أنه آمن ، مع ضمان السرية والنزاهة والتوافر. من خلال إطار عمل seL4 CAmkES ، يمكننا أيضًا توفير مكونات نظام محددة بشكل ثابت وقابلة للتحليل. يوفر نظام KataOS نظامًا أساسيًا آمنًا يمكن التحقق منه يحمي خصوصية المستخدم لأنه من المستحيل منطقيًا أن تنتهك التطبيقات إجراءات حماية أمان أجهزة kernel ومكونات النظام الآمنة التي يمكن التحقق منها.
يتم تطوير المنصة مع وضع الرقائق في الاعتبار خاصة مصمم لتشغيل تطبيقات الخصوصية والتعلم الآلي تتطلب مستوى معينًا من الحماية وتضمن عدم وجود أعطال. الأنظمة التي تتعامل مع صور الأشخاص والتسجيلات الصوتية معطاة كمثال على هذه التطبيقات. يضمن استخدام التحقق من الموثوقية في KataOS أنه في حالة حدوث عطل في جزء واحد من النظام ، فإن هذا الفشل لا ينتشر إلى بقية النظام وعلى وجه الخصوص إلى النواة والأجزاء الحرجة.
هندسة معمارية تتفوق seL4 في الأجزاء المتحركة لإدارة موارد النواة في مساحة المستخدم وتطبيق نفس ضوابط الوصول لتلك الموارد مثل موارد المستخدم.
النواة الصغيرة لا تقدم تجريدات عالية المستوى خارج الصندوق لإدارة الملفات والعمليات واتصالات الشبكة وما شابه ، ولكنها توفر فقط الحد الأدنى من الآليات للتحكم في الوصول إلى مساحة العنوان الفعلية والمقاطعات وموارد المعالج. يتم تنفيذ التجريدات عالية المستوى وبرامج التشغيل للتفاعل مع الأجهزة بشكل منفصل أعلى النواة الدقيقة في شكل مهام على مستوى المستخدم. يتم تنظيم وصول مثل هذه المهام إلى الموارد المتاحة للنواة الدقيقة من خلال تعريف القواعد.
لمزيد من الحماية ، تم تطوير جميع المكونات باستثناء النواة الدقيقة مبدئيًا في Rust استخدام تقنيات البرمجة الآمنة التي تقلل من الأخطاء عند العمل مع الذاكرة ، مما يؤدي إلى مشاكل مثل الوصول إلى منطقة من الذاكرة بعد تحريرها ، وإلغاء الإشارة إلى المؤشرات الفارغة ، وتجاوز المخزن المؤقت.
أداة تحميل التطبيق في بيئة seL4 ، وخدمات النظام ، وإطار تطوير التطبيقات ، وواجهة برمجة التطبيقات للوصول إلى استدعاءات النظام ، ومدير العمليات ، وآلية تخصيص الذاكرة الديناميكية ، وما إلى ذلك. هم مكتوبون في Rust. بالنسبة للتجميع الذي تم التحقق منه ، يتم استخدام مجموعة أدوات CAmkES التي طورها مشروع seL4. يمكن أيضًا إنشاء مكونات CAmkES في Rust.
يتم توفير سلامة الذاكرة في الصدأ في وقت الترجمة عن طريق التحقق من المراجع ، وتتبع ملكية الكائن ، وعمر الكائن (النطاق) ، وكذلك عن طريق تقييم صحة الوصول إلى الذاكرة أثناء تنفيذ التعليمات البرمجية. يوفر الصدأ أيضًا حماية عدد صحيح من التدفق الزائد ، يتطلب تهيئة المتغيرات قبل الاستخدام ، ويفرض مفهوم المتغيرات والمراجع الثابتة بشكل افتراضي ، ويوفر كتابة ثابتة قوية لتقليل الأخطاء المنطقية.
أخيرًا للمهتمين ، يجب أن تعلم أن مكونات نظام KataOS مكتوبة باللغة Rust وتعمل على نواة seL4 microkernel ، والتي يتم توفير دليل رياضي على الموثوقية في أنظمة RISC-V ، مما يشير إلى أن الكود يتوافق تمامًا مع المواصفات المحدد في اللغة الرسمية.
رمز المشروع مفتوح بموجب ترخيص Apache 2.0 ، يمكنك الرجوع إلى مزيد من التفاصيل حوله في الرابط التالي.