نُشرت مقالة علمية في اتصالات ACM ، أكتوبر 2018 ، المجلد 61 ، العدد 10 ، الصفحات 68−77 ، doi: 10.1145 / 3230627

في فبراير 2017 ، أقلعت طائرة هليكوبتر من مهبط طائرات بوينغ في أريزونا مع المهمة المعتادة: الطيران حول أقرب التلال. طار بشكل مستقل تماما. وفقًا لمتطلبات السلامة في إدارة الطيران الفيدرالية الأمريكية ، فإن الطيار لم يلمس الضوابط. لم تكن هذه هي الرحلة الأولى AH-6 ذاتية الحكم ، والتي تطلقها الشركة على الطيور الصغيرة غير المأهولة (ULB). لقد كان يطير مثل هذا لسنوات عديدة. ومع ذلك ، هذه المرة في منتصف الرحلة تعرضت لهجوم طائرة هليكوبتر السيبرانية. هاجم الكمبيوتر الموجود على متن البرنامج البرامج الضارة لكاميرا الفيديو ، وكذلك الفيروس الذي تم تسليمه عبر محرك الأقراص المحمول المصاب ، والذي تم إدراجه أثناء الصيانة. هدد الهجوم بعض الأنظمة الفرعية ، لكنه لم يؤثر على التشغيل الآمن للطائرة.

الأفكار الرئيسية

• يمكن تحجيم الأدلة الرسمية المستقاة من بنية برنامج microkernel تم التحقق منه إلى أنظمة حقيقية.
• مستويات مختلفة من الأمان والموثوقية داخل نفس النظام ممكنة ومرغوبة. ليس من الضروري ضمان أقصى درجة من الموثوقية للكود بأكمله.
• إعادة التصميم المعتادة وإعادة التجهيز كافية لرفع الأنظمة الحالية إلى مستوى الكود الموثوق به للغاية.

قد تعتقد أن الطيران العسكري يمكن أن يصد بسهولة مثل هذا الهجوم السيبراني. في الواقع ، نجح فريق من المحتالين المحترفين بتكليف من DARPA كجزء من برنامج لتطوير أنظمة كمبيوتر عسكرية موثوقة بدرجة عالية أنظمة سايبر العسكرية الحربية (HACMS) في عام 2013 في اختراق الإصدار الأول من برنامج ULB ، الذي تم تطويره في الأصل لضمان سلامة الرحلة ، وليس الحماية من الهجمات الإلكترونية. حصلت على المتسللين الفرصة لتحطم طائرة هليكوبتر أو الهبوط في أي مكان كما يحلو لهم. لذلك ، لا يمكن المبالغة في تقدير مخاطر حدوث مثل هذه الهجمات مع أحد الركاب على متن الطائرة ، وتشير محاولة قرصنة غير ناجحة في فبراير 2017 إلى بعض التغييرات الأساسية في البرنامج.

تشرح هذه المقالة هذه التغييرات والتكنولوجيا التي جعلتها ممكنة. هذه تقنية تم تطويرها كجزء من برنامج HACMS الذي يهدف إلى ضمان التشغيل الآمن للأنظمة الحرجة في بيئة إلكترونية معادية - وفي هذه الحالة ، العديد من المركبات المستقلة. تعتمد هذه التقنية على التحقق الرسمي من البرنامج - وهي برامج مزودة ببراهين رياضية يتم التحقق منها تلقائيًا وتعمل وفقًا لمواصفاتها. على الرغم من أن المقالة ليست مخصصة للطرق الرسمية نفسها ، إلا أنها تشرح كيفية استخدام التحقق من القطع الأثرية لحماية الأنظمة الحقيقية في الممارسة العملية.

ربما تكون النتيجة الأكثر إثارة للإعجاب في نظام HACMS هي أنه يمكن توسيع التكنولوجيا لتشمل الأنظمة الحقيقية الحالية ، مما يحسن بشكل كبير حمايتها من الهجمات السيبرانية. وتسمى هذه العملية "التحديث الأمني ​​الزلزالي" ، على غرار ترقيات المباني الزلزالية. علاوة على ذلك ، فإن معظم عملية إعادة الهندسة تم تنفيذها بواسطة مهندسي بوينج ، بدلاً من متخصصي التحقق الرسميين.


"الطيور" خلال رحلة تجريبية غير مأهولة

