Kernel C-to-Rust हार्डनिंग स्पाइक: UVC डिस्क्रिप्टर पार्सर

क्या किसी सुरक्षा-महत्वपूर्ण Linux kernel C पार्सर को Rust में पुनः लिखकर हार्डन किया जा सकता है, जिसमें पुनर्लेखन को मूल के समतुल्य दिखाया जाए और फिर औपचारिक रूप से सत्यापित किया जाए? यह स्पाइक एक लक्ष्य पर पूरा चक्र चलाता है: UVC वीडियो डिस्क्रिप्टर पार्सर (drivers/media/usb/uvc/ से uvc_parse_format/uvc_parse_frame, v7.2-rc2), जिसे इसलिए चुना गया क्योंकि इसमें सोलह वर्षों के अंतराल पर दो स्वतंत्र मेमोरी-सुरक्षा CVE थे (CVE-2008-3496, CVE-2024-53104, जिनमें से उत्तरार्द्ध CISA KEV कैटलॉग में है)।

चक्र, और प्रत्येक चरण ने क्या स्थापित किया

1. C लीफ निकालें (c/)। पार्सिंग लॉजिक kernel से बाइट-दर-बाइट कॉपी किया गया; केवल environment को स्टब किया गया (// SPIKE-STUB)। यह C-ABI लाइब्रेरी में कंपाइल होता है। निकाले गए लीफ में काउंटिंग पास और आकार-निर्धारित allocation शामिल है, इसलिए CVE-2024-53104 बग वर्ग (काउंट ने जितना allocate किया उससे आगे पार्स द्वारा लिखना) पहुँच-योग्य है, अमूर्त नहीं किया गया।

2. Rust में पुनर्लेखन (rust/)। वही पार्सिंग लीफ safe Rust में, वही C ABI और परिणाम struct। C से प्रत्येक विचलन को // DEVIATION टैग किया गया है और प्रलेखित किया गया है।

3. डिफरेंशियल फ़ज़िंग (fuzz/)। stable rustc पर एक LibAFL हार्नेस दोनों कार्यान्वयनों को एक ही इनपुट से चलाता है और आउटपुट की फ़ील्ड-दर-फ़ील्ड तुलना करता है। परिणाम: कंपाइलर-निर्भर signed-overflow स्थल पर एक पोर्टिंग बेमेल ठीक करने के बाद, 93% edge coverage पर 54,019 निष्पादनों में शून्य विचलन। विश्वसनीय v7.2-rc2 कोड पर कोई out-of-bounds एक्सेस पहुँच-योग्य नहीं है (दोनों CVE पैच किए गए हैं)। एक opt-in नेगेटिव कंट्रोल (--features vuln, दोनों भाषाओं में प्रतिबिंबित) CVE-2024-53104 बेमेल को पुनः प्रस्तुत करता है: उसी इनपुट पर C एक heap out-of-bounds write करता है (ASan), Rust सुरक्षित रूप से panic करता है। विवरण: fuzz/RESULTS.md।

4. औपचारिक सत्यापन (verify/)। विश्वसनीय Rust लीफ Charon और Aeneas के माध्यम से Lean 4 में निकलता है, जिसमें जनरेट किए गए कोड में कोई sorry नहीं है, और कोई union अवरोधक नहीं है (Binder स्पाइक के विपरीत)। दो प्रमेय, verify/VERIFY-REPORT.md और ROADMAP.md में:

   • सभी इनपुट पर पूर्ण सुरक्षा (प्रत्येक परिणाम ok / नियंत्रित fail / nontermination है, कभी भी undefined-behaviour परिणाम नहीं): सिद्ध, sorry-मुक्त। यह उस मेमोरी-सुरक्षा गुण को, जो C में नहीं है, एक जाँचे गए कथन के रूप में स्पष्ट करता है।
   • सुगठित इनपुट पर no-panic (panic केवल विकृत इनपुट पर होता है, जहाँ यह C के OOB write के स्थान पर इच्छित सुरक्षित व्यवहार है): प्रगति पर। काउंटिंग-बनाम-राइट invariant, जिसका उल्लंघन CVE-2024-53104 है, sorry-मुक्त सिद्ध है, साथ ही दो पुन: प्रयोज्य Aeneas लूप-तर्क सिद्धांत और 5 संरचनात्मक रूप से-समाप्त होने वाले लूपों के लिए div-मुक्तता। शेष एक नामित positional-walk functional-correctness कोर (चार कथित लेम्मा) तक घटता है; देखें ROADMAP.md।

स्थिति

चक्र एक लक्ष्य पर शुरू से अंत तक प्रदर्शित है। पुनर्लेखन को डिफरेंशियल फ़ज़िंग द्वारा C के समतुल्य दिखाया गया है; मेमोरी-सुरक्षा अंतर को नेगेटिव कंट्रोल द्वारा ठोस बनाया गया है; Rust स्वच्छ रूप से Lean में निकलता है और इसका पूर्ण-सुरक्षा गुण मशीन-जाँचित है। no-panic प्रमेय के लिए, काउंटिंग invariant (CVE-2024-53104 कोर) sorry-मुक्त सिद्ध है और शेष कार्य एक नामित functional-correctness कोर तक घटाया गया है, जो कथित है परंतु अभी सिद्ध नहीं है। पूर्ण प्रमाण स्थिति और खुले लेम्मा ROADMAP.md में हैं।

लेआउट

• c/ — निकाला गया C लीफ और उसके स्टब
• rust/ — safe-Rust पुनर्लेखन
• fuzz/ — LibAFL डिफरेंशियल फ़ज़र, परिणाम, और CVE-वर्ग नियंत्रण
• verify/ — Charon/Aeneas/Lean निष्कर्षण और प्रमेय
• ROADMAP.md — प्रमाण स्थिति और शेष खुले लेम्मा
• OPEN_CHALLENGES.md — ठोस कार्य जिन्हें कोई योगदानकर्ता उठा सकता है
• */README.md, fuzz/RESULTS.md, verify/VERIFY-REPORT.md — प्रति-चरण विवरण

Environment

Kernel v7.2-rc2 (read-only संदर्भ)। Rust stable 1.94.0। LibAFL 0.15। Charon 909ff09a (v0.1.220, --preset=aeneas), Aeneas c2015b86, Lean/mathlib v4.31.0।