تحليل البرنامج الساكن
عودة للموسوعة| عملية تطوير البرمجيات | |
|---|---|
| نشاطات وخطوات | |
|
المتطلبات · مواصفة وظيفية البنيان · تصميم البرمجيات التطبيق · الفحص نشر البرمجيات · صيانة البرمجيات | |
| منهجيات | |
|
أجيل · هندسة برمجيات الغرفة النظيفة · Iterative RAD · RUP · Spiral Waterfall · XP · Lean سكرم · V-Model · TDD | |
| اختصاصات داعمة | |
|
إدارة تكوين البرمجيات توثيق البرمجيات ضمان الجودة Project management تصميم تجربة المستخدم | |
| أدوات | |
|
المصرف · المصحح · Profiler GUI designer · ب ت م | |
تحليل البرامج الساكن (بالإنجليزية: Static program analysis) هوتحليل لبرمجيات الحاسوب يُجرى دون تطبيق البرامج عمليًا، على عكس التحليل الديناميكي، الذي يُجرى على البرامج أثناء تطبيقها. يُجرى التحليل في معظم الحالات على بعض إصدارات الكود المصدري، أوعلى بعض أشكال الكود الهدف في حالات أخرى.
يطبق هذا المصطلح عادةً على التحليل المنفذ بواسطة أداة تلقائية، يسمى التحليل البشري فهم البرنامج أوإدراك البرنامج أومراجعة الكود. وتُستخدم في الحالة الأخيرة عمليات فحص البرمجيات وتقديم البرمجيات.
السبب المنطقي لاستخدامه
يختلف مدى تطور التحليل الذي تنفذه الأدوات من التي تبحث في سلوك التعليمات والتصريحات الفردية فقط، إلى التي تتضمن الكود المصدري الكامل للبرنامج في تحليلها. تختلف استخدامات المعلومات الناتجة عن التحليل من تميز أخطاء الترميز المحتملة (مثل، أداة لنت) إلى الأساليب الرسمية التي تثبت رياضيًا خواص برنامج معين (يتوافق سلوكه مع مواصفاته مثلًا).
يمكن وصف المقاييس البرمجية والهندسة العكسية كأشكال من التحليل الساكن. يتزايد نشر المقاييس البرمجية المشتقة والتحليل الساكن معًا، خاصةً في إنشاء أنظمة مضمنة، من خلال تعريف ما يسمى أهداف جودة البرمجيات.
هناك استخدام تجاري متزايد للتحليل الساكن في التحقق من خصائص البرمجيات المستخدمة في الأنظمة الحاسوبية الحساسة للسلامة وتحديد مسقط الكود الضعيف المحتمل. مثلًا، حددت الصناعات التالية استخدام تحليل الكود الساكن كوسيلة لتحسين نوعية البرمجيات المعقدة والمتطورة بصورة متزايدة:
- البرمجيات الطبية: حددت إدارة الغذاء والدواء الأمريكية (إف دي إيه) استخدام التحليل الساكن للأجهزة الطبية.
- البرمجيات النووية: يوصي مخط التنظيم النووي في المملكة المتحدة باستخدام التحليل الساكن لأنظمة حماية المفاعل.
- برمجيات الطيران (إلى جانب التحليل الديناميكي).
أشارت دراسة أجرتها شركة فيّ دي سي ريسيرش عام 2012 إلى حتى 28.7% من مهندسي البرمجيات المضمنة المشمولين بالاستقصاء يستخدمون حاليًا أدوات التحليل الساكن ومن المتسقط حتى يستخدمه 39.7% في غضون عامين. وجدت دراسة من عام 2010 حتى 60% من المطورين الذين جرت لقاءتهم في مشاريع بحثية أوروبية استفادوا على الأقل من برامج التحليل الساكن المدمجة في بيئة التطوير المتكامل الخاصة بهم. واستخدم نحو10% فقط أداة تحليل أخرى (ربما أكثر تطوراً).
يستخدم في مجال صناعة أمن التطبيقات أيضًا ما يسمى اختبار أمن التطبيقات الساكن (إس إيه إس تي). يعتبر اختبار أمن التطبيقات الساكن جزءًا مهمًا من دورة حياة تطوير الأمن (إس دي إل) مثل دورة حياة تطوير الأمن من مايكروسوفت، وهوممارسة شائعة في شركات البرمجيات.
أنواع الأدوات
نشرت مجموعة إدارة الهدف (أوإم جي) دراسة تتعلق بأنواع تحليل البرمجيات المطلوب لقياس جودة البرمجيات وتقييمها. يصف هذا المستند عن «كيفية تسليم أنظمة تكنولوجيا معلومات المرنة والآمنة والفعالة وسهلة التغيير وفقًا لتوصيات اتحاد جودة برمجيات تكنولوجيا المعلومات (سي إس آي كيو)» ثلاثة مستويات من تحليل البرمجيات.
مستوى الوحدة
التحليل الذي يتم داخل برنامج أوروتين فرعي معين، دون الاتصال بسياق ذلك البرنامج.
المستوى التقني
التحليل الذي يراعي التفاعلات بين برامج الوحدة للحصول على رؤية أكثر شمولية ودلالية للبرنامج الكلي للعثور على المشاكل وتجنب النتائج الإيجابية الزائفة الواضحة. مثلًا، يمكن تحليل حزمة تقنية أندرويد بشكل ساكن للعثور على أخطاء الأذونات.
مستوى النظام
التحليل الذي يراعي التفاعلات بين برامج الوحدة، لكن دون تقيد بتقنية أولغة برمجة واحدة محددة.
يمكن تعريف مستوى آخر من تحليل البرمجيات.
مستوى المهمة/العمل
التحليل الذي يراعي مصطلحات وقواعد وعمليات طبقة العمل/المهمة المنفذة ضمن نظام البرمجيات لتشغيله كجزء من أنشطة طبقة المؤسسة أوالبرنامج/المهمة. تُنفذ هذه العناصر دون تقيدها بتكنولوجيا أولغة برمجة محددة، وتوزع في حالات كثيرة على لغات متعددة، لكنها تُستخرج وتُحلل بشكل ساكن لفهم النظام وبالتالي لضمان المهمة.
الأساليب الشكلية
الأساليب الشكلية هي المصطلح المطبق على تحليل البرمجيات (والعتاد الحاسوبي) الذي تُستخدم أساليب رياضية دقيقة حصرًا للحصول على نتائجه. تضم التقنيات الرياضية المستخدمة دلالات ترميزية، ودلالات بديهية، ودلالات تشغيلية والتفسير المجرد.
يمكن من خلال الحد المباشر لمسألة التوقف، إثبات حتى عثور (أي لغة كاملة حسب تورينغ) على جميع أخطاء زمن التطبيق المحتملة في برنامج كيفي (أوأي نوع من خرق المواصفات في النتيجة النهائية للبرنامج عمومًا) غير قابل للحسم: لا توجد طريقة آلية يمكنها دائمًا الإجابة بصدق عمّا إذا كان البرنامج الكيفي سيظهر أولن يظهر أخطاء زمن التطبيق. تعود هذه النتائج إلى أعمال تشرتش وغودل وتورنغ في ثلاثينيات القرن العشرين (انظر: مسألة التوقف ونظرية رايس). مثل الكثير من الأسئلة غير القابلة للحسم، يمكن محاولة تقديم حلول تقريبية مفيدة.
تتضمن بعض تقنيات تطبيق التحليل الساكن الشكلي ما يلي:
- التفسير المجرد، لنمذجة تأثير جميع تعليمة على حالة الآلة المجردة (أي «يُنفذ» البرمجيات بناءً على الخصائص الرياضية لكل تعليمة وتصريح). تقارب هذه الآلة المجردة سلوكيات النظام بشكل مفرط: وبالتالي يصبح نظام المجرد أسهل في التحليل، على حساب عدم الاكتمال (ليس جميع خاصية حقيقية في النظام الأصلي حقيقة في النظام المجرد). ولكن إذا أُجري التفسير المجرد على النحوالسليمقد يكون سليمًا (يمكن تعيين جميع خاصية حقيقية للنظام التجريدي إلى خاصية حقيقية للنظام الأصلي). يعتمد ملحق تحليل قيمة إطار التحليل المعياري لبرامج سي (فريما سي). وأداة التحليل بوليسبيس بشدة على التفسير المجرد.
- تحليل تدفق البيانات، تقنية تعتمد على الشبكية لجمع المعلومات عن مجموعة القيم المحتملة؛
- منطق هور، نظام شكلي مع مجموعة من القواعد المنطقية للتفكير بدقة حول صحة برامج الحاسوب. يوجد أداة دعم لبعض الغات البرمجة (مثل لغة البرمجة سبارك (مجموعة فرعية من لغة البرمجة أيدا) ولغة جافا للنمذجة -جاي إم إل- باستخدام المدقق الساكن الموسع للجافا (إي إس سي/ جافا) والمدقق الساكن الموسع لجافا 2 ومحلق إطارالتحليل المعياري لبرامج سي ذات الشرط المسبق الأضعف (دبليوبّي) للغة سي الموسعة بلغة المحاكاة المستمرة المتقدمة إيه سي إس إل (لغة مواصفات سي حسب المعهد الوطني الأمريكي للمعايير/آيزو).
- التحقق من النموذج، يراعي الأنظمة ذات الحالات المنتهية أويمكن اختزالها إلى حالة منتهية عن طريق التجريد؛
- التطبيق الرمزي، مستخدم أيضًا لاشتقاق العبارات الرياضية التي تمثل قيمة المتغيرات المتحولة عند نقاط معينة في الكود.
تحليل ساكن مُساق بالبيانات
يستخدم التحليل الساكن المساق بالبيانات كميات كبيرة من التعليمات البرمجية لاستنتاج قواعد الترميز. مثلًا، يمكن استعمال جميع حزم جافا مفتوحة المصدر في مسقط غيت هاب لتفهم استراتيجية تحليل جيدة. يمكن لقاعدة الاستدلال حتى تستخدم تقنيات التفهم الآلي. فمثلُا، تبين أنه عندما ينحرف كثيرًا عن طريقة استخدام قابلة برمجة التطبيقات كائنية التوجه، فمن المحتمل حتىقد يكون هذا خطأ برمجي. من الممكن أيضًا التفهم من الإصلاحات والتحذيرات السابقة الكثيرة.
انظر أيضًا
- فهم الدلالة الشكلي
مراجع
- ^ Wichmann, B. A.; Canning, A. A.; Clutterbuck, D. L.; Winsbarrow, L. A.; Ward, N. J.; Marsh, D. W. R. (Mar 1995). "Industrial Perspective on Static Analysis" (PDF). Software Engineering Journal: 69–75. مؤرشف من الأصل (PDF) في 27 سبتمبر 2011.
- ^ "Software Quality Objectives for Source Code" نسخة محفوظة 2015-06-04 على مسقط واي باك مشين. (PDF). Proceedings: Embedded Real Time Software and Systems 2010 Conference, ERTS2010.org, Toulouse, France: Patrick Briand, Martin Brochet, Thierry Cambois, Emmanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Loic Noury, Philippe Spozio, Frederic Retailleau.
- ^ نسخة محفوظة 2011-06-05 على مسقط واي باك مشين. (PDF), Benjamin Livshits, section 7.3 "Static Techniques for Security". Stanford doctoral thesis, 2006.
- ^ FDA (2010-09-08). "Infusion Pump Software Safety Research at FDA". Food and Drug Administration. مؤرشف من الأصل في 01 سبتمبر 2010. اطلع عليه بتاريخ 09 سبتمبر 2010.
- ^ Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, "Computer based safety systems" (PDF). مؤرشف من الأصل (PDF) في January 4, 2013. اطلع عليه بتاريخ 15 مايو2013.
- ^ Position Paper CAST-9. Considerations for Evaluating Safety Engineering Approaches to Software Assurance نسخة محفوظة 2013-10-06 على مسقط واي باك مشين. // FAA, Certification Authorities Software Team (CAST), January, 2002: "Verification. A combination of both static and dynamic analyses should be specified by the applicant/developer and applied to the software."
- ^ VDC Research (2012-02-01). "Automated Defect Prevention for Embedded Software Quality". VDC Research. مؤرشف من الأصل في 11 أبريل 2012. اطلع عليه بتاريخعشرة أبريل 2012.
- ^ Prause, Christian R., René Reiners, and Silviya Dencheva. "Empirical study of tool support in highly distributed research projects." Global Software Engineering (ICGSE), 2010 5th IEEE International Conference on. IEEE, 2010 http://ieeexplore.ieee.org/ielx5/5581168/5581493/05581551.pdf
- ^ M. Howard and S. Lipner. The Security Development Lifecycle: SDL: A Process for Developing Demonstrably More Secure Software. Microsoft Press, 2006. (ردمك 978-0735622142)
- ^ Achim D. Brucker and Uwe Sodan. Deploying Static Application Security Testing on a Large Scale نسخة محفوظة 2014-10-21 على مسقط واي باك مشين.. In GI Sicherheit 2014. Lecture Notes in Informatics, 228, pages 91-101, GI, 2014. "Archived copy" (PDF). مؤرشف (PDF) من الأصل في 21 أكتوبر 2014. اطلع عليه بتاريخ 20 مايو2015. صيانة CS1: الأرشيف كعنوان (link)
- ^ "Archived copy" (PDF). مؤرشف (PDF) من الأصل في 28 ديسمبر 2013. اطلع عليه بتاريخ 18 أكتوبر 2013. صيانة CS1: الأرشيف كعنوان (link)
- ^ Bartel, Alexandre; Klein, Jacques; Monperrus, Martin; Le Traon, Yves (1 June 2014). "Static Analysis for Extracting Permission Checks of a Large Scale Framework: The Challenges and Solutions for Analyzing Android". IEEE Transactions on Software Engineering. 40 (6): 617–632. arXiv:1408.3976. doi:10.1109/tse.2014.2322867. مؤرشف من الأصل في 17 مايو2020.
- ^ Vijay D’Silva; et al. (2008). "A Survey of Automated Techniques for Formal Software Verification" (PDF). Transactions On CAD. مؤرشف (PDF) من الأصل في 04 مارس 2016. اطلع عليه بتاريخ 11 مايو2015.
- ^ Jones, Paul (2010-02-09). "A Formal Methods-based verification approach to medical device software analysis". Embedded Systems Design. مؤرشف من الأصل فيعشرة يوليو2011. اطلع عليه بتاريخ 09 سبتمبر 2010.
- ^ "Learning from other's mistakes: Data-driven code analysis". www.slideshare.net (باللغة الإنجليزية). مؤرشف من الأصل في 15 يناير 2017.
- ^ Oh, Hakjoo; Yang, Hongseok; Yi, Kwangkeun (2015). "Learning a strategy for adapting a program analysis via bayesian optimisation". Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2015. صفحات 572–588. doi:10.1145/2814270.2814309. ISBN .
- ^ Monperrus, Martin; Mezini, Mira (2013). "Detecting missing method calls as violations of the majority rule". ACM Transactions on Software Engineering and Methodology. 22 (1): 1–25. arXiv:1306.0762. doi:10.1145/2430536.2430541. مؤرشف من الأصل في 26 أبريل 2019.
التصنيفات: عملية تطوير البرمجيات, اختبار البرمجيات, ضمان الجودة, قالب أرشيف الإنترنت بوصلات واي باك, صيانة CS1: الأرشيف كعنوان, صفحات بها مراجع بالإنجليزية (en), مقالات تحتوي نصا بالإنجليزية, بوابة برمجيات/مقالات متعلقة, بوابة برمجة الحاسوب/مقالات متعلقة, جميع المقالات التي تستخدم شريط بوابات