ليست كل برامج طائرات الهليكوبتر مبنية على نماذج رياضية وأدلة. مجال التحقق الرسمي ليس جاهزًا بعد لمثل هذا النطاق. ومع ذلك ، فقد أثبت برنامج HACMS أن التطبيق الاستراتيجي للطرق الرسمية على الأجزاء الأكثر أهمية في النظام العام يحسن بشكل كبير الحماية. يعمل نهج HACMS على الأنظمة التي يمكن فيها تحقيق ميزة الأمان المطلوبة من خلال فرض بحت على مستوى البنية. ويستند هذا إلى microkernel الذي تم التحقق منه من sel4 ، والذي سنتحدث عنه أدناه. إنه يضمن العزل بين الأنظمة الفرعية ، باستثناء قنوات الاتصال المحددة بوضوح والتي تخضع لسياسات أمان النظام. هذه العزلة مضمونة على مستوى البنية مع إطار CAmkES الذي تم التحقق منه لمكونات النظام. باستخدام لغات المجال المحددة من Galois Inc. CAmkES يتكامل مع أدوات تحليل الهندسة المعمارية من روكويل كولينز وجامعة مينيسوتا ، وكذلك مكونات البرامج الموثوقة للغاية.

تستند إنجازات HACMS إلى صديق مؤمن قديم لمهندس البرمجيات - التوحيد القياسي. الابتكار هو أن الأساليب الرسمية تثبت قابلية الملاحظة للواجهات وتغليف الوحدات الداخلية. يسمح هذا الالتزام المضمون بالوحدة النمطية للمهندسين الذين ليسوا خبراء في الطرق الرسمية (كما هو الحال في شركة Boeing) بإنشاء أنظمة جديدة أو حتى تحديث الأنظمة الحالية وتحقيق الاستقرار العالي. على الرغم من أن الأدوات لا توفر بعد دليلا كاملا على أمن النظام.

التحقق الرسمي

يعود دليل صحة البرامج إلى الستينيات على الأقل ، ولكن لفترة طويلة كانت فوائدها الحقيقية لتطوير البرمجيات محدودة النطاق والعمق. ومع ذلك ، في السنوات الأخيرة ، كان هناك عدد من الاختراقات المثيرة للإعجاب في التحقق الرسمي على مستوى الكود الخاص بالأنظمة الحقيقية ، بدءًا من برنامج التحويل البرمجي C CompCert الذي تم التحقق منه إلى نظام microLerner seL4 الذي تم التحقق منه (انظر المقالات العلمية حول هذا الموضوع) ونظام المؤتمرات الذي تم التحقق منه من CoCon ومجمع برنامج التحقق من CakeML ML والبرامج التي تم التحقق منها لإثبات نظريتي Milawa و Candle ، ونظام الملفات FFSQ الذي تم التحقق من سلامته ، ونظام توزيع IronFleet الذي تم التحقق منه ، وإطار عمل kernel المتوافق CertiKOS ، بالإضافة إلى أهميته النظريات الرياضية ، بما في ذلك مشاكل أربعة ألوان ، والدليل التلقائي لفرضية كبلر ونظرية Faith - Thompson حسب ترتيب فردي . كل هذه أنظمة حقيقية. على سبيل المثال ، يعد CompCert منتجًا تجاريًا ، حيث يتم استخدام seL4 microkernel في الطائرات الفضائية والطائرات بدون طيار ، كمنصة لإنترنت الأشياء ، وقد تم استخدام نظام CoCon في العديد من المؤتمرات العلمية الكبيرة.

هذه المشاريع التحقق تتطلب جهدا كبيرا. لإتاحة الوسائل الرسمية للجمهور ، يجب تقليل هذه الجهود. نوضح هنا كيف أن الجمع الاستراتيجي بين الطرق الرسمية وغير الرسمية والأتمتة الجزئية للطرق الرسمية وتطوير البرمجيات بعناية لزيادة فوائد المكونات المعزولة قد سمح لنا بزيادة كبيرة في موثوقية الأنظمة التي يكون حجمها الكلي وتعقيدها أكبر بكثير من تلك المذكورة أعلاه.

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

seL4

دعنا نبدأ بالأساس لبناء أنظمة موثوقة - نواة نظام التشغيل (OS). هذا هو الجزء الأكثر أهمية الذي يضمن موثوقية النظام بأكمله بطريقة فعالة من حيث التكلفة.

يوفر seL4 microkernel الحد الأدنى الذي تم التحقق منه رسميًا من آليات تطبيق الأنظمة الآمنة. على عكس النواة القياسية ، فهي عالمية بشكل هادف وبالتالي فهي مناسبة لتنفيذ عدد من سياسات الأمن ومتطلبات النظام.

أحد الأهداف الرئيسية لتطوير seL4 هو توفير عزلة قوية بين مكونات عدم الثقة المتبادلة التي تعمل على قمة النواة. يدعم عمله كمشرف ، على سبيل المثال ، لأنظمة تشغيل Linux بأكملها ، مع الاحتفاظ بها بمعزل عن المكونات الحساسة للأمان التي يمكن أن تعمل معًا ، كما هو مبين في الشكل 1. على وجه الخصوص ، تتيح هذه الوظيفة لمطوري النظام استخدام المكونات القديمة مع مخفي نقاط الضعف بجانب مكونات موثوقة للغاية.


