خلل في Borrow Checker في Rust: ماذا تعني الـ Soundness فعلاً

يَعِد نظام الأنواع في Rust بوعد صارم: إذا تجمّع كودك الآمن، فلا يمكن أن يحتوي على مؤشرات معلّقة (dangling pointers) أو سباقات بيانات (data races) أو استخدام بعد التحرير (use-after-free). لذلك، عندما عرضت إحدى مشكلات GitHub مقتطفًا من Rust يبدو آمنًا تمامًا لكنه يطبع قمامة مأخوذة من إطار مكدس ميّت، واتضح أن الثغرة كانت كامنة في Rust borrow checker منذ إحدى عشرة سنة، شعر كثيرون بأن الأرض تهتز تحت أقدامهم. يسمح الخلل بتمرير متطلبات عمر (lifetime) حقل من struct عبر إسناد حقل من نوع covariant، ومع تنفيذ Drop خبيث يمكنك تخزين مرجع إلى متغير محلي في متغير عام ثم قراءته بعد زوال المتغير. يسميه AddressSanitizer stack-use-after-scope. أما المترجم فاعتبره سليمًا.

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

الخرافة 1: خلل Unsoundness يعني أن نموذج الأمان في Rust فشل

أول رد فعل هو اعتبار ذلك شقًا في النظرية. لكنه ليس كذلك. لم يُعِد أحد كتابة قواعد الأعمار (lifetimes)، ولم يكتشف أحد أن الملكية (ownership) والاستعارة (borrowing) مكسورتان من الأساس. نظام الأنواع في Rust، كما صُمّم على السبورات وفي الـ RFCs، يقول إن هذا البرنامج يجب أن يُرفض. المترجم فقط فشل في رفضه.

هذا التمييز بين المواصفة والتنفيذ من أقدم خطوط الصدع في مجالنا. قدّم Tony Hoare نظرية جميلة للعمليات المتسلسلة المتواصلة (CSP)، ثم أخطأت مترجمات C لعقود في ترجمة شيفرة كانت صحيحة تمامًا وفق المعيار. النظرية تصمد بينما الأداة تتسرب. كتبنا من قبل عن فجوة المواصفة والتنفيذ، وهي المكان الذي تعيش فيه الأخطاء، وهذه حالة مثالية لذلك. قواعد الأعمار لم تكن خاطئة. الكود المسؤول عن استنتاج التغاير (variance) في rustc، أي الجزء الذي يقرر متى يكون استبدال &'a T بمكان متوقع فيه &'static T مشروعًا، كان به ثغرة عندما يمر الإسناد عبر حقل من نوع covariant.

إليك شكل الاستغلال مبسطًا. تبني غلافًا (wrapper) يقوم تنفيذ Drop فيه بنسخ حمولته إلى مخزن عام من نوع 'static. عادةً يفرض المترجم أن تكون الحمولة 'static، فلا تدخل إليها مراجع لمتغيرات محلية. الخلل يسمح لك بتهريب مرجع قصير العمر عبر إسناد من نوع covariant، فينتهي الغلاف بحمل &l حيث l هو String محلي:

struct Q<T: 'static + Send>(Option<T>);
impl<T: 'static + Send> Drop for Q<T> {
fn drop(&mut self) {
if let Some(t) = self.0.take() {
KEPT.lock().unwrap().push(Box::new(t)); // escapes to 'static!
}
}
}
fn main() {
{
let l = String::from("hello world, this is long enough");
let mut q = Q(None);
q.0 = Some(&l); // should be rejected; 'static required
} // <- drop runs here, stashing &l in KEPT
// l is gone; KEPT now holds a dangling &'static String
}

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

إذن لا، نموذج الأمان لم يفشل. فشل فرض نموذج الأمان. وهذا فشل أصغر، لكنه، كما سنرى، ليس تافهًا.

الخرافة 2: إن بقاء الخلل دون اكتشاف إحدى عشرة سنة يعني أنه غير ضار

