runtimeverification/kernel-c-to-rust-spikeتحصين محللات لغة C في النواة عبر إعادة كتابتها بلغة Rust + الاختبار العشوائي التفاضلي + التحقق الرسمي. الهدف الأول: UVC (CVE-2024-53104).
هل يمكن تقوية محلل C أمني حرج في نواة Linux عبر إعادة كتابته بلغة Rust، مع إثبات تكافؤ إعادة الكتابة مع الأصل ثم التحقق منها رسميًا؟ تُجري هذه التجربة الحلقة الكاملة على هدف واحد: محلل أوصاف فيديو UVC (uvc_parse_format/uvc_parse_frame من drivers/media/usb/uvc/، الإصدار v7.2-rc2)، وقد اختير لأنه حمل ثغرتين مستقلتين من فئة أمان الذاكرة (CVE) تفصل بينهما ستة عشر عامًا (CVE-2008-3496، وCVE-2024-53104، والأخيرة مدرجة في كتالوج CISA KEV).
استخراج ورقة C (c/). نُسخت منطق التحليل حرفيًا من النواة؛ ولم يُستبدل سوى البيئة (// SPIKE-STUB). يُترجم إلى مكتبة بواجهة C-ABI. تتضمن الورقة المستخرجة تمريرة العدّ والتخصيص المُقاس، لذا فإن فئة خطأ CVE-2024-53104 (كتابة التحليل بما يتجاوز ما خصصه العدّ) قابلة للوصول، لا مجرّدة.
إعادة الكتابة بلغة Rust (rust/). نفس ورقة التحليل بلغة Rust آمنة، بنفس واجهة C-ABI وبنية النتيجة. كل انحراف عن C موسوم بـ // DEVIATION وموثّق.
الاختبار التبايني التلقائي (fuzzing) (fuzz/). أداة LibAFL على rustc المستقر تشغّل كلا التطبيقين من مدخل واحد وتقارن المخرجات حقلًا بحقل. النتيجة: بعد إصلاح عدم تطابق واحد في نقل الكود عند موضع تجاوز إشارة يعتمد على المترجم، صفر اختلافات على 54,019 تنفيذًا بتغطية حواف 93%. على كود v7.2-rc2 الأمين لا يمكن الوصول إلى أي وصول خارج الحدود (كلتا الثغرتين مُرقّعتان). يعيد عنصر تحكم سلبي اختياري (--features vuln، منعكس في كلتا اللغتين) إدخال عدم التطابق الخاص بـ CVE-2024-53104: على المدخل نفسه يقوم C بكتابة خارج حدود الكومة (ASan)، بينما تتعطل Rust بأمان. التفاصيل: fuzz/RESULTS.md.
التحقق الرسمي (verify/). تُستخرج ورقة Rust الأمينة عبر Charon وAeneas إلى Lean 4 دون أي sorry في الكود المولّد، ودون عائق union (بخلاف تجربة Binder). مبرهنتان، في verify/VERIFY-REPORT.md وROADMAP.md:
ok / fail مُتحكَّم به / عدم إنهاء، وليست أبدًا نتيجة سلوك غير معرّف): مُبرهَنة، خالية من sorry. وهذا يجعل خاصية أمان الذاكرة التي يفتقر إليها C صريحة كعبارة مُتحقَّق منها.sorry، إلى جانب مبدأين قابلين لإعادة الاستخدام لاستدلال الحلقات في Aeneas وخلوّ من القسمة للحلقات الخمس المنتهية بنيويًا. ويُختزل الباقي إلى نواة صحة وظيفية مسماة للمشي الموضعي (أربع مبرهنات مساعدة معلنة)؛ انظر ROADMAP.md.الحلقة مُبرهَنة من البداية إلى النهاية على هدف واحد. أُثبت تكافؤ إعادة الكتابة مع C عبر الاختبار التبايني التلقائي؛ وأصبح فرق أمان الذاكرة ملموسًا بفضل عنصر التحكم السلبي؛ وتُستخرج Rust بنظافة إلى Lean وتُفحص خاصية السلامة الكلية آليًا. أما مبرهنة عدم التعطل، فقد ثُبتت ثابتة العدّ (جوهر CVE-2024-53104) خالية من sorry، واختُزل العمل المتبقي إلى نواة صحة وظيفية مسماة، معلنة لكن غير مُبرهَنة بعد. حالة الإثبات الكاملة والمبرهنات المساعدة المفتوحة في ROADMAP.md.
c/ — ورقة C المستخرجة وبيئاتها البديلةrust/ — إعادة الكتابة بلغة Rust الآمنةfuzz/ — أداة LibAFL للاختبار التبايني التلقائي، والنتائج، وعنصر التحكم بفئة CVEverify/ — استخراج Charon/Aeneas/Lean والمبرهناتROADMAP.md — حالة الإثبات والمبرهنات المساعدة المفتوحة المتبقيةOPEN_CHALLENGES.md — مهام ملموسة يمكن للمساهم أن يلتقطها*/README.md، fuzz/RESULTS.md، verify/VERIFY-REPORT.md — تفاصيل كل مرحلةنواة v7.2-rc2 (مرجع للقراءة فقط). Rust المستقر 1.94.0. LibAFL 0.15. Charon 909ff09a (v0.1.220، --preset=aeneas)، Aeneas c2015b86، Lean/mathlib v4.31.0.