شكل 1. العزلة والاتصالات التي تسيطر عليها في seL4

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

seL4 API

يوفر seL4 kernel مجموعة قليلة من آليات تطبيق الأنظمة الآمنة: التدفقات ، وإدارة القدرة ، ومساحات العنوان الافتراضية ، والاتصالات بين العمليات (IPC) ، والتشوير وتسليم المقاطعة.

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

تتفاعل مؤشرات الترابط وتزامنها عن طريق إرسال الرسائل من خلال "نقاط النهاية" للاتصال المتبادل. يمكن لمؤشر ترابط واحد لديه القدرة على الإرسال إلى نقطة النهاية المقابلة إرسال رسالة إلى مؤشر ترابط آخر لديه القدرة على تلقي نقطة النهاية هذه. توفر كائنات الإعلام التزامن عبر مجموعات من الإشارات الثنائية. يتم التحكم في ترجمة العنوان الظاهري بواسطة كائنات kernel التي تمثل أدلة الصفحات ، وجداول الصفحات ، وكائنات الإطار أو التجريدات الدقيقة على كائنات هندسة المعالج المقابلة. كل تيار له قدرة "VSpace" معينة ، والتي تشير إلى جذر شجرة كائنات ترجمة عنوان الدفق. تتم إدارة القدرات نفسها بواسطة kernel وتخزينها في كائنات kernel "CNodes" الموجودة في بنية الرسم البياني ، والتي تقوم بتعيين الارتباطات إلى كائنات لها حقوق وصول ، على غرار مقارنة جداول الصفحات الافتراضية مع العناوين الفعلية في الذاكرة. كل مؤشر ترابط لديه القدرة الخاصة به لتحديد الجذر CNode. مجموعة القدرات المتاحة من هذا الجذر ، نسميها "CSpace Stream". يمكن نقل القدرات من خلال نقاط النهاية مع نقل الوظيفة ، ويمكن أيضًا إعلان مشاركتها باستخدام CSpace المشترك. يوضح الشكل 2 هذه الكائنات النواة.


شكل 2. نواة الكائنات في نظام seL4 مع اثنين من المواضيع التي تتفاعل من خلال نقطة النهاية

دليل السلامة

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

يستخلص المفهوم الرفيع المستوى لسياسات التحكم في الوصول ملخصات من كائنات فردية وقدرات kernel ، ويجمع بدلاً من ذلك تكوين التحكم في الوصول للنظام باستخدام مجموعة من "الموضوعات" (المكونات) المجردة والصلاحيات التي يتمتع بها كل منهم على الآخرين (على سبيل المثال ، لقراءة البيانات وإرسال الرسائل) . في المثال في التين. 2 ، اكتسبت المكونات A و B السلطة على نقطة النهاية.

أثبت Sewell وزملاؤه أن سياسات التحكم في الوصول إلى seL4 تضمن احترام ميزات الأمان الأساسية اثنين: تقييد الامتياز والنزاهة.

تقييد السلطة يعني أن سياسة التحكم في الوصول هي تقريب آمن ثابت (لم يتغير) لإمكانيات محددة وكائنات kernel في النظام لأي حالة مستقبلية. تتضمن هذه الخاصية أنه بغض النظر عن كيفية تطور النظام ، لن يحصل أي مكون على سلطة أكثر مما تتوقعه سياسة التحكم في الوصول. في الشكل 2 ، لا تتمتع السياسة الخاصة بالمكون "ب" بوصول الكتابة إلى المكون "أ". وبالتالي ، لن يتمكن المكون "ب" من الحصول على هذا الوصول في المستقبل. تتضمن هذه الخاصية أن التفكير على مستوى السياسة هو تقريب آمن للتفكير حول الحالة المحددة للتحكم في الوصول في النظام.

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

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

يتضمن الدليل الإضافي في seL4 امتدادًا للصحة الوظيفية ، وبالتالي نظريات الأمان إلى المستوى الثنائي لبنية ARMv7 وملف تعريف وقت التشغيل الأسوأ للنواة ( 1 ، 2 ) ، وهو أمر ضروري للأنظمة في الوقت الفعلي. نواة seL4 متاحة للعديد من البنى: ARMv6 ، ARMv7 ARMv7a ، ARMv8 ، RISC-V ، Intel x86 و Intel x64. في الوقت الحالي ، اجتاز اختبار الجهاز على بنية ARMv7 لكدسة التحقق بأكملها ، وكذلك على ARMv7a مع ملحقات برنامج Hypervisor للصحة الوظيفية.

