سبارك (لغة برمجة)

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

سبارك هي لغة برمجة حاسوبية مُعرَّفة رسميًا، مبنية على لغة البرمجة آدا ، ومُصممة لتطوير برمجيات عالية الموثوقية تُستخدم في الأنظمة التي تتطلب تشغيلًا موثوقًا وقابلًا للتنبؤ بدرجة عالية. تُسهِّل سبارك تطوير التطبيقات التي تتطلب السلامة والأمان وسلامة الأعمال. وقد وجدت استخدامًا واسعًا في الحوسبة الآنية والأنظمة المُدمجة ، حيث تُعدّ مسائل السلامة الحرجة أو أمن الحاسوب ذات أهمية قصوى. [ 2 ]

في الأصل، كانت هناك ثلاثة إصدارات من SPARK (SPARK83، SPARK95، SPARK2005)، تستند إلى Ada 83، Ada 95، و Ada 2005 على التوالي.

تم إصدار نسخة رابعة، SPARK 2014، مبنية على Ada 2012، في 30 أبريل 2014. SPARK 2014 عبارة عن إعادة تصميم كاملة للغة وتدعم أدوات التحقق من البرامج .

تتألف لغة SPARK من مجموعة فرعية محددة جيدًا من لغة Ada، تستخدم العقود لوصف مواصفات المكونات بصيغة مناسبة للتحقق الثابت والديناميكي على حد سواء. [ 3 ] كما صُممت SPARK لإزالة جميع بنيات اللغة التي قد تُسبب سلوكًا غير متوقع. [ 4 ]

في SPARK83/95/2005، تُشفّر العقود في تعليقات Ada، ولذلك يتجاهلها أي مُصرّف Ada قياسي، ولكن تتم معالجتها بواسطة SPARK Examiner والأدوات المرتبطة به. تركز هذه الإصدارات السابقة على التحقق الثابت من العقود. [ 3 ]

على النقيض من ذلك، يستخدم SPARK 2014 بنية الجوانب المدمجة في لغة Ada 2012 للتعبير عن العقود، مما يجعلها جزءًا أساسيًا من اللغة. تعتمد الأداة الرئيسية لـ SPARK 2014 (GNATprove) على بنية GNAT/GCC ، وتعيد استخدام معظم واجهة GNAT Ada 2012 الأمامية.

نظرة عامة فنية

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

يُمكّن الجمع بين هذه الأساليب مشروع SPARK من تحقيق أهدافه التصميمية، وهي:

قال أحد أعضاء فريق عمل براكسيس: "إن معدل العيوب لدينا مع سبارك أقل بعشر مرات على الأقل، وأحيانًا بمئة مرة، من تلك التي يتم إنشاؤها باستخدام لغات أخرى." [ 4 ]

أمثلة على العقود

انظر إلى مواصفات البرنامج الفرعي بلغة Ada أدناه:

إجراء زيادة (X : إدخال إخراج نوع_العداد)؛

في لغة Ada النقية، قد يزيد هذا المتغير Xبمقدار واحد أو ألف؛ أو قد يقوم بتعيين عداد عام Xوإرجاع القيمة الأصلية للعداد في X؛ أو قد لا يفعل شيئًا مع X.

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

الإجراء Increment (X : in out Counter_Type)  with Global => null , يعتمد => (X => X)؛

يحدد هذا أن Incrementالإجراء لا يستخدم أي متغير عام (لا تحديث ولا قراءة) وأن عنصر البيانات الوحيد المستخدم في حساب القيمة الجديدة Xهو Xوحده.

أو بدلاً من ذلك، يمكن كتابة المواصفات على النحو التالي:

الإجراء Increme (X : in out Counter_Type)  with Global => (In_Out => Count), يعتمد => (العدد => (العدد، س)، X => null);

يحدد هذا أن Incrementسيستخدم المتغير العام Countفي نفس الحزمة مثل Increment، وأن القيمة المصدرة لـ Countتعتمد على القيم المستوردة لـ Countو X، وأن القيمة المصدرة لـ Xلا تعتمد على أي متغيرات على الإطلاق وسيتم اشتقاقها من البيانات الثابتة فقط.

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

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

الإجراء Increment (X : in out Counter_Type)  with Global => null, يعتمد على => (X => X)، Pre => X < Counter_Type'Last, Post => X = X'Old + 1;

وهذا يحدد الآن ليس فقط أن Xالقيمة مشتقة من نفسها وحدها، ولكن أيضًا أنه قبل Incrementاستدعائها Xيجب أن تكون أقل تمامًا من آخر قيمة ممكنة لنوعها (لضمان عدم حدوث تجاوز في النتيجة أبدًا ) وأن القيمة بعد ذلك Xستكون مساوية للقيمة الأولية Xزائد واحد.

شروط التحقق

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

  • فهرس المصفوفة خارج النطاق
  • انتهاك نطاق النوع
  • القسمة على صفر
  • تجاوز عددي

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

يستخدم برنامج GNATprove، في جوهره، لغة Why3 الوسيطة ومولد VC، [ 3 ] بالإضافة إلى أدوات إثبات النظريات CVC4 و Z3 و Alt-Ergo لتفريغ VCs. كما يُمكن استخدام أدوات إثبات أخرى (بما في ذلك أدوات التحقق التفاعلية من البراهين) من خلال مكونات أخرى من مجموعة أدوات Why3.

تاريخ

تعود بدايات هذه التقنية إلى عام 1987، استنادًا إلى أعمال أُجريت في جامعة ساوثهامبتون . [ 3 ] أُنتجت النسخة الأولى من SPARK (المبنية على لغة Ada 83) في الجامعة، برعاية وزارة الدفاع البريطانية، على يد برنارد كاريه وتريفور جينينغز. استُمد اسم SPARK من SPADE Ada Kernel ، في إشارة إلى مجموعة SPADE الفرعية من لغة برمجة باسكال . [ 5 ]

بعد ذلك، جرى توسيع اللغة وتحسينها تدريجيًا، أولًا من قِبل شركة Program Validation Limited ثم من قِبل شركة Praxis Critical Systems Limited. في عام 2004، غيّرت شركة Praxis Critical Systems Limited اسمها إلى شركة Praxis High Integrity Systems Limited، واستمر العمل على برنامج SPARK. [ 4 ] في يناير 2010، أصبحت الشركة تُعرف باسم Altran Praxis .

في أوائل عام 2009، عقدت شركة براكسيس شراكة مع شركة أداكور، وأصدرت برنامج SPARK Pro بموجب شروط رخصة جنو العمومية (GPL). تبع ذلك في يونيو 2009 إصدار SPARK GPL Edition 2009، الموجه إلى مجتمعات البرمجيات الحرة والمفتوحة المصدر (FOSS) والمجتمعات الأكاديمية.

في يناير 2013، غيرت شركة Altran-Praxis اسمها إلى Altran، والتي أصبحت في أبريل 2021 شركة Capgemini Engineering (بعد اندماج Altran مع Capgemini ).

تم الإعلان عن الإصدار الاحترافي الأول من SPARK 2014 في 30 أبريل 2014، وسرعان ما تبعه إصدار SPARK 2014 GPL، الذي يستهدف مجتمعات البرمجيات الحرة والمفتوحة المصدر والمجتمعات الأكاديمية.

التطبيقات الصناعية

تم استخدام برنامج SPARK في عدد من التطبيقات الصناعية الواقعية. ويُعتبر دمجه في أقرب وقت ممكن من عملية التصميم هو الأكثر فعالية بشكل عام. [ 6 ]

تم استخدام SPARK في العديد من الأنظمة الهامة ذات الأهمية البالغة للسلامة، والتي تغطي الطيران التجاري (نظام أجهزة حدود التشغيل للسفن/المروحيات، [ 6 ] محركات رولز رويس ترينت النفاثة، ونظام ARINC ACAMS ، وطائرة لوكهيد مارتن C130J [ 6 ] )، والطيران العسكري ( يوروفايتر تايفون ، [ 3 ] هارير GR9 ، إير ماكي M346 )، وإدارة الحركة الجوية ( نظام UK NATS iFACTS [ 3 ] )، والسكك الحديدية (العديد من تطبيقات الإشارات)، والطب (جهاز LifeFlow للمساعدة البطينية )، وتطبيقات الفضاء ( مشروع CubeSat التابع لكلية فيرمونت التقنية [ 7 ] ).

فيما يتعلق بعمليات الموافقة اللازمة لمثل هذه الأنظمة، تم استخدام SPARK للحصول على شهادة وفقًا لمعيار الدفاع البريطاني (DEFSTAN) 00-55، [ 3 ] وكذلك وفقًا لمعيار DO-178B المستوى A و ITSEC E6. [ 6 ]

استُخدمت لغة SPARK أيضًا في تطوير الأنظمة الآمنة. ومن بين مستخدميها شركة روكويل كولينز (حلول Turnstile وSecureOne متعددة النطاقات)، وتطوير هيئة إصدار الشهادات الأصلية MULTOS ، [ 6 ] ونموذج Tokeneer التجريبي التابع لوكالة الأمن القومي الأمريكية ، [ 3 ] ومحطة العمل متعددة المستويات secunet، ونواة الفصل Muen، وبرنامج تشفير أجهزة الكتل Genode . كما طُبقت في حالة أخرى هيئة إصدار شهادات آمنة لبطاقة القيمة المخزنة التي تنتجها شركة Mondex International ، حيث استُخدمت صيغة Z كتمهيد للترميز في SPARK. [ 4 ]

في أغسطس 2010، قام رود تشابمان، كبير مهندسي شركة ألتران براكسيس، بتطبيق خوارزمية سكين ، إحدى الخوارزميات المرشحة لـ SHA-3 ، في لغة سبارك. بعد تحسين دقيق، تمكن من جعل نسخة سبارك أبطأ بنسبة تتراوح بين 5 و10% فقط من نسخة لغة C. لاحقًا، ساهمت التحسينات التي أُدخلت على واجهة Ada الوسيطة في GCC (التي نفذها إريك بوتكازو من شركة أداكور) في تقليص الفجوة، حيث أصبح أداء كود سبارك مطابقًا تمامًا لأداء كود C. [ 2 ]

اعتمدت شركة NVIDIA أيضًا تقنية SPARK لتنفيذ البرامج الثابتة ذات الأهمية الأمنية البالغة . [ 8 ] [ 9 ] ونظرًا لنجاحها في هذا المجال، أضافت الشركة تقنية SPARK لمشاريع إضافية متعلقة بالبرامج الثابتة، وبدأت بتقديم تدريب داخلي على استخدام هذه التقنية. [ 3 ]

في عام 2020، أعاد رود تشابمان برمجة مكتبة التشفير TweetNaCl في SPARK 2014. [ 10 ] تتميز نسخة SPARK من المكتبة بإثبات تلقائي كامل لسلامة النوع، وسلامة الذاكرة، وبعض خصائص الصحة، مع الحفاظ على خوارزميات ثابتة الوقت. كما أن كود SPARK أسرع بكثير من TweetNaCl. [ 3 ]

انظر أيضاً

مراجع

  1. ↑ "مبررات Ada2012" (ملف PDF) . adacore.com . مؤرشف (ملف PDF) من الأصل بتاريخ 18 أبريل 2016. تم الاطلاع عليه بتاريخ 5 مايو 2018 .
  2. 1 2 هاندي، أليكس (24 أغسطس 2010). "عملة Skein المشفرة المشتقة من Ada تُظهر SPARK" . صحيفة SD Times . شركة BZ Media LLC . تم الاطلاع عليه في 31 أغسطس 2010 .
  3. 1 2 3 4 5 6 7 8 9 10 تشابمان، رودريك؛ دروس، كلير؛ ماثيوز، ستيوارت؛ موي، يانيك (مارس 2024). "البرامج المطورة بشكل مشترك وإثبات صحتها" . مجلة اتصالات رابطة مكائن ​​الحوسبة . 67 (3): 84-94 . doi : 10.1145/3624728 .
  4. 1 2 3 4 روس، فيليب إي. (سبتمبر 2005). "المبيدون" . مجلة IEEE Spectrum . 42 (9): 36-41 . doi : 10.1109/MSPEC.2005.1502527 . ISSN 0018-9235 . S2CID 26369398 .  
  5. ↑ "SPARK – نواة SPADE Ada (بما في ذلك RavenSPARK)" . AdaCore . تم الاطلاع عليه بتاريخ 30 يونيو 2021 .
  6. 1 2 3 4 5 تشابمان، رودريك (ديسمبر 2000). "التجربة الصناعية مع SPARK". رسائل ACM SIGAda Ada . XX (4): 64–68 . doi : 10.1145/369264.369270 .
  7. ↑ براندون، كارل س. (2013). "برمجيات كيوب سات عالية الموثوقية مع SPARK/Ada" (ملف PDF) . iCubeSat.org . تاريخ الاسترجاع: 20 ديسمبر 2025 .
  8. ↑ "تأمين مستقبل السلامة والأمن للبرمجيات المدمجة" . 8 يناير 2020.
  9. ↑ زابروكي، آدم؛ ميتيتش، ماركو (8 أغسطس 2025). "كيفية تأمين نظام بيئي فريد يضم أكثر من مليار نواة؟" (ملف PDF) . تم الاطلاع عليه بتاريخ 13 أغسطس 2025 .{{cite web}}: CS1 maint: url-status ( link )
  10. ↑ "SPARKNaCl" . GitHub . 8 أكتوبر 2021.

للمزيد من القراءة

  • بارنز، جون (2012). سبارك: المنهج المُثبت لبرمجيات عالية الموثوقية . ألتران براكسيس. ISBN 978-0-9572905-1-8أُرشف من الأصل في 14 أكتوبر 2016. تم الاطلاع عليه في 31 ديسمبر 2014 .