تُحدث النماذج اللغوية الكبيرة ثورة في جعل التحقق الرسمي من البرمجيات ممكنًا على نطاق أوسع بكثير

Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross

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

المقدمة

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

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

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

لكن نماذج LLM تجعل الأمر أسهل بكثير. فالنماذج الرائدة أصبحت الآن قادرة على إنتاج براهين صحة للبرمجيات الواقعية بشكل مستقل تمامًا. ولإظهار ذلك، طلبنا من Claude إثبات خصائص أمنية مفيدة عبر 123 مكتبة مفتوحة المصدر، بما في ذلك إثبات أن بعض مخرجاتها التنفيذية يمكنها ألا تنهار أبدًا في ظل ظروف معينة. وتحديدًا، أثبت Claude أن هذه البرامج ستخرج دائمًا بشكل طبيعي دون إحداث أخطاء في سلامة الذاكرة أو فشل التأكيدات، لكل مدخل أقل من 64 ميغابايت ولكل استجابة لأنظمة لينكس المصممة نموذجيًا ولكل تخطيط للذاكرة، في ظل افتراضات معينة (أي أن البرنامج يعمل كملف ثنائي ثابت أحادي الخيوط بميزانية ذاكرة ثابتة على معالج RISC-V¹ CPU يعمل بنظام لينكس). ولا يزال هذا بعيدًا عن إصلاح كل الأخطاء الممكنة، لكنه يقربنا من ذلك أكثر بكثير من قبل ويوفر خارطة طريق نحو تلك الغاية.

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

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

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

في بقية هذه التدوينة، نغطي تجاربنا في التحقق الشكلي بمزيد من التفصيل.

تحويل الاختبارات إلى إثباتات

لإثبات أن قطعة من البرمجيات صحيحة، يجب أولًا أن نحدد ما تعنيه كلمة «صحيحة» أصلًا. تُعرَّف الصحة بواسطة المواصفات (spec). في بعض البرامج، توجد طريقة واضحة لتحديد السلوك المقصود للبرنامج شكليًا. على سبيل المثال، يأخذ مفكك PNG تسلسلًا من البايتات و(وفقًا لمعيار RFC 2083) يفك ترميز هذه البايتات إلى الصورة المقابلة. لكن بالنسبة لمعظم البرامج، ليست الأمور بهذه السهولة. ماذا يعني أن يكون محرر نصوص أو متصفح ويب «صحيحًا»؟ إن صعوبة الحصول على مواصفات شاملة وغير غامضة تمثل عقبة كبيرة أمام التحقق من البرمجيات على نطاق أوسع.

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

في هذا المشروع، بدأنا بـ اختبارات الفوضى (fuzz tests). في هذه الاختبارات، يكتب المطورون نقطة دخول² إلى أكوادهم تأخذ مدخلات، بحيث يكون أي مُدخل يتسبب في انهيار البرنامج خطأً يهتم به المؤلفون. ثم يولّد المولّد العشوائي، وهو محرك اختبار، أعدادًا هائلة من المدخلات شبه العشوائية والمطفّرة عند نقطة الدخول في محاولة للعثور على خطأ (كما هو موضح في الشكل 1). وكلما طال تشغيل المولّد العشوائي، وجد أخطاء أكثر. لكن هذا بطبيعته عملية بالقوة الغاشمة، بلا ضمان لتغطية كل مسار كود ممكن، مهما حاولت من مدخلات.

للعثور على جميع الأخطاء التي كان سيكشفها اختبار الضجيج (fuzz test)، حوّلنا اختبار الضجيج إلى مواصفة معرّفة فوق تعليمات RISC-V المُصرَّفة. تنص المواصفة على أن اختبار الضجيج لن يتعطل لأي مدخل أقل من 64 ميغابايت.³ إذا تمكن Claude من إثبات هذه المواصفة، يصبح اختبار الضجيج على RISC-V زائدًا عن الحاجة: اختبار الضجيج لنقطة الدخول هذه لن يجد أي أخطاء أبدًا.