الأمن العمارة

يصف القسم السابق طرق البرمجة التي تخلق بواسطتها نواة seL4 أساسًا قويًا للأنظمة الموثوقة. تشكل النواة قاعدة حوسبة موثوقة (TCB) - مكونًا أساسيًا من البرامج التي يجب أن تعمل بشكل صحيح لضمان أمان النظام. في النظم الحقيقية ، هذه القاعدة أوسع بكثير من مجرد نواة دقيقة. من الضروري التحقق من رصة البرنامج الإضافية للحصول على نفس مستوى الثقة بالنسبة للنواة. ومع ذلك ، هناك فئات من الأنظمة التي ليست هناك حاجة لمثل هذا التحقق: فهي تحتاج إلى نظريات العزل على مستوى kernel لاشتقاق بعض خصائص الأمان على مستوى النظام. يقدم هذا القسم مثالاً على مثل هذا النظام.

هذه هي الأنظمة التي طبقت فيها مكونات البنية بالفعل خاصية مهمة ، وربما إلى جانب العديد من المكونات الصغيرة الموثوقة. مثالنا هو برنامج quadcopter للتحكم في الطيران ، وهو جهاز تجريبي في برنامج HACMS المذكور سابقًا.

يوضح الشكل 3 مكونات الأجهزة الرئيسية في quadrocopter. العمارة أكثر تعقيدًا عن تلك المطلوبة من قبل quadcopter ، حيث كان من المفترض أن تمثل ULB وفي هذا المستوى من التجريد تشبه بنية ULB.


شكل 3. الهندسة المعمارية للطائرة ذاتية الحكم

يوضح الشكل جهازي كمبيوتر رئيسيين: كمبيوتر على متن الطائرة يتصل بالمحطة الأرضية ويتحكم في البرنامج على متن الطائرة (على سبيل المثال ، الكاميرا) ، وجهاز كمبيوتر للملاحة للتحكم في رحلة السيارة ، وقراءة بيانات المستشعر ، ومحركات التحكم. يتم توصيل أجهزة الكمبيوتر عبر شبكة داخلية أو حافلة CAN على quadrocopter ، Ethernet على ULB. يحتوي quadrocopter أيضًا على نقطة WiFi غير محمية ، مما يجعل من الممكن إظهار طرق حماية إضافية.

في هذا المثال ، ضع في الاعتبار الكمبيوتر الموجود على متن الطائرة. يجب استيفاء أربعة خصائص أساسية لذلك:

• المصادقة الصحيحة للأوامر من المحطة الأرضية ؛
  
• خصوصية مفاتيح التشفير ؛
  
• لا توجد رسائل إضافية للكمبيوتر الملاحة ؛
  
• لا يمكن أن تؤثر البرامج غير الموثوق بها من الأنظمة الأخرى الموجودة على متن الطائرة على طيران الجهاز.

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

يوضح الشكل 4 كيف تم تصميم بنية quadrocopter لتوفير هذه الخصائص. يُعد جهاز Linux الظاهري (VM) بمثابة حاوية لبرامج الأجهزة المدمجة القديمة وبرامج تشغيل الكاميرا ونقاط اتصال WiFi. نقوم بعزل وحدة التحكم في التشفير في مكونها الخاص ، من خلال اتصالات بـ CAN ، وقناة المحطة الأرضية ، وجهاز Linux الظاهري لإرسال البيانات إلى المحطة الأرضية. تتمثل مهمة مكون التشفير في إرسال (فقط) رسائل معتمدة إلى الكمبيوتر الموجود على متنها عبر واجهة CAN الخاصة بالمكدس وإرسال بيانات تشخيصية مرة أخرى إلى المحطة الأرضية. يرسل مكون الراديو ويتلقى الرسائل الأولية التي يتم تشفيرها وفك تشفيرها (مع المصادقة) بواسطة مكون التشفير.


الشكل 4. كوادكوبتر مبسطة هندسة الكمبيوتر على متن الطائرة

يتم تحديد خصائص النظام المرغوبة فقط لخصائص العزل وسلوك البنية من حيث تدفق المعلومات ، وكذلك سلوك مكون تشفير موثوق واحد. على افتراض السلوك الصحيح لهذا المكون ، لا يمكن اختراق المفاتيح ، لأنه لا يوجد مكون آخر يمكنه الوصول إليها. القناة بين Linux ومكون التشفير في الشكل. 4 مخصص فقط للمراسلة ولا يتيح الوصول إلى الذاكرة. يمكن فقط الوصول إلى الرسائل المسموح بها إلى ناقل CAN ، لأن مكون التشفير هو التواصل الوحيد مع الناقل. يتم تغليف البرامج غير الموثوق بها و WiFi ، كجزء من جهاز Linux الظاهري ، بمعزل عن المكونات ويمكنها فقط التفاعل مع بقية النظام من خلال مكون تشفير موثوق.