منطق فريق Rust في الفرز كان تقريبًا هكذا: هذا سيكون P-critical لو كان الناس يصطدمون به، لكن إحدى عشرة سنة دون رصد تعني أنه لا يمكن أن يكون سهل الإثارة، فهو إذن P-high. وفي ذلك شيء من الصحة. لكي يسبب الخلل عدم أمان في الذاكرة فعلًا، تحتاج إلى تنفيذ Drop خبيث بقصد يحرك البيانات إلى موقع 'static. نادرًا ما يكتب أحد ذلك. سطح التعرض العرضي صغير جدًا.

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

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

الخرافة 3: كثرة الأعين تجعل كل الأخطاء سطحية

هذه هي الخرافة التي يجب أن تحرجنا أكثر من غيرها. rustc من أكثر المترجمات تدقيقًا على الإطلاق. إنه مفتوح المصدر، ولديه فريق أنواع مخصص، ومجتمع أكاديمي نشط (قدّم RustBelt قبل سنوات نموذجًا رسميًا لنواة من Rust)، وملايين المستخدمين يختبرونه يوميًا. ومع ذلك بقيت ثغرة في الـ soundness داخل استنتاج الأعمار لأكثر من عقد، عبر إعادة كتابة كاملة للآليات المحيطة بها.

قانون Linus يفترض أن الأعين تنظر إلى المكان الصحيح بالنموذج الذهني الصحيح. وخلل الـ unsoundness في نظام الأنواع يُفشل الافتراضين معًا. تسكن هذه الأخطاء عند تقاطع عدة ميزات (التغاير، وترتيب الإتلاف drop order، والتحويل الضمني coercion، وقيود الـ trait)، وكل ميزة صحيحة محليًا. يقرأ المراجعون الكود فيرون الثابت المقصود، لأن الكود كُتب من قِبل أشخاص رأوا الثابت المقصود نفسه. التحيز التأكيدي متأصل في العملية. والمثال المضاد يتطلب التفكير كخصم، والتفكير الخصامي تجاه تجريداتك الخاصة صعب فعلًا.

هناك موقع كامل، counterexamples.org، يوثّق طرقًا تنكسر بها قواعد أنواع تبدو معقولة، والخيط المشترك فيها هو التغيّرية (mutability) مركّبة مع شيء آخر معقّد، وهذا بالضبط شكل هذا الخلل. هذه ليست دروسًا جديدة. عانى نظام أنواع ML من عدم سلامة شهيرة تتعلق بالمراجع القابلة للتعديل والتعدد الأشكال (polymorphism)، وأُصلحت بقيد القيمة (value restriction). مصفوفات Java متغايرة التغاير (covariant)، ويمكنها أن ترمي ArrayStoreException وقت التشغيل لأن مصممي اللغة اختاروا الراحة على السلامة. ومع مرور الوقت، تتحد الميزات الثلاث نفسها، أي التصنيف الفرعي (subtyping) والتعديل (mutation) والأنواع العامة (generics)، لتوقع أحدهم في المشكلة. إذا كنت تستمتع بهذا النوع من علم الآثار، فإن تاريخ Lisp الممتد لستين عامًا يبيّن كم من الوقت تتطور هذه الأفكار، وتبدو قواعد Rob Pike القديمة عن البساطة بمعنى مختلف حين تدرك أن التعقيد هو الحاضنة لثغرات الـ soundness.

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

الخرافة 4: التفكير غير الرسمي هو في الأساس برهان

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

الفجوة بين الاثنين هي المكان الذي تأتي منه مشاريع مثل RustBelt والعمل الجاري على محلّل الـ trait من الجيل التالي. RustBelt، المبني في Coq (المسمى الآن Rocq) على إطار Iris لمنطق الفصل (separation logic)، تحقق آليًا من نموذج لقواعد الأنواع الأساسية في Rust، بما في ذلك الأجزاء المخيفة مثل حدود تجريدات unsafe. كان ذلك إنجازًا مفصليًا. لكن لاحظ ما الذي أثبته: نموذج من Rust، لا rustc نفسه. البرهان يغطي حساب λRust، والمترجم الإنتاجي انحرف، وأضاف ميزات، وراكم قرارات تنفيذ لم يُعِد أحد التحقق منها. هذه المشكلة هي فاتورة هذا الانحراف، وقد حان موعد دفعها.