فعلنا هذا لمئات المشاريع في مبادرة OSS-Fuzz الخاصة بشركة Google، والتي توفر اختبار ضجيج مستمرًا للمشاريع مفتوحة المصدر المؤهلة. يحتوي OSS-Fuzz على آلاف نقاط الدخول التي كتبها المطورون وتبحث عن خصائص شيفرة معطوبة من خلال التعطل (على سبيل المثال، عند فشل تأكيد assertion). يقوم OSS-Fuzz تلقائيًا بتجهيز برامج C و ++C بأداة AddressSanitizer⁴ (ASan)، مما يجعلها تتعطل كلما تم الوصول إلى الذاكرة بشكل غير صحيح (وهو سبب رئيسي لثغرات البرمجيات). المواصفات واسعة النطاق مثل أمان الذاكرة تنطبق على جميع البرمجيات تقريبًا.

على مدى بضعة أسابيع، نجح كلود في إصلاح الأخطاء التي عثر عليها، ثم أثبت عدم وجود أي انهيارات على أي مدخلات (حتى بحجم 64 ميغابايت) في 239 نقطة دخول عبر 123 مكتبة مختلفة من مكتبات OSS-Fuzz. تعمل هذه الإثباتات على تعليمات RISC-V المُجمَّعة (أي الملفات الثنائية التنفيذية)، وتتألف من نحو 180 مليون سطر من Rocq، حيث يصل الإثبات النموذجي إلى نحو 600,000 سطر لتوفير ضمانات أمنية على ملفات ثنائية يبلغ طولها الوسيط 18,000 تعليمة RISC-V. تُبنى هذه الإثباتات عن طريق ترجمة كود التجميع RISC-V إلى نموذج رياضي باستخدام دلالات Theorem لتعليمات RISC-V وعمليات Linux. وهذا يعني أن هذه الإثباتات تفترض حاليًا أن البرنامج يعمل كملف ثنائي ثابت أحادي الخيوط ضمن ميزانية ذاكرة ثابتة على معالج RISC-V يستخدم نظام تشغيل Linux. توسيع نطاق هذه الإثباتات أمر في المتناول تمامًا، إذ يتطلب توحيد الدلالات لمعماريات تجميع إضافية وعمليات أنظمة تشغيل أخرى. انظر رأي أحد الخبراء في الإثباتات التي كتبها كلود.

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

• النماذج الرسمية لمعمارية RISC-V ولعمليات Linux؛
• عبارات النظريات الدقيقة التي تم إثباتها؛
• مدقق إثباتات Rocq نفسه.⁵

لا يعني هذا أن هذه المكتبات خالية من الأخطاء. بل يعني أن أي أخطاء متبقية إما توجد ضمن العناصر المذكورة أعلاه أو خارج نطاق إثبات كلود. تعزيز تلك المكوّنات الموثوقة التي قد تكون معيبة بعد (Rocq، ودلالات RISC-V وLinux) ليس أمرًا بسيطًا، لكنه مهمة أكثر قابلية للإنجاز بكثير من تنقيح كل سطر من الأسطر البرمجية التي تغطيها الإثباتات الموسّعة — خاصة أن هذا النهج يمكنه تأمين عدد غير محدود من المشاريع دون زيادة حجم المكوّنات الموثوقة.

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

إيجاد الأخطاء وإصلاحها

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

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