من السهل أن نتخيل أن مثل هذا التحليل للعمارة يمكن أتمتة إلى حد كبير من خلال فحص النماذج وأدوات التفكير المنطقي الميكانيكية على مستوى أعلى. كما هو موضح في أنظمة MILS ، فإن حدود المكونات في مثل هذه البنية ليست مجرد أداة مناسبة للتقسيم وإدارة الشفرة ، ولكن مع العزلة القسرية توفر حدودًا فعالة للتفكير الرسمي حول سلوك النظام. ومع ذلك ، كل هذا يتوقف على التطبيق الصحيح لحدود المكونات في وقت التشغيل في تنفيذ النظام الثنائي النهائي.

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

التحقق من عرض المكون

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


شكل 5. يسير سير العمل

توليد الشفرة

داخليًا ، ينفذ CAmkES هذه التجريدات باستخدام كائنات kernel منخفضة المستوى في seL4. يحتوي كل مكون (على الأقل) على دفق واحد و CSpace و VSpace. تستخدم موصلات RPC كائنات نقطة النهاية ، ويقوم CAmkES بإنشاء رمز وسيط لمعالجة الرسائل وإرسالها إلى نقاط نهاية IPC. وبالمثل ، يتم تطبيق موصل منفذ البيانات من خلال الذاكرة المشتركة - الإطارات الشائعة الموجودة في مساحات العنوان لمكونين - ويمكن أن يحد اختياريا من اتجاه نقل البيانات. أخيرًا ، يتم تطبيق موصل الحدث باستخدام آلية الإخطار seL4.

ينشئ CAmkES أيضًا في capDL مواصفات منخفضة المستوى للتكوين الأولي للكائنات وقدرات نواة النظام. تصبح هذه المواصفات مدخلات إلى مُهيئ seL4 ، والتييبدأ أولاً بعد التحميل ويقوم بتنفيذ عمليات seL4 اللازمة لإنشاء مثيل وتهيئة النظام .

وبالتالي ، فإن النظام الأساسي للمكونات يولد الكود دون بذل جهد إضافي من جانب المطور. تصف بنية المكونات مجموعة من الكتل والسهام ، وتأتي مهمة التنفيذ لتعبئة الحقول. يقوم النظام بإنشاء الباقي ، مما يوفر تنفيذ البنية الموصوفة.

في النظام الأساسي الذي يحتوي على مكونات تقليدية ، ستعمل التعليمة البرمجية التي تم إنشاؤها على توسيع قاعدة الحوسبة الموثوق بها للنظام ، حيث يمكن أن تؤثر على وظائف المكونات. ومع ذلك ، CAmkES يولد أيضا أدلة.

دليل السيارات

عند إنشاء الكود "الوسيط" ، ينتج CAmkES البراهين الرسمية في Isabelle / HOL ، مما يؤدي التحقق من الصحة أثناء الترجمة ويوضح أن الكود "الوسيط" الذي تم إنشاؤه يطيع المواصفات عالية المستوى ، ومواصفات capDL التي تم إنشاؤها هي المواصفات الصحيحة لوصف CAmkES . لقد أثبتنا أيضًا أن مُهيئ seL4 يقوم بتكوين النظام بشكل صحيح في التكوين الأولي المطلوب. في الوقت نفسه ، نقوم تلقائيًا بمعظم عمليات بناء النظام دون توسيع قاعدة الحوسبة الموثوقة.

نادراً ما ينظر المطورون إلى إصدار منشئي الشفرات ؛ فهم مهتمون فقط بالوظائف والمنطق التجاري. نفترض أيضًا أن دليل الشفرة الوسيطة لا يحتاج إلى التحقق ، أي أنه يمكن للمطورين التركيز على إثبات صحة الشفرة الخاصة بهم. تمامًا مثلما يوفر رأس CAmkES الذي تم إنشاؤه للمطور واجهة برمجة تطبيقات للشفرة التي تم إنشاؤها ، فإن مشغلي lemma من المستوى الأعلى ينتجون واجهة برمجة تطبيقات للإثبات. تصف Lemmas السلوك المتوقع للموصلات. في مثال RPC الوسيطة في الشكل 6 وظيفة ولدت$$و يوفر وسيلة لاستدعاء وظائف عن بعد$و$$$ز في مكون آخر. لحفظ التجريد ، اتصل$g$$$و يجب أن يكون معادلا للدعوة$و$$$$g$ . نظام ولدت ليما يضمن ذلك $$و من رمز RPC الذي تم إنشاؤه يتصرف مثل الاتصال المباشر$و$$$$g$ .