صياغة مترجم إنتاجي كامل رسميًا مكلّفة بشكل وحشي. CompCert، مترجم C المتحقق رسميًا، استغرق سنوات من الجهد الخبير للغة أصغر بكثير من Rust، والأهم أنه يتحقق من مراحل الترجمة، لا من إثبات أن نظام أنواع المصدر يلتقط كل برنامج سيئ. لن يكتب أحد برهان Coq لمليوني سطر من rustc. المسار الواقعي يشبه أكثر الدفاع متعدد الطبقات:

• نماذج متحقق منها آليًا للقواعد الأساسية (على غرار RustBelt)، بحيث تخلو النظرية نفسها من الثغرات.
• أدوات فحص منهجي (fuzzing) وتحليل حالات تولّد برامج عدائية، أي الزوايا الناتجة عن تفاعل الميزات التي لا يفكر البشر في اختبارها.
• اختبار الطفرات (mutation) والاختبار القائم على الخصائص (property-based) للمُدقِّق: إذا كان قلب قيد يجب أن يُفشل برنامجًا، فتأكد أنه يفعل ذلك. ثقافة اختبار SQLite هي النموذج هنا.
• قائمة محدّثة بقضايا عدم السلامة المعروفة، ولدى Rust أكثر من مئة مُعلَّمة، تُعامَل كقائمة متراكمة ذات أولوية هندسية، لا كمعرفة شفوية متداولة.

المثير أن البحث المدعوم بالـ LLM قد ينتهي بأن يكون إضافة صافية هنا: أداة تركّب الميزات بطرق منحرفة دون كلل هي بالضبط الخصم الذي يفتقده التفكير غير الرسمي. النهاية التي يأملها كثيرون منا هي Rust ذات مواصفة رسمية، ومُدقِّق مُثبَت مقابل تلك المواصفة، لكن حتى ذلك الحين يبقى العمل بطيئًا ومملًّا، وحلًّا لقيود بلا بريق.

الخرافة 5: إذا لم تكن الـ soundness مطلقة، فالأمان الثابت خدعة

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

الـ soundness في نظام الأنواع مبرهنة عن كائن رياضي. أما ما تمنحك إياه لغة إنتاجية فهو ضمان إحصائي واقتصادي: فئات كاملة من الأخطاء، مثل استخدام بعد التحرير وسباقات البيانات وإبطال المُكرِّرات (iterator invalidation)، تنتقل من «إشعاع خلفية ثابت في قاعدة شيفرتك» إلى «أحداث نادرة بما يكفي لتصدّر الصفحة الأولى حين تُكتشف بعد إحدى عشرة سنة». قارن معدلات الأساس. أخطاء أمان الذاكرة في قواعد شيفرة C و C++ الكبيرة تشكّل غالبية الثغرات الخطيرة (CVE) عامًا بعد عام، ولم يعد أحد يتفاجأ بأي واحدة منها. أما أخطاء الـ unsoundness في Rust فنادرة لدرجة أن كل واحدة منها تحصل على قضيتها الخاصة في GitHub، وخيط نقاشها، وثقافة تقرير ما بعد الحادثة. الندرة التي يمكنك عدّها عالم مختلف عن الندرة التي لا يمكنك عدّها.

هناك أيضًا فرق في كيفية تراكم الإخفاقات. في C، كل سطر هو خطر محتمل على أمان الذاكرة، فتكلفة اليقظة تتضخم مع حجم الكود إلى الأبد. في Rust، تتركز اليقظة عند الحواف: كتل unsafe، وواجهة FFI، و(كما عرفنا الآن) مُدقِّق المترجم نفسه. هذا التركيز هو ما يجعل التدقيق، وأدوات مثل Miri، والأساليب الرسمية، ممكنة أصلًا. الضمان ليس ثنائيًا، بل إعادة تشكيل جذرية لمكان وجود المخاطر.

نظام أنواع فيه خلل معروف لم تصله حركة الإنتاج طوال إحدى عشرة سنة ما زال أقوى بلا حدود من لغة يكون فيها الخلل هو التصميم نفسه.

ما الذي ينبغي أن تأخذه فعلًا

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

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

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