الكثير من الأخطاء التي عثرنا عليها هي أخطاء يصعب على أداة الفوضوية (fuzzer) العثور عليها أبدًا. فالأدوات الفوضوية تحوّر مدخلات صغيرة، تقتصر عادةً على 1 ميغابايت، وتعتمد عادةً على تغطية الكود لتوجيهها نحو الأخطاء. أثناء إثبات نقطة دخول في إحدى المكتبات، عثر كلود على نقص تحت العدد (counter underflow) في نسخته من أداة فك الضغط أدى إلى كتابة خارج الحدود، ولكن فقط على مدخلات بحوالي 20 ميغابايت لها تخطيط نادر ومحدد. ومن الأخطاء الأخرى: قراءة خارج الحدود في وحدة فك ترميز الصور تتطلب مدخلًا بحجم 64 ميغابايت وأكثر من 2 غيغابايت من الذاكرة، وقراءة خارج الحدود في مكتبة أخرى تتطلب تسلسلًا معينًا من الاستدعاءات عبر مقبضين للملف نفسه، وإعادة اكتشاف CVE-2026-56132 في libexpat، والتي تتطلب مدخلات متداخلة بعمق. كما عثر كلود على أخطاء منطقية لا تسبب انهيارًا على الإطلاق. فعلى سبيل المثال، أثناء إثبات أمان ذاكرة إحدى المكتبات، لاحظ أن ميزة لتقييد الملفات التي يمكن للتطبيق تحميلها لا تُطبَّق دائمًا.

كان الهدف النهائي من هذا المشروع هو تحقيق إثبات بأن اختبارات الفوضوية المُجمَّعة بـ RISC-V لم يتبقَّ فيها أي انهيارات يمكن العثور عليها. ومع ذلك، تُظهر أخطاء مثل ما سبق أن للعملية فائدة أخرى، بغض النظر عما إذا كان ذلك الهدف قد تحقق: فمجرد محاولة هذه العملية تنتج أخطاء حقيقية تحتاج إلى إصلاح.

إثبات أكثر من مجرد أمان الذاكرة

إثبات أن اختبار الضوضاء (fuzz test) لا يجد المزيد من الأعطال أكثر أهمية مما يبدو. من الشائع أن تختبر اختبارات الضوضاء في الأكواد الواقعية انتهاكات خصائص عليا ذات معنى، مثل دورة الترميز-فك-الترميز، والخاصية الأحادية (idempotence)، والقوانين الجبرية، والاختبار التفاضلي، والاتساق الذاتي، أو التكافؤ مع التطبيقات المرجعية. على سبيل المثال، اختبار ضوضاء لخوارزمية الضغط LZO يتحقق من أنه إذا ضغطتَ مدخلاً ثم فك ضغطه، فإن النتيجة مطابقة للأصل. وإذا لم تتحقق الخاصية، يتعطل البرنامج—لذا فإن إثبات أن الاختبار لا يتعطل أبداً يعادل إثبات الخاصية نفسها.

يمكن أن يحدث هذا أيضاً حتى عندما لا تكون الخصائص محددة مباشرة من قبل المطوّر. على سبيل المثال, حتى يتمكن Claude من إكمال إثباته لـ OSS-Fuzz الخاص بمكتبة cpp-httplib, كان من الضروري استبعاد إمكانية تجاوز المكدس (stack overflow) بسبب التكرار المفرط في مدمّر std::set. هذا العمق التكراري محدود بالعمق الأقصى للشجرة, لذا كان على Claude أن يثبت (على لغة الآلة!) أن خوارزمية إعادة موازنة الشجرة الحمراء-السوداء في libc++ مُحسَّنة بشكل صحيح للحفاظ على عمق الشجرة محدوداً لوغاريتمياً.

دراسات حالة أخرى في التحقق الصوري

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

رأينا أيضاً نجاحاً في استخدام النماذج اللغوية الكبيرة مع التحقق الصوري بطرق أخرى. على سبيل المثال, طلبنا من Claude كتابة مواصفة صورية لـ RFC 1950, الوثيقة التقنية التي تُعرّف صيغة ملفات ضغط zlib. ثم طلبنا من Claude أن يثبت أن تطبيق zlib في نواة Linux يطبّق تلك المواصفة بشكل صحيح. كما في الأمثلة أعلاه, أثبت Claude هذه الخاصية على مستوى الثنائيات (binary), لكن بدلاً من RISC-V, أثبت Claude مباشرة الثنائي المُجمَّع لـ x86 باستخدام دلالات صورية مولَّدة من Claude (ومُختبَرة بكثافة) لمعمارية x86 ISA.⁷ ثم كررنا هذه العملية على نصف دزينة من المكتبات الأخرى المستخدمة على نطاق واسع. وDurante ذلك وجدنا بعض الأخطاء البسيطة (غير القابلة للاستغلال) في حالات حدّية، وهي قيد الإيداع لدى المطوّرين الأصليين. نستخلص من هذا التمرين نتيجتين: (1) قواعد الكود هذه المُختبَرة بكثافة شديدة صحيحة بالفعل تقريباً بالكامل، و(2) من الممكن إثبات خصائص صحة من البداية إلى النهاية حول قواعد كود حقيقية موجودة.