شكل 6. رمز RPC الذي تم إنشاؤه من

أجل الاستخدام الفعلي للأدلة الناتجة عن النظام ، يجب أن تكون قابلة للتكوين مع أدلة تعسفية (تقريبًا) مقدمة من قبل المستخدم ، كما هو الحال بالنسبة لوظيفة$$ز ، والسياقات التي$g$$$$g$ و $$$و$ .لتحقيق هذا التركيب ، يتم تحديد مواصفات الموصل من خلال المواصفات التي يوفرها المستخدم للوظائف عن بُعد. وبهذه الطريقة ، يمكن للمهندسين التفكير في بنيتهم ​​من خلال توفير المواصفات والأدلة لمكوناتهم ، والاعتماد على مواصفات الشفرة التي تم إنشاؤها.

حتى الآن ، لقد أظهرنا هذه العملية من البداية إلى النهاية باستخدام موصل CAmkES RPC الخاص ( 1 ، 2 ). نظرًا لأن القوالب الخاصة بالموصلات الأخرى (منافذ البيانات والأحداث) أبسط بكثير من RPCs ، فلن يكون من الصعب توسيع منشئ الأدلة لدعم هذه الموصلات ، مما سيتيح لك إنشاء أنظمة تحقق أكثر تنوعًا.

بعد رمز الاتصال ، ينشئ CAmkES التكوين الأولي للتحكم في الوصول لتطبيق حدود البنية. لإثبات أن هذين الوصفين للنظام - capDL و CAmkES - يتطابقان مع بعضهما البعض ، يجب الأخذ في الاعتبار وصف CAmkES على أنه تجريد لوصف capDL. نحن نستخدم إطار العمل الذي تم اختباره مسبقًا لاشتقاق سلطة كائن على كائن آخر من وصف capDL. لذلك سنزيد الأدلة إلى مستوى السياسة. بالإضافة إلى ذلك ، قمنا بتحديد قواعد لسحب السلطة بين المكونات في وصف CAmkES. يضمن هذا الدليل أن كائنات capDL الممثلة كرسم امتياز مع الكائنات التي تم تجميعها حسب المكونات لها نفس الحدود بين المجموعات كما في الرسم البياني المكون المكافئ CAmkES. حدسيًا ، تعني مراسلات الحدود هذه أن تحليل بنية السياسة من وصف CAmkES سيوفر السياسة من الوصف الذي تم إنشاؤه بواسطة capDL ، والذي بدوره يضمن تلبية متطلبات تقييد السلطة والنزاهة والسرية ، كما ذكر سابقًا.

أخيرًا ، لإثبات التهيئة الصحيحة ، يستخدم CAmkES أداة تهيئة عالمية تبدأ كأول مهمة للمستخدم بعد التحميل. في seL4 ، تتمتع مهمة المستخدم الأولى (الفريدة) هذه بالوصول إلى جميع الذاكرة المتاحة ، واستخدامها لإنشاء كائنات و "قدرات" وفقًا للوصف التفصيلي لـ capDL ، التي تقبلها كمدخلات. ثبت ذلكالحالة بعد تنفيذ المُهيِّئ ترضي الحالة الموصوفة في المواصفات المحددة . ينطبق هذا الدليل على نموذج المُهيئ الدقيق ، ولكن ليس على مستوى التنفيذ. مقارنة بعمق سلسلة الأدلة ، قد يبدو هذا القيد ضعيفًا ، لكنه بالفعل دليل رسمي أكثر مما هو مطلوب على أعلى مستوى (EAL7) لمعايير تقييم السلامة العامة.

ترقية الأمن الزلزالي

في الممارسة العملية ، من الصعب ضمان تطوير نظام من نقطة الصفر من أجل الأمن ، وبالتالي فإن القدرة على ترقية البرامج القديمة أمر بالغ الأهمية لتطوير أنظمة آمنة. يدعم إطار عملنا المستندة إلى seL4 عملية تكرارية نسميها "ترقيات السلامة الزلزالية" ، حيث سيقوم المهندس المعماري المنتظم بترقية المباني القائمة لتحقيق مزيد من الاستقرار الزلزالي. نوضح العملية من خلال مثال على التكيف التدريجي لهندسة البرمجيات الحالية لطائرة هليكوبتر بدون طيار ، والانتقال من مخطط الاختبار التقليدي إلى نظام موثوق للغاية مع نظريات تدعمها أساليب رسمية. على الرغم من أن هذا المثال يعتمد على مشروع ULB حقيقي ، إلا أنه مبسط هنا ولا يشمل جميع التفاصيل.

العمارة الأصلية للمروحية تتزامن مع العمارة الموصوفة في الشكل. 3. يتم توفير وظيفتها من قبل جهازي كمبيوتر منفصلين: يتحكم كمبيوتر الملاحة في الرحلة الفعلية ، ويقوم الكمبيوتر الموجود على متن الطائرة بمهام عالية المستوى (مثل الاتصال بمحطة أرضية والتنقل في الصورة من الكاميرا). كان الإصدار الأولي من الكمبيوتر الموجود على متن الطائرة تطبيقًا مترابطًا لنظام Linux. خلال عملية التحديث ، طبق مهندسو بوينج الأساليب والأدوات والمكونات المقدمة من شركاء HACMS.

الخطوة 1. الافتراضية

(. . 7). . seL4 CAmkES, (VMM) , Linux. , VMM . seL4 , VMM, VMM . VMM , .


. 7.

, , . MMU IOMMU . , . 1 2.

الخطوة 2. أجهزة افتراضية متعددة

الخطوة الثانية من التحديث الزلزالي تعزز الجدران القائمة. في البرامج ، يمكن للمطور زيادة الأمان والموثوقية عن طريق تقسيم النظام المصدر إلى عدة أنظمة فرعية ، كل منها يتكون من جهاز افتراضي يعمل فقط على جزء من كود النظام المصدر. يتم تنفيذ كل تركيبة VM / VMM في مكون CAmkES منفصل ، والذي يقدم عزلًا بين الأنظمة الفرعية المختلفة ، ولا يسمح لهم بالتأثير على بعضهم البعض ، ثم يسمح بالتعايش بين مستويات مختلفة من الأمان.

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

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

بالإضافة إلى الأجهزة الظاهرية التي تمثل النظم الفرعية للنظام المصدر ، نقوم أيضًا باستخراج وتنفيذ المكونات لأي موارد مشتركة (مثل واجهة الشبكة).

يمكنك تكرار الخطوة 2 حتى نصل إلى التفاصيل المطلوبة للأقسام. التفاصيل الصحيحة هي حل وسط بين قوة العزل ، من ناحية ، وزيادة تكاليف الاتصالات وإعادة الإعمار ، من ناحية أخرى.

في مثالنا ، حصلنا على ثلاثة أقسام: آلة افتراضية تنفذ وظائف الاتصال لمحطة أرضية تشغل Linux ؛ جهاز افتراضي آخر يقوم بتنفيذ وظائف التنقل القائمة على الكاميرا (التي تعمل أيضًا بنظام Linux) ؛ ومكون مشاركة الشبكة الأصلية ، كما هو موضح في الشكل. 8.


الشكل 8. وظائف مقسمة إلى العديد من الأجهزة الافتراضية

الخطوة 3. المكونات الأصلية

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

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

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

في مثالنا ، سنقوم بتحليل الجهاز الظاهري لقناة الاتصال بين الكمبيوتر على متن الطائرة والمحطة الأرضية إلى وحدات أصلية. في المكونات الأصلية ، يتم تنفيذ وظائف الاتصال والتشفير والتحكم (مدير المهام). سنترك الكاميرا و WiFi في الجهاز الظاهري كمكون قديم لا يمكن الاعتماد عليه (انظر الشكل 9). أصبح هذا الفصل حلاً وسطًا بين الجهود المبذولة لإعادة تشكيل النظم الفرعية وفوائد استخدام المكونات الأصلية من حيث الأداء والموثوقية.


شكل 9. وظيفة تنفيذها في المكونات الأصلية

الخطوة 4. موثوقية النظام ككل

بعد تلقي جميع الوحدات اللازمة ، سنتخذ الخطوة الأخيرة: تحليل النظام بأكمله ككل بناءً على موثوقية الهيكل والمكونات الفردية.

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

يتم تطبيق مكون الشبكة على كود C القياسي ، والذي يتكون من كود المستخدم للنظام الأساسي ورمز المكتبة الحالي. مستوى موثوقيتها يتوافق مع المستوى الذي تم الحصول عليه من خلال التنفيذ الدقيق للشفرة المعروفة. يمكن تحسين الموثوقية دون حساب كبير باستخدام طرق مثل توليف برنامج التشغيل ، وكذلك باستخدام لغات آمنة من النوع مثل العاج. في تحليل عام لأمان النظام ، فإن أي حل وسط لمكون الشبكة سوف يؤثر فقط على حزم الشبكة. نظرًا لأن حركة المرور مشفرة ، فإن هذا الهجوم لن يعرض للخطر حالة المواصفات التي تصل بها الأوامر المخولة فقط إلى الكمبيوتر الموجود على متن الطائرة.

الجهاز الظاهري لكاميرا الفيديو هو أضعف جزء من النظام ، لأنه يعمل على نظام Linux ويفترض أنه يحتوي على نقاط ضعف. لكن جهاز VM معزول ، لذا إذا قام المهاجمون بتكسيره ، فلن يتمكنوا من الانتقال إلى مكونات أخرى. أسوأ شيء يمكن للمهاجم القيام به هو إرسال بيانات خاطئة إلى عنصر التحكم. كما هو الحال في quadrocopter ، يتحقق هذا المكون من البيانات الواردة من الكاميرا. وصمد بنجاح الهجوم السيبراني المذكور في بداية المقال. لقد كان هجوم "مربع أبيض" ، حيث تم منح فريق البنتستر الوصول إلى جميع الشفرات والوثائق ، وكذلك لجميع قنوات الاتصال الخارجية. تم منحها عمدا الوصول إلى الجذر إلى الجهاز الظاهري للكاميرا ، محاكاة هجوم ناجح على البرامج التي عفا عليها الزمن. أصبح احتواء الهجوم والقدرة على الدفاع ضد هذا السيناريو القوي اختبارًا جيدًا لمتطلبات الأمان الخاصة بنا وتحديد أي افتراضات ضائعة أو مشكلات في الواجهة أو مشكلات أمنية أخرى قد لا يتعرف عليها فريق البحث.

القيود والعمل في المستقبل

توفر هذه المقالة نظرة عامة حول طريقة تحقيق مستويات عالية جدًا من الأمان للأنظمة التي تكون فيها ميزة الأمان قابلة للتطبيق من خلال بنية المكون. لقد أثبتنا نظريات مستوى kernel وتكوينه الصحيح ، وكذلك النظريات التي تضمن أن النظام الأساسي للمكونات يحدد حدود الأمان بشكل صحيح وفقًا لوصف بنيته ، وأنه يولد الرمز الصحيح لمكالمات الإجراء البعيد. يظل الاتصال بتحليل الأمان عالي المستوى للنظام غير رسمي ، ولا تغطي نظريات رمز الاتصال جميع بدائل الاتصال التي توفرها المنصة. للحصول تلقائيًا على نظرية تغطي النظام بالكامل من البداية إلى النهاية ، يلزم القيام بعمل إضافي. ومع ذلك ، في هذه المرحلة ، من الواضح أن هذه مهمة ممكنة.

الهدف الرئيسي من العمل المقدم هو التقليل بشكل كبير من جهود التحقق لفئات معينة من الأنظمة. يمكن توسيع نطاق النهج المعماري البحت الموصوف هنا إلى أنظمة أخرى غير ULB ، ولكن من الواضح أنه مقيد بحقيقة أنه يمكن فقط التعبير عن الخصائص التي تحددها بنية المكون للنظام. ستنخفض العوائد إذا تغيرت هذه البنية أثناء تنفيذ البرنامج ، وإذا كانت الخصائص تعتمد اعتمادًا كبيرًا على سلوك الكثير من المكونات أو المكونات الموثوق بها ذات الحجم الكبير جدًا.

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

التطبيق: تكاليف العمالة

استغرق تطوير التصميم ورمز seL4 عامين. إذا أضفنا جميع الأدلة الخاصة بالنمط المصلي ، فسيتم الحصول على ما مجموعه 18 عامًا لكل شخص لـ 8700 سطرًا من التعليمات البرمجية لـ C. للمقارنة ، فإن تطوير microkernel L4Ka :: Pistachio المقارن من عائلة seL4 استغرق 6 سنوات ولم يوفر مستوى كبيرًا من الموثوقية. وهذا يعني وجود اختلاف في سرعة التطوير يبلغ 3.3 مرة فقط بين البرامج التي تم التحقق منها والبرامج التقليدية. وفقًا لطريقة تقييم Colbert و Bohm ، ستستغرق الشهادة وفقًا لمعايير EAL7 التقليدية لـ 8700 سطرًا من الكود C أكثر من 45.9 عامًا. هذا يعني أن التحقق الرسمي للتنفيذ على المستوى الثنائي يكون بالفعل أقل 2.3 مرة من أعلى مستوى من الشهادات وفقًا للمعايير العامة ، مع توفير موثوقية أعلى بكثير.

للمقارنة ، يستخدم نهج HACMS الموصوف هنا فقط الأدلة الموجودة لكل نظام جديد ، بما في ذلك الأدلة الناتجة عن الأدوات. وبالتالي ، فإن جهد إثبات عام لنظام يتطابق مع هذا النهج يأتي إلى أسابيع رجل ، وليس سنوات ، ويأتي الاختبار فقط للتحقق من صحة الافتراضات.