تحليل البرامج الثابتة

في علوم الحاسوب ، يُعرف تحليل البرامج الثابت (المعروف أيضًا بالتحليل الثابت أو المحاكاة الثابتة ) بأنه تحليل برامج الحاسوب دون تنفيذها، وذلك على عكس تحليل البرامج الديناميكي الذي يُجرى على البرامج أثناء تنفيذها في بيئة متكاملة. ^{[ 1 ] [ 2 ]}

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

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

لا ينبغي الخلط بين علم التحليل الثابت وعلم التدقيق اللغوي ، وهو عملية التحقق من أخطاء أسلوب البرمجة .

تتفاوت درجة تعقيد التحليل الذي تُجريه الأدوات، فمنها ما يقتصر على دراسة سلوك العبارات والتصريحات الفردية، ^{[ 4 ]} ومنها ما يشمل تحليله كامل شفرة المصدر للبرنامج. وتتنوع استخدامات المعلومات المُستقاة من التحليل، بدءًا من تسليط الضوء على أخطاء البرمجة المحتملة (مثل أداة lint ) وصولًا إلى الأساليب الرسمية التي تُثبت رياضيًا خصائص برنامج مُعين (مثل تطابق سلوكه مع مواصفاته).

يمكن وصف مقاييس البرمجيات والهندسة العكسية بأنهما شكلان من أشكال التحليل الثابت. ويجري استخدام استخلاص مقاييس البرمجيات والتحليل الثابت معًا بشكل متزايد، لا سيما في إنشاء الأنظمة المدمجة، من خلال تحديد ما يسمى بأهداف جودة البرمجيات . ^{[ 5 ]}

يتزايد استخدام التحليل الثابت تجاريًا في التحقق من خصائص البرمجيات المستخدمة في أنظمة الحاسوب بالغة الأهمية للسلامة، وتحديد الثغرات البرمجية التي قد تكون عرضة للاختراق . ^{[ 6 ]} على سبيل المثال، اعتمدت الصناعات التالية على التحليل الثابت للبرمجيات كوسيلة لتحسين جودة البرمجيات المتطورة والمعقدة بشكل متزايد:

1. البرمجيات الطبية : حددت إدارة الغذاء والدواء الأمريكية (FDA) استخدام التحليل الثابت للأجهزة الطبية. ^{[ 7 ]}
2. البرمجيات النووية: في المملكة المتحدة، يوصي مكتب التنظيم النووي (ONR) باستخدام التحليل الثابت لأنظمة حماية المفاعلات . ^{[ 8 ]}
3. برامج الطيران (بالتزامن مع التحليل الديناميكي ). ^{[ 9 ]}
4. السيارات والآلات (تشكل ميزات السلامة الوظيفية جزءًا لا يتجزأ من كل مرحلة من مراحل تطوير منتجات السيارات، ISO 26262 ، القسم 8).

أفادت دراسة أجرتها شركة VDC Research عام 2012 أن 28.7% من مهندسي البرمجيات المدمجة الذين شملهم الاستطلاع يستخدمون أدوات التحليل الثابت، وأن 39.7% منهم يتوقعون استخدامها خلال عامين. ^{[ 10 ]} ووجدت دراسة أخرى أجريت عام 2010 أن 60% من المطورين الذين شملهم الاستطلاع في مشاريع بحثية أوروبية استخدموا على الأقل أدوات التحليل الثابت الأساسية المدمجة في بيئات التطوير المتكاملة (IDE). ومع ذلك، لم يستخدم سوى 10% منهم أداة تحليل إضافية (وربما أكثر تطورًا). ^{[ 11 ]}

في مجال أمن التطبيقات ، يُستخدم مصطلح اختبار أمان التطبيقات الثابت (SAST). يُعدّ اختبار أمان التطبيقات الثابت جزءًا أساسيًا من دورات حياة تطوير الأمان (SDLs)، مثل دورة حياة تطوير الأمان التي حددتها مايكروسوفت ^{[ 12 ]} ، وهو ممارسة شائعة في شركات البرمجيات. ^{[ 13 ]}

نشرت مجموعة إدارة الكائنات (OMG ) دراسةً حول أنواع تحليل البرمجيات المطلوبة لقياس جودة البرمجيات وتقييمها. وتصف هذه الوثيقة، بعنوان "كيفية تقديم أنظمة تقنية معلومات مرنة وآمنة وفعّالة وسهلة التغيير بما يتماشى مع توصيات CISQ"، ثلاثة مستويات لتحليل البرمجيات. ^{[ 14 ]}

مستوى الوحدة

التحليل الذي يتم داخل برنامج أو روتين فرعي محدد، دون الاتصال بسياق ذلك البرنامج.