في تجربة أخرى، طلبنا من Claude تطوير مُفسِّر لمجموعة فرعية كبيرة من لغة Python بلغة Rust، وإثبات (باستخدام Verus، وهي أداة تحقق لـ Rust) أنه يلتزم بدلالات CPython الموضحة في ورقة أكاديمية. ثم قسنا الالتزام بسلوك CPython تجريبياً، عبر تشغيل أكثر من 1.7 مليون برنامج Python مولّد عشوائياً، ووجدنا سلوكاً مطابقاً لـ CPython في 99.95% من الاختبارات، مع اختلافات متبقية في الاختبارات كانت حالات حدّية معروفة وغير مدهشة.

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

انظر الملحق لمزيد من التفاصيل حول بعض هذه الجهود.

هذه مجرد البداية

أحد القيود الرئيسية للتحقق الصوري المدعوم بالنماذج اللغوية الكبيرة هو أن الإثباتات قد تتطلب مئات الملايين من الرموز (tokens) لإنتاجها. الكفاءة من حيث التكلفة حاسمة إذا كان هدفنا إتاحة هذه الأساليب لمنظومة البرمجيات بأكملها. ولحسن الحظ، هناك أسباب مقنعة لنتوقع تحسّن الكفاءة.

النماذج الأحدث تحتاج إلى رموز أقل

بنينا 36 مهمة تحقق صغيرة من كود OSS-Fuzz حقيقي. يثبت Opus 5.5 نصفها بنحو 40% رموز أقل من Opus 5. نتوقع أن يستمر هذا الاتجاه مع تدريب النماذج على مهام تحقق طويلة.

يمكن إعادة استخدام الإثباتات

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

لاحظنا الظاهرة نفسها تحدث على نطاق واسع خلال جهودنا لإثبات الصحة في OSS-Fuzz. معظم الإثبات يتعلق بشيفرة تحتويها كل البرامج (وبخاصة تهيئة بيئة تشغيل C وAddressSanitizer)، لذا يمكن لبرامج مختلفة تمامًا أن تنتهي بإثباتات متداخلة بشكل كبير. استفادت فرق الوكلاء من ذلك بنسخ إثبات مكتمل لفريق آخر ثم تكييفه مع برنامجها (الشكل 6).

إعادة استخدام الإثباتات بهذا الشكل هي الطريقة التي نما بها Mathlib، وهي مكتبة مشتركة للرياضيات الصورية في Lean، لتقترب من 300,000 theorem قدّمها أكثر من 700 مساهم: كل إثبات جديد يُبنى على جسد العمل القائم. راكمت جهودنا في OSS-Fuzz جسدًا مشابهًا من الإثباتات، بعضها ندرجه في إصدارنا (لا نقوم بإصدار الإثباتات التي قد تكشف عن ثغرة غير مرقّعة في البرمجيات مفتوحة المصدر).

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

يسهّل هذا النهج أيضًا إعادة استخدام الإثباتات على مستوى دقة الحزم، ما يعني أن كل اعتمادية تحتاج إلى التحقق منها مرة واحدة فقط. تتبع الاعتماديات قانون القوة: إثبات صحة حتى مجموعة صغيرة من المكتبات المشتركة يجعل شريحة واسعة جدًا من البرمجيات قابلة للإثبات. لمزيد من التفاصيل، انظر خارطة طريق Theorem للتحقق من صحة منظومة Nix بأكملها، والتي تشمل بنية تحتية حرجة مثل glibc وOpenSSL وcURL.

القيود

عمليًا، قد يثبت التحقق الصوري أحيانًا ما هو أقل مما نتمناه عن أمان الشيفرة.

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

الآلة الواقعية تفعل شيئًا لا يصفه النموذج. تتعلق إثباتاتنا بملفات ثنائية أحادية الخيوط وثابتة (static) لمعمارية RISC-V ومربوطة بمكتبة musl libc. غير أن معظم الناس يشغّلون هذه المكتبات على x86 أو ARM ويربطونها ديناميكيًا بـ glibc. لسد هذه الفجوة، نحتاج إلى نماذج أنظمة تشبه الأنظمة المنشورة أكثر. على سبيل المثال، خطوة في هذا الاتجاه ستكون توليد دلالات دقيقة لمعمارية x86.

قد لا يغطي الادعاء كل ما يهمّنا. أثبتنا أن الانهيار (crash) لا يحدث أبدًا لأي مدخل بحجم أقل من 64 ميغابايت في العديد من نقاط دخول الاختبار الضربوي في Google OSS-Fuzz، بما في ذلك انهيارات ASan. غير أن ASan لا يكتشف كل أخطاء أمان الذاكرة، ولم نتحقق من جميع نقاط الدخول لكل مكتبة. وحتى لو فعلنا، فلن يغطي التحقق من جميع نقاط الدخول المكتبة بأكملها (خاصة إذا وُجدت شيفرة ميتة). إضافةً إلى ذلك، قد تسيء البرامج الواقعية استخدام المكتبة، ما يؤدي إلى تلف في الذاكرة داخل الدالة المستدعية. لسد تلك الفجوة، سنحتاج إلى تحديد ما يجب على المستدعين فعله لكل دالة عامة، وأن يلتزم المستدعون بذلك التزامًا صارمًا.

نتوقع أنه مع تعلّم المزيد عن الاستفادة من نماذج اللغة الكبيرة في الأساليب الصورية، ومع استمرار تحسّن النماذج، ستصبح هذه القيود قابلة للمعالجة، وسنتمكن من التحقق من نسبة أكبر بكثير من الشيفرة التي نعتمد عليها.

الخلاصة

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

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

اقرأ الملحق الكامل.

الحواشي السفلية

01‏RISC-V هي تصميم معالج، مثل x86 أو ARM، يعرّف تعليمات التجميع (الأوامر الأساسية التي ينفذها الشريحة) التي تُترجَم إليها البرمجيات.

02نقطة الدخول هي باب أمامي إلى الشيفرة، يوفرها مؤلفوها لأغراض الاختبار. أي مُدخل إلى نقطة الدخول يتسبب في انهيار يُعد خطأً يهتم به المؤلفون.

03تتطلب زيادة هذا جهدًا بشريًا بسيطًا لتغيير المُعامل وإعادة توليد المواصفة، ثم جعل Claude يعيد إثبات العبارة.

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

05هذا يعني تقنيًا أيضًا أنه علينا أن نثق في العتاد ونظام التشغيل ومترجم OCaml الذي يعتمد عليها مُدقِّق إثباتات Rocq.

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

07نحن نرى أن قدرة Claude على—بشكل مستقل تمامًا—توليد الدلالات الشكلية لمعمارية ISA هي درس منفصل ومثير للاهتمام. وبينما لا يمكننا التأكد من أن دلالاتنا نفسها مثالية، فقد وجدنا عمليًا أن التنفيذ خطوة بخطوة عبر دلالاتنا يمكنه إقnak مساحة مستخدم لنظام Ubuntu فوق نواة Linux. وقد مكّن توليد هذه الدلالات أيضًا من اكتشاف مئات الأخطاء في وثائق المرجع الرسمية، بالإضافة إلى عدد أصغر من الأخطاء في العتاد نفسه.