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

الموسوعة الحرة

في سياق أنظمة الأجهزة والبرمجيات ، يُعرَّف التحقق الرسمي بأنه عملية إثبات أو دحض صحة نظام ما وفقًا لمواصفات أو خصائص رسمية محددة، باستخدام الأساليب الرسمية للرياضيات . [ 1 ] يُعد التحقق الرسمي حافزًا رئيسيًا للمواصفات الرسمية للأنظمة ، وهو جوهر الأساليب الرسمية . كما يُمثل بُعدًا هامًا من أبعاد التحليل والتحقق في أتمتة التصميم الإلكتروني، وهو أحد مناهج التحقق من البرمجيات . يُتيح استخدام التحقق الرسمي الحصول على أعلى مستوى من ضمان التقييم ( EAL7 ) ضمن إطار المعايير المشتركة لشهادة أمن الحاسوب . [ 2 ]

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

يتم التحقق من هذه الأنظمة من خلال ضمان وجود برهان رسمي لنموذج رياضي للنظام. [ 3 ] ومن أمثلة الكائنات الرياضية المستخدمة لنمذجة الأنظمة: آلات الحالة المحدودة ، وأنظمة الانتقال المصنفة ، وعبارات هورن ، وشبكات بيتري ، وأنظمة جمع المتجهات ، والأتمتة الموقوتة ، والأتمتة الهجينة ، وجبر العمليات ، والدلالات الرسمية للغات البرمجة مثل الدلالات التشغيلية ، والدلالات التفسيرية ، والدلالات البديهية ، ومنطق هوار . [ 4 ]

الأساليب

التحقق من النموذج

يتضمن التحقق من النموذج استكشافًا منهجيًا وشاملًا للنموذج الرياضي. هذا الاستكشاف ممكن للنماذج المحدودة ، وكذلك لبعض النماذج غير المحدودة، حيث يمكن تمثيل مجموعات غير محدودة من الحالات بشكل فعال باستخدام التجريد أو الاستفادة من التناظر. عادةً، يتضمن ذلك استكشاف جميع الحالات والانتقالات في النموذج، باستخدام تقنيات تجريد ذكية ومخصصة للمجال، وذلك للنظر في مجموعات كاملة من الحالات في عملية واحدة وتقليل وقت الحساب. تشمل تقنيات التنفيذ تعداد فضاء الحالة ، وتعداد فضاء الحالة الرمزي، والتفسير المجرد ، والمحاكاة الرمزية ، وتحسين التجريد. غالبًا ما تُوصف الخصائص المراد التحقق منها في منطق زمني ، مثل المنطق الزمني الخطي (LTL)، ولغة مواصفات الخصائص (PSL)، وتأكيدات SystemVerilog (SVA)، [ 5 ] أو منطق الشجرة الحسابي (CTL). الميزة الكبرى للتحقق من النموذج هي أنه غالبًا ما يكون تلقائيًا بالكامل؛ أما عيبه الرئيسي فهو أنه لا يتوسع بشكل عام ليشمل الأنظمة الكبيرة. عادةً ما تقتصر النماذج الرمزية على بضع مئات من بتات الحالة، بينما يتطلب تعداد الحالة الصريح أن تكون مساحة الحالة التي يتم استكشافها صغيرة نسبيًا.

التحقق الاستنتاجي

يُعد التحقق الاستنتاجي نهجًا آخر. [ 6 ] [ 7 ] ويتألف من توليد مجموعة من التزامات البرهان الرياضي من النظام ومواصفاته (وربما غيرها من البيانات) ، حيث يدل صدق هذه الالتزامات على مطابقة النظام لمواصفاته، ثم إثبات هذه الالتزامات باستخدام إما برامج مساعدة البرهان (برامج إثبات النظريات التفاعلية) (مثل HOL و ACL2 و Isabelle و Rocq (المعروف سابقًا باسم Coq ) أو PVS )، أو برامج إثبات النظريات الآلية ، بما في ذلك على وجه الخصوص حلول قابلية الإرضاء المعيارية للنظريات (SMT). ويكمن عيب هذا النهج في أنه قد يتطلب من المستخدم فهمًا دقيقًا لسبب عمل النظام بشكل صحيح، ونقل هذه المعلومات إلى نظام التحقق، إما في شكل سلسلة من النظريات المراد إثباتها أو في شكل مواصفات (ثوابت، شروط مسبقة، شروط لاحقة) لمكونات النظام (مثل الدوال أو الإجراءات) وربما مكونات فرعية (مثل الحلقات أو هياكل البيانات).

