Directed Symbolic Execution for Path Feasibility Analysis]{Directed Symbolic Execution for Path Feasibility Analysis in Software Security Testing
تقدم هذه الورقة طريقة تنفيذ رمزي موجه تعزز التحليل الأمني الساكن من خلال التحقق بكفاءة من إمكانية المسارات عبر الإجراءات باستخدام الرمزية الآلية وحدود تكرار الحلقات، مما يحسن الدقة بشكل كبير مع الحفاظ على الاستدعاء في الاختبارات المعيارية الواقعية.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تعد أمن البرمجيات معركة مستمرة ضد العيوب الخفية، تماماً مثل مخطط مدينة يحاول ضمان قدرة كل جسر ونفق في مدينة مترامية الأطراف على الصمود أمام زلزال. وللقيام بذلك، يستخدم المهندسون أدوات مؤتمتة تقوم بفحص الكود دون تشغيله فعلياً، مما يرسم خريطة لكل مسار محتمل يمكن أن يسلكه البرنامج. هذه الخرائط، المعروفة باسم رسوم تدفق التحكم (control flow graphs)، مفصلة للغاية، حيث توضح كيفية انتقال البرنامج من تعليمات إلى أخرى. ومع ذلك، غالباً ما تكون هذه الخرائط دقيقة أكثر من اللازم؛ فهي تسلط الضوء على مسارات تبدو خطيرة على الورق ولكنها مستحيلة التنفيذ في الواقع. وهذا يخلق فيضاً من الإنذارات الكاذبة، مما يجبر الخبراء البشريين على إضاعة الوقت في التحقيق في "أشباح داخل الآلة". التحدي إذن يكمن في بناء نظام يمكنه التمييز بسرعة بين المسار الذي هو مجرد احتمال نظري وبين المسار القابل للتنفيذ فعلياً، دون أن يضيع في حجم الاحتمالات الهائل.
قام فريق من الباحثين في الجامعة الروسية الأرمنية بتطوير طريقة جديدة لحل هذه المشكلة، باستخدام تقنية تسمى التنفيذ الرمزي الموجه (directed symbolic execution). تخيل مسافراً يحاول التحقق مما إذا كان هناك مسار محدد عبر مدينة معقدة. النهج التقليدي سيكون إرسال مستكشفين للمشي في كل شارع في المدينة لمعرفة إلى أين تؤدي، وهي مهمة قد تستغرق وقتاً طويلاً وتثقل كاهل الفريق. بدلاً من ذلك، يعمل نهج الباحثين مثل جولة سياحية موجهة؛ فهو يأخذ مساراً محدداً أبلغ عنه ماسح أمني ويوجه مستكشفاً افتراضياً لاتباع ذلك المسار فقط، متجاهلاً كل شارع آخر لا يؤدي إلى الوجهة. هذا النهج "الموجه" يسمح للنظام بالتحقق مما إذا كان الخطر المبلغ عنه حقيقياً دون إضاعة الطاقة في متاهات غير ذات ص relevance.
يكمن جوهر هذا العمل في كيفية تعامل النظام مع المجهول. في البرمجيات الحقيقية، غالباً ما تتعامل البرامج مع بيانات لم يتم تحديدها بعد، أو تستدعي وظائف من مكتبات خارجية حيث يكون الكود الداخلي مخفياً. قد يتعثر المستكشف التقليدي أو يستسلم عند مواجهة هذه الفراغات. ومع ذلك، فقد صُمم نظام الباحثين للتعامل مع هذه المجاهيل كمتغيرات مرنة. فإذا قرأ برنامج موقع ذاكرة لم يتم ملؤه بعد، يقوم النظام بتعيين قيمة رمزية له، مما يسمح باستكشاف كل نتيجة محتملة قد تتخذها تلك القيمة. وهو يفعل الشيء نفسه بالنسبة لنتائج الوظائف الخارجية ومعاملات المؤشرات (pointers) المعقدة، والتي تعمل كعناوين ديناميكية يمكن أن تشير إلى أماكن مختلفة اعتماداً على الموقف. ومن خلال ملء هذه الفجوات تلقائياً بالاحتمالات بدلاً من التخمينات الملموسة، يمكن للنظام تتبع المسار عبر الكود حتى عندما لا تكون الصورة الكاملة مرئية.
هناك عقبة رئيسية أخرى في التنقل عبر البرمجيات وهي "الحلقة" (loop)، وهي قسم من الكود يتكرر نفسه. في برنامج حقيقي، قد تعمل الحلقة بضع مرات أو ملايين المرات، وفي التحليل الرمزي، يمكن أن تحبس المستكشف في دورة لانهائية. قدم الباحثون استراتيجية للتعامل مع هذا الأمر من خلال وضع حد لعدد المرات التي سيتبع فيها النظام الحلقة قبل إجباره على الخروج. هذا ليس قطعاً عشوائياً؛ فالنظام يسجل بعناية ما حدث خلال تلك التكرارات ثم يقفز إلى النقطة التي تنتهي عندها الحلقة بشكل طبيعي. هذا يسمح للتحليل بالاستمرار بعد القسم المتكرر دون التعثر، مما يضمن قدرة الأداة على الوصول إلى نهاية المسار الذي تحقق منه.
لاختبار طريقتهم، طبق الفريق منهجهم على برمجيات حقيقية وعلى مجموعة معيارية من حالات الاختبار المعروفة باسم "جوليت سويت" (Juliet suite). قاموا أولاً بفحص نظامهم مقابل المسارات المستخرجة من "جي إن يو كوريوطيلز" (GNU Coreutils)، وهي مجموعة أساسية من الأدوات لنظام التشغيل لينكس. نجح النظام في التحقق من أن 95.3% من هذه المسارات الواقعية كانت بالفعل قابلة للتنفيذ، مما أثبت قدرته على التعامل مع الكود المتداخل والمعقد. ثم قاموا بدمج طريقتهم مع أداة أمنية موجودة تسمى MLH. قبل إضافة هذا الجزء، كانت الأداة ترفع 666 إنذاراً كاذباً من بين آلاف التقارير. وبعد تطبيق تحليل جدوى المسار الجديد، اختفت تلك الإنذارات الكاذبة تماماً، بينما استمرت الأداة في رصد كل ثغرة حقيقية وجدتها من قبل. وهذا يعني أن دقة الفحص الأمني قفزت من 56.6% إلى 100% على المجموعة المختبرة، دون أي فقدان في القدرة على اكتشاف الأخطاء الحقيقية.
كما قارن الباحثون نهجهم بـ KLEEF، وهي أداة متخصصة أخرى مصممة لمهام مماثلة. عند اختبارهم على التقارير الناتجة عن ماسحين أمنيين رئيسيين آخرين، وهما Infer وClang Static Analyzer، كانت النتائج صارخة. فقد واجه KLEEF صعوبة كبيرة، وفشل في التحقق من معظم التقارير الإيجابية الحقيقية، مما أدى إلى انخفاض درجات أدائه بشكل حاد. في المقابل، حافظت الطريقة الجديدة على أداء الماسحات الأصلية أو حسنت من أدائها قليلاً. لقد نجحت في التحقق من جميع الثغرات الحقيقية التي أبلغ عنها أداة Infer وتعاملت مع الغالبية العظمى من تقارير Clang، مما يدل على أنها قوية بما يكفي للعمل مع الكود ذي المعايير الصناعية.
تشير النتائج إلى أن هذا النهج الموجه يوفر طريقة عملية لتنقية الضجيج في اختبار أمن البرمجيات. فمن خلال التركيز فقط على المسارات المهمة والتعامل تلقائياً مع تعقيدات الذاكرة والوظائف الخارجية، يقوم المنهج بتصفية السيناريوهات المستحيلة التي تضيع وقت البشر. وبينما يقوم النظام بعملية مقايضة محسوبة من خلال تحديد تكرارات الحلقة للحفاظ على استمرارية العمل، إلا أن النتائج تظهر أن هذا لا يأتي على حساب تفويت المخاطر الحقيقية. يوفر هذا العمل مساراً واضحاً لجعل أدوات الأمن المؤتمتة أكثر موثوقية، مما يضمن أنه عندما يصدر تحذير، فإنه يمثل تهديداً حقيقياً يستحق التحقيق.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.