المستوى التكنولوجي

تحليل يأخذ في الاعتبار التفاعلات بين برامج الوحدات للحصول على رؤية أكثر شمولية ودلالية للبرنامج ككل من أجل إيجاد المشكلات وتجنب النتائج الإيجابية الخاطئة الواضحة .

مستوى النظام

تحليل يأخذ في الاعتبار التفاعلات بين البرامج الوحدوية، ولكن دون أن يقتصر على تقنية أو لغة برمجة محددة.

يمكن تحديد مستوى آخر من تحليل البرمجيات.

مستوى المهمة/الأعمال

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

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

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

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

تتضمن بعض تقنيات تنفيذ التحليل الثابت الرسمي ما يلي: ^{[ 15 ]}

• التفسير المجرد ، لنمذجة تأثير كل عبارة على حالة آلة مجردة (أي أنها "تنفذ" البرنامج بناءً على الخصائص الرياضية لكل عبارة وتصريح). تُقارب هذه الآلة المجردة سلوكيات النظام بشكل مفرط: مما يُسهّل تحليل النظام المجرد، على حساب عدم الاكتمال (ليست كل خاصية صحيحة في النظام الأصلي صحيحة في النظام المجرد). مع ذلك، إذا تم تطبيقه بشكل صحيح، يكون التفسير المجرد سليمًا (يمكن ربط كل خاصية صحيحة في النظام المجرد بخاصية صحيحة في النظام الأصلي). ^{[ 16 ]}
• تحليل تدفق البيانات ، وهو أسلوب قائم على الشبكة لجمع المعلومات حول مجموعة القيم المحتملة؛
• منطق هوار ، وهو نظام رسمي يتضمن مجموعة من القواعد المنطقية للاستدلال بدقة حول صحة برامج الحاسوب . يتوفر دعم للأدوات لبعض لغات البرمجة (مثل لغة البرمجة SPARK (وهي مجموعة فرعية من Ada ) ولغة نمذجة جافا - JML - باستخدام ESC/Java و ESC/Java2 ، ومكون Frama-C WP ( أضعف شرط مسبق ) الإضافي للغة C الممتد باستخدام ACSL ( لغة مواصفات ANSI/ISO C )).
• تعتبر عملية التحقق من النموذج الأنظمة التي لها حالة محدودة أو يمكن اختزالها إلى حالة محدودة عن طريق التجريد ؛
• التنفيذ الرمزي ، كما هو مستخدم لاستخلاص التعبيرات الرياضية التي تمثل قيمة المتغيرات المتغيرة في نقاط معينة في الكود.
• تحليل المرجع القابل للتصفير

يستفيد التحليل الثابت القائم على البيانات من قواعد بيانات برمجية واسعة النطاق لاستنتاج قواعد البرمجة وتحسين دقة التحليل. ^{[ 17 ] [ 18 ]} على سبيل المثال، يمكن استخدام جميع حزم جافا مفتوحة المصدر المتوفرة على GitHub لتعلم استراتيجيات تحليل جيدة. ويمكن استخدام تقنيات التعلم الآلي لاستنتاج القواعد. ^{[ 19 ]} كما يمكن التعلم من عدد كبير من الإصلاحات والتحذيرات السابقة. ^{[ 17 ]}

تُصدر أدوات التحليل الثابتة تحذيرات. بالنسبة لأنواع معينة من هذه التحذيرات، من الممكن تصميم وتنفيذ تقنيات معالجة آلية . على سبيل المثال، اقترح لوغوزو وبال معالجات آلية لـ cccheck في لغة C# . ^{[ 20 ]}

• أيواه، ناثانيال؛ هوفماير، ديفيد؛ مورغنثالر، ج. ديفيد؛ بينيكس، جون؛ بو، ويليام (2008). "استخدام التحليل الثابت لاكتشاف الأخطاء". مجلة IEEE للبرمجيات . 25 (5): 22-29 . CiteSeerX 10.1.1.187.8985 . doi : 10.1109/MS.2008.130 . S2CID 20646690 .  
• برايان تشيس، جاكوب ويست (فورتيفاي سوفتوير) (2007). البرمجة الآمنة باستخدام التحليل الثابت . أديسون-ويسلي. ISBN 978-0-321-42477-8.
• فليمنج نيلسون؛ هان ر. نيلسون؛ كريس هانكين (10 ديسمبر 2004). مبادئ تحليل البرامج (طبعة 1999 (مصححة 2004)  ). سبرينغر. ISBN 978-3-540-65410-0.
• "التفسير المجرد والتحليل الثابت"، المدرسة الشتوية الدولية حول علم الدلالة والتطبيقات 2003، بقلم ديفيد أ. شميدت