تطبيق على البرمجيات

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

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

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

التحقق والتدقيق

التحقق هو أحد جوانب اختبار مدى ملاءمة المنتج للغرض المقصود، أما التحقق من الصحة فهو الجانب المكمل له. وغالبًا ما يُشار إلى عملية الفحص الشاملة بمصطلحي "التحقق من الصحة والتحقق من الصحة".

  • التحقق : "هل نحاول صنع الشيء الصحيح؟"، أي هل المنتج مصمم وفقًا لاحتياجات المستخدم الفعلية؟
  • التحقق : "هل صنعنا ما كنا نحاول صنعه؟"، أي هل المنتج مطابق للمواصفات؟

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

إصلاح البرنامج الآلي

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

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

الاستخدام الصناعي

مع ازدياد تعقيد التصاميم، تزداد أهمية تقنيات التحقق الرسمي في صناعة الأجهزة . [ 10 ] [ 11 ] في الوقت الراهن، تستخدم معظم شركات الأجهزة الرائدة، إن لم تكن جميعها، التحقق الرسمي، [ 12 ] إلا أن استخدامه في صناعة البرمجيات لا يزال محدودًا. يُعزى ذلك إلى الحاجة الماسة إليه في صناعة الأجهزة، حيث تكتسب الأخطاء أهمية تجارية أكبر. ونظرًا للتفاعلات الدقيقة المحتملة بين المكونات، يصبح من الصعب بشكل متزايد محاكاة مجموعة واقعية من الاحتمالات. تُعدّ جوانب مهمة من تصميم الأجهزة قابلة للتطبيق على أساليب الإثبات الآلية، مما يُسهّل إدخال التحقق الرسمي ويجعله أكثر إنتاجية. [ 13 ]

اعتبارًا من عام 2011تم التحقق رسميًا من عدة أنظمة تشغيل، منها: النواة المصغرة الآمنة المدمجة من الطبقة الرابعة (Secure Embedded L4) التابعة لـ NICTA ، والتي تُباع تجاريًا باسم seL4 من قِبل OK Labs؛ [ 14 ] ونظام التشغيل ORIENTAIS القائم على OSEK/VDX والمُصمم للعمل في الوقت الحقيقي من قِبل جامعة شرق الصين للمعلمين ؛ ونظام التشغيل Integrity من Green Hills Software ؛ ونظام PikeOS من SYSGO . [ 15 ] [ 16 ] وفي عام 2016، قام فريق بقيادة تشونغ شاو في جامعة ييل بتطوير نواة نظام تشغيل تم التحقق منها رسميًا تُسمى CertiKOS. [ 17 ] [ 18 ]

اعتبارًا من عام 2017، طُبِّقَ التحقق الرسمي على تصميم شبكات الحاسوب الكبيرة من خلال نموذج رياضي للشبكة، [ 19 ] وكجزء من فئة جديدة من تقنيات الشبكات، وهي الشبكات القائمة على النوايا . [ 20 ] ومن بين موردي برامج الشبكات الذين يقدمون حلول التحقق الرسمي: سيسكو [ 21 ]، وفوروارد نتوركس [ 22 ] [ 23 ] ، وفيريفلو سيستمز. [ 24 ]

توفر لغة برمجة SPARK مجموعة أدوات تمكن من تطوير البرمجيات مع التحقق الرسمي وتستخدم في العديد من الأنظمة عالية الموثوقية .

يُعد مُترجم CompCert C مُترجم C تم التحقق منه رسميًا، وهو يُنفذ غالبية معيار ISO C. [ 25 ] [ 26 ]

انظر أيضاً

مراجع

  1. ↑ سانغافي، ألوك (21 مايو 2010). "ما هو التحقق الرسمي؟". إي إي تايمز آسيا .
  2. ↑ "المعايير المشتركة لتقييم أمن تكنولوجيا المعلومات، الجزء 5: حزم محددة مسبقًا من متطلبات الأمان" (ملف PDF) . تم الاطلاع عليه بتاريخ 15 أبريل 2025 .
  3. ↑ سانجيت أ. سيشيا؛ ناتاشا شاريجينا؛ ستافروس تريباكيس (2018). "الفصل 3: النمذجة للتحقق". في: كلارك، إدموند م.؛ هينزينجر، توماس أ.؛ فيث، هيلموت؛ بلوم، رودريك (محررون). دليل التحقق من النماذج . سبرينغر. ص 75-105 . doi : 10.1007/978-3-319-10575-8 . ISBN  978-3-319-10574-1.
  4. ↑ مقدمة في التحقق الرسمي ، جامعة كاليفورنيا، بيركلي، تم الاطلاع عليه في 6 نوفمبر 2013
  5. ↑ كوهين، بن؛ فينكاتارامانان، سرينيفاسان؛ كوماري، أجيتا؛ بايبر، ليزا (2015). دليل تأكيدات SystemVerilog ( الطبعة الرابعة). منصة النشر المستقلة CreateSpace. ISBN  978-1518681448.
  6. ↑ أهرندت، وولفغانغ؛ بيكرت، برنارد؛ بوبل، ريتشارد؛ هانله، راينر؛ شميت، بيتر هـ.، محرران (2016). التحقق الاستنتاجي من البرمجيات - الكتاب الرئيسي: من النظرية إلى التطبيق ( الطبعة الأولى 2016). تشام: دار نشر سبرينغر الدولية : اسم العلامة التجارية: سبرينغر. ISBN   978-3-319-49812-6.
  7. ↑ بريتشنر، ألكسندر؛ مولر، بيتر؛ ستوكل، باتريك، محرران. (2019). "بناء مدققات البرامج الاستنتاجية - ملاحظات المحاضرة". هندسة أنظمة برمجيات آمنة وموثوقة . أمستردام، هولندا: دار نشر IOS. ISBN 978-1-61499-976-8.
  8. ↑ لو غويس، كلير ؛ نغوين، ثانه فو؛ فورست، ستيفاني؛ وايمر، ويستلي (يناير 2012). "GenProg: طريقة عامة لإصلاح البرمجيات تلقائيًا" . معاملات IEEE في هندسة البرمجيات . 38 (1): 54-72 . doi : 10.1109/TSE.2011.104 . S2CID 4111307 . 
  9. ↑ ديماركو، فافيو؛ شوان، جيفنغ؛ لو بير، دانيال؛ مونبيروس، مارتن (2014). "الإصلاح التلقائي لشروط if المعيبة والشروط المسبقة المفقودة باستخدام SMT" . المؤتمر الدولي السادس والثلاثون لهندسة البرمجيات ICSE '14: 30-39 . arXiv : 1404.3186 . doi : 10.1145 /2593735.2593740 . تاريخ الاسترجاع: 8 يونيو 2026 .
  10. ↑ هاريسون، ج. (2003). "التحقق الرسمي في إنتل". المؤتمر السنوي الثامن عشر لمعهد مهندسي الكهرباء والإلكترونيات حول المنطق في علوم الحاسوب، 2003. وقائع المؤتمر . الصفحات 45-54 . doi : 10.1109/LICS.2003.1210044 . ISBN  978-0-7695-1884-8. S2CID 44585546 . 
  11. ↑ التحقق الرسمي من تصميم أجهزة تعمل في الوقت الحقيقي . Portal.acm.org (27 يونيو 1983). تم الاطلاع عليه في 30 أبريل 2011.
  12. ↑ "التحقق الرسمي: أداة أساسية لتصميم VLSI الحديث من تأليف إريك سيليغمان، وتوم شوبرت، وإم في أتشوثا كيرانكومار" . 2015.
  13. ↑ "التحقق الرسمي في الصناعة" (ملف PDF) . تم الاطلاع عليه بتاريخ 20 سبتمبر 2012 .
  14. ↑ "المواصفات الرسمية المجردة لواجهة برمجة التطبيقات seL4/ARMv6" (ملف PDF) . مؤرشف من الأصل (ملف PDF) بتاريخ 21 مايو 2015. تم الاطلاع عليه بتاريخ 19 مايو 2015 .
  15. ↑ كريستوف باومان، برنارد بيكرت، هولجر بلاسوم، وثورستن بورمر: مكونات صحة نظام التشغيل؟ دروس مستفادة من التحقق الرسمي من نظام التشغيل بايك أو إس. مؤرشف في 19 يوليو 2011 على موقع Wayback Machine .
  16. ↑ "الوصول إلى الصواب" بقلم جاك جانسل
  17. ↑ هاريس، روبن. "نظام تشغيل غير قابل للاختراق؟ يُمكّن نظام CertiKOS من إنشاء نواة نظام آمنة" . ZDNet . تم الاطلاع عليه في 10 يونيو 2019 .
  18. ↑ "CertiKOS: جامعة ييل تطور أول نظام تشغيل مقاوم للاختراق في العالم" . صحيفة إنترناشونال بيزنس تايمز البريطانية . 15 نوفمبر 2016. تم الاطلاع عليه بتاريخ 10 يونيو 2019 .
  19. ↑ سكروكسون، أليكس. "بالنسبة لشركة سيسكو، الشبكات القائمة على النوايا تبشر بمتطلبات تقنية مستقبلية" . مجلة كمبيوتر ويكلي . تم الاطلاع عليه بتاريخ 12 فبراير 2018 .
  20. ↑ ليرنر، أندرو. "الشبكات القائمة على النوايا" . غارتنر . تم الاطلاع عليه بتاريخ 12 فبراير 2018 .
  21. ↑ كيرفالا، زيوس. "سيسكو تُدخل الشبكات القائمة على النوايا إلى مراكز البيانات" . NetworkWorld. مؤرشف من الأصل في 11 ديسمبر 2023. تم الاطلاع عليه في 12 فبراير 2018 .
  22. ↑ "الشبكات الأمامية: تسريع عمليات الشبكة وتقليل مخاطرها" . شركة إنسايتس سكسيس ميديا ​​آند تكنولوجي المحدودة . إنسايتس سكسيس. ١٦ يناير ٢٠١٨. تم الاطلاع عليه بتاريخ ١٢ فبراير ٢٠١٨ .
  23. ↑ "التعمق في الشبكات القائمة على النية" (ملف PDF) . NetworkWorld . تم الاطلاع عليه بتاريخ 12 فبراير 2018 .
  24. ↑ "أنظمة فيريفلو" . بلومبيرغ . تم الاطلاع عليه بتاريخ 12 فبراير 2018 .
  25. ↑ "CompCert - مُترجم لغة C من CompCert" . compcert.org . تم الاطلاع عليه بتاريخ 22 فبراير 2023 .
  26. ↑ باريير، أوريل؛ بلازي، ساندرينا ؛ بيشاردي، ديفيد (9 يناير 2023). "توليد كود أصلي مُدقَّق رسميًا في مُترجم فوري فعال: تحويل الواجهة الخلفية لـ CompCert إلى مُترجم فوري مُدقَّق رسميًا" . وقائع مؤتمر ACM للغات البرمجة . 7 (POPL): 249-277 . arXiv : 2212.03129 . doi : 10.1145/3571202 . ISSN 2475-1421 . S2CID 253736486 .