منصب الدكتوراه - المواصفات متعددة المستويات والتحقق من خصائص الأمن السيبراني لبرامج C.

تفاصيل الفرصة

المكافأة الإجمالية

0 $

جامعة حكومية

CEA Tech

المنطقة

أوروبا الغربية

البلد المضيف

فرنسا

آخر موعد للتقديم

31 أكتوبر 2021

المستوى التعليمي

الدكتوراه

نوع الفرصة

الدكتوراه

التخصصات

تكنولوجيا المعلومات وعلوم الحاسوب

تمويل الفرصة

غير ممولة

الدول المؤهلة

هذه الفرصة متوفرة لجميع البلدان

المنطقة المؤهلة

جميع المناطق

SL-DRT-21-0866

مجال البحث

الأمن السيبراني: الأجهزة والبرامج

نبذة مختصرة

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