Loading...
السلسلة: سلسلة التحقق الشكلي · الجزء 1 من 3 الجمهور: المبتدئون تماماً. لا يُفترض وجود خلفية في الرياضيات أو البرمجة أو علم التشفير. ما ستخرج به: فهم واضح لما يعنيه إثبات صحة البرمجيات، ولماذا يختلف ذلك جذرياً عن اختبارها، وما هو البرهان المتحقق منه آلياً، والحدود الدقيقة (والصادقة) لما يمكن أن يعد به مثل هذا البرهان.
يُوثق بمعظم البرمجيات لأنها خضعت للاختبار: نشغّلها على كثير من المدخلات ونراقب سلوكها. يطرح التحقق الشكلي سؤالاً أكثر جرأة. هل يمكننا إثبات، بيقين رياضي، أن نظاماً ما يفعل ما ينبغي له فعله مع كل مدخل محتمل، بما في ذلك المدخلات التي لم يفكر أحد قط في تجربتها؟ تبني هذه المقالة الفكرة من الأساس. الحدس أولاً، ولا رموز قبل أن نستحقها.
إليك قصة حقيقية، وهي سبب وجود هذه السلسلة.
في عام 2022، أطلقت العملة المشفرة المتمحورة حول الخصوصية Zcash مجموعة محمية جديدة باسم Orchard، تتيح للناس إجراء معاملات مع إخفاء المبالغ. وعلى مدى أربع سنوات، عملت بلا عيوب واجتازت تدقيقات مهنية متكررة. ثم، في مايو 2026، اكتشف باحث أمني، من خلال الاستدلال المتأني على الرياضيات الكامنة (وبمساعدة أدوات AI)، موضعاً واحداً ناقص القيود في رياضيات النظام. وكان يمكن لهذه الفجوة وحدها أن تسمح لمهاجم بإنشاء كمية غير محدودة من الأموال المزيفة، ولأن المبالغ كانت مخفية، لما رأى أحد حدوث ذلك. ظل الخلل موجوداً طوال الوقت.
لم يُكتشف بالاختبار. فقد نجح كل اختبار لمدة أربع سنوات. اكتشفه شخص استدل على الرياضيات. وعندما أصلح الفريق الأمر، لم يكتفوا برقعة ثم يمضوا قدماً. بل كتبوا برهاناً رياضياً متحققاً منه آلياً، يشمل أكثر من 2,700 نظرية منفردة، يثبت أن البديل لا يمكن أن يحتوي إطلاقاً على هذه الفئة من العيوب.
ذلك هو التحقق الشكلي، وهذا ما يمنحك إياه: ليس «جرّبنا حالات كثيرة ونجحت»، بل «أثبتنا أنها تصح في كل حالة». وفي الأنظمة التي تكون فيها حالة واحدة فائتة كارثية (الأموال والطائرات والأجهزة الطبية وعلم التشفير)، فإن هذا الفرق يعني كل شيء.
سمّى عالم الحاسوب Edsger Dijkstra النقطة العمياء في الاختبار قبل عقود، وما زالت صحيحة:
يمكن للاختبار أن يُظهر وجود الأخطاء، لكنه لا يُظهر أبداً غيابها.
إذا نجح اختبار ما، فقد تعلّمت أن النظام يعمل مع ذلك الإدخال. ولم تتعلم شيئاً عن المدخلات التي لم تجرّبها، والأخطاء الخطرة تكون دائماً تقريباً في الحالات التي لم يجرّبها أحد.
تخيّل أنك مسؤول عن مبنى فيه ألف باب، وأن مهمتك ضمان إقفال كل باب ليلاً.
الفرق هو بين أخذ عينات من الواقع وإثبات خاصية في التصميم. الاختبار يأخذ عينات. التحقق الشكلي يثبت. تلك هي الفكرة برمتها، وكل ما عداها أدوات لإنجازها بدقة.
كل تحقق شكلي، مهما بلغ من التقدم، يُبنى من ثلاثة مكونات بالضبط. استوعبها بوضوح، وما تبقى تفاصيل.
| الركيزة | المعنى البسيط | تشبيه المبنى |
|---|---|---|
| المواصفة | بيان دقيق لما تعنيه «الصحة» | «يجب أن يُقفل كل باب ليلاً» |
| النظام | الشيء الفعلي الذي يجري فحصه (برنامج أو دائرة أو بروتوكول) | المبنى وآلية إقفاله |
| البرهان | حجة صارمة تثبت أن النظام يفي دائماً بالمواصفة | البرهنة المنطقية على أن الضغط على «إقفال» يقفل كل الأبواب |
وهناك مكوّن رابع أكثر هدوءاً يجعل الأمر كله جديراً بالثقة:
من مساعدات البرهان التي قد تسمع أسماءها Lean وRocq (المعروف سابقاً باسم Coq) وIsabelle. وهي، عملياً، محركات شديدة الصرامة للتحقق من المنطق. كُتب برهان Zcash في قصتنا الافتتاحية باستخدام Lean. ومن اللافت أن نماذج AI الحديثة تُستخدم بصورة متزايدة للمساعدة في كتابة هذه البراهين، بإرشاد من البشر، مما اختصر جهوداً كانت تستغرق سنوات إلى أسابيع. ولا تزال الآلة تتحقق من كل خطوة، لذلك لا يأتي تسريع العمل على حساب اليقين.
قد تبدو كلمة «برهان» مهيبة، فلنزل غموضها بمثال ملموس قابل للتحقق. لا علم تشفير، بل حساب مدرسي فقط.
الادعاء: لكل عدد صحيح غير سالب n، يساوي المجموع 0 + 1 + 2 + ... + n المقدار n(n+1)/2.
يمكنك اختبار ذلك. n = 5 يعطي 0+1+2+3+4+5 = 15، و5 × 6 / 2 = 15. ✓ إنه متطابق. جرّب n = 10: المجموع هو 55، وتعطي الصيغة 10 × 11 / 2 = 55. ✓ (تُحسب هذه القيم وتُؤكَّد؛ والادعاء في الواقع صحيح لكل n من 0 إلى 999 عند فحصه مباشرة.)
لكن اختبار القيم، حتى ألف منها، لا يبلغ «لكل عدد صحيح غير سالب». فهناك عدد لا نهائي منها. يسد البرهان هذه الفجوة اللانهائية بحجة منتهية، باستخدام تقنية تسمى الاستقراء:
n = 0، يكون المجموع ببساطة 0، وتعطي الصيغة 0 × 1 / 2 = 0. وهما متساويان. ✓k. أضف الآن العدد التالي، k+1. يصبح المجموع حتى k+1 هو (sum up to k) + (k+1) = k(k+1)/2 + (k+1). يعيد سطر من الجبر ترتيب ذلك إلى (k+1)(k+2)/2، وهو بالضبط الصيغة مع k+1 بدلاً من k. ✓بما أنها تصح في البداية (0)، وكل خطوة تنقلها إلى العدد التالي، فهي تصح لكل الأعداد الصحيحة غير السالبة، إلى الأبد، في حجة منتهية واحدة. ذلك هو البرهان. ويفعل مساعد البرهان هذا الاستدلال نفسه، لكنه يتحقق آلياً من أن كل خطوة، بما فيها «سطر الجبر»، تترتب حقاً عما سبقها.
القفزة التي تستحق استيعابها: يحول البرهان «حالات لا نهائية» إلى حجة منتهية قابلة للتحقق. تلك هي القوة الخارقة التي يفتقر إليها الاختبار بنيوياً.
يتمتع التحقق الشكلي بالقوة جزئياً بسبب رؤية توضيحية تتعلق بمصدر الأخطاء من البداية. يمكن تتبع أي خلل في نظام للتحقق من القواعد إلى أحد ثلاثة مواضع:
| مصدر الخطأ | ما يعنيه | هل يمكننا إثبات زواله؟ |
|---|---|---|
| المواصفة | الرياضيات أو القواعد نفسها خاطئة (شرط مفقود أو تعريف سيئ) | نعم، مباشرة؛ فهذا هو المجال الأساسي للتحقق الشكلي |
| التنفيذ | يفشل الكود في تطبيق مواصفة صحيحة بأمانة | جزئياً؛ إذ غالباً ما تترك هذه الإخفاقات دليلاً يمكن كشفه |
| افتراض منهار | يتبين أن شيئاً يعتمد عليه النظام كله غير صحيح | لا؛ فالافتراضات هي الأساس غير القابل للاختزال |
هذا التصنيف أهم مما يبدو، ويعتمد عليه الجزآن 2 و3. تميل الأخطاء الأعمق والأخطر، التي يمكن أن تبقى مخفية إلى الأبد، إلى العيش في المواصفة: الوصف الرياضي لما يُفترض أن يفعله النظام. والمواصفة هي بالضبط ما يمكن للبرهان المتحقق منه آلياً فحصه مباشرة، في كل الحالات دفعة واحدة. ولهذا تستهدف جهود التحقق الشكلي الجادة ذلك أولاً.
التحقق الشكلي قوي، لكن وعده دقيق، وسوء فهمه يضلل الناس. لذا فلنصرح به بعناية:
يضمن البرهان أن النظام يفي بـالمواصفة، في ظل افتراضات معلنة. لا أكثر.
تترتب أربع نتائج، وكل واحدة منها مهمة:
وبعيداً عن إضعاف التحقق الشكلي، فإن هذه الدقة هي مصدر قوته. فهي تخبرك بالضبط بما تحصل عليه. وكما سنرى في الجزء 3، فإن فريق Zcash الذي يصرّح بنطاقه وافتراضاته بوضوح («أثبتنا سلامة المعروض، في ظل هذه الافتراضات المسماة، وليس الخصوصية») يمثل نموذجاً لهذه الصراحة.
لإبقاء هذا قابلاً للقراءة، بسّطنا الأمور. تُكتب المواصفات الحقيقية بلغات شكلية دقيقة، لا بجمل إنجليزية؛ وهناك عدة أساليب للتحقق الشكلي (إثبات النظريات التفاعلي، والتحقق بالنماذج، والأساليب القائمة على SMT) تناسب مشكلات مختلفة؛ ولا تزال كتابة هذه البراهين عملاً يتطلب مهارة وجهداً، حتى مع مساعدة AI. كما تجاوزنا كيفية تمثيل مساعد البرهان للمنطق داخلياً. لا يغير أي من ذلك الجوهر: مواصفة ونظام وبرهان متحقق منه آلياً على توافقهما، في ظل افتراضات معلنة. وستعود التفاصيل حين نحتاج إليها.
| المصطلح | المعنى بلغة بسيطة |
|---|---|
| Formal verification | إثبات، رياضياً، أن نظاماً يفي بمواصفة في جميع الحالات |
| Specification | بيان دقيق لما يعنيه «السلوك الصحيح» |
| System | البرنامج أو الدائرة أو البروتوكول الفعلي الذي يجري فحصه |
| Proof | سلسلة منتهية من الخطوات المنطقية تثبت ادعاءً في جميع الحالات |
| Proof assistant / theorem prover | برمجيات (Lean وRocq وIsabelle) تتحقق من كل خطوة في البرهان |
| Machine-checked | يتحقق منه حاسوب خطوة بخطوة، لا بمجرد قراءة بشرية |
| Induction | تقنية برهان: تصح في البداية، وتنقلها كل خطوة إلى التالية |
| Assumption | شرط يعتمد عليه البرهان؛ وإذا كان خاطئاً، فقد لا يصح الضمان |
هل يحل التحقق الشكلي محل الاختبار؟ لا. إنهما يكملان بعضهما. يلتقط الاختبار المشكلات العملية والافتراضات الخاطئة بكلفة منخفضة؛ بينما يستبعد التحقق فئات كاملة من الأخطاء التي قد لا يأخذ الاختبار عينة منها أبداً.
إذا كان بهذه القوة، فلماذا لا يُتحقق من كل شيء شكلياً؟ إنه مكلف ويتطلب مهارة متخصصة، رغم أن مساعدة AI تخفض تلك الكلفة. ويُخصص للأنظمة التي سيكون فيها خطأ نادر كارثياً، وهي بالضبط الحالات التي تبرر فيها فائدته كلفته.
هل يمكن لنظام متحقق منه شكلياً أن يفشل رغم ذلك؟ نعم، إذا كانت المواصفة خاطئة أو صيغ تعريف ما خطأً أو لم يتحقق افتراض ما أو كان الإخفاق خارج ما حددته المواصفة. لا يغطي البرهان إلا ما يدّعي تغطيته.
هل البرهان المتحقق منه آلياً أكثر جدارة بالثقة من البرهان البشري؟ في البراهين الكبيرة والمعقدة، نعم عموماً. لن تغفل الآلة فجوة دقيقة ولن تقبل ادعاءً بلا برهان، رغم أنها تظل تثق بالمواصفة والتعريفات المعطاة لها.
إذا ساعد AI في كتابة البرهان، فلماذا نثق به؟ لأن مساعد البرهان يتحقق آلياً من كل خطوة. يقترح AI الخطوات؛ وتتحقق الآلة منها. تُرفض الخطوة الخاطئة ببساطة، ولذلك يسرّع AI العمل دون إضعاف الضمان.
تثبت أن برمجيات بنك «لا تسمح أبداً بأن يصبح رصيد حساب ما سالباً». وبعد سنة، لا تزال الأموال تختفي. كيف يمكن أن يكون كلا الأمرين صحيحاً في الوقت نفسه؟ (الإجابة أدناه.)
ضمن البرهان خاصية واحدة بالضبط: ألا تصبح الأرصدة سالبة أبداً. ويمكن أن تختفي الأموال بطرق لم تتناولها تلك الخاصية مطلقاً، مثل خطأ ينقل الأموال إلى الحساب الخطأ (الذي يظل رصيده غير سالب)، أو عيب في جزء من النظام لم يُحدد في المواصفة أبداً. نفّذ التحقق بالضبط ما وعد به ولا شيء أكثر. هذا هو تحفظ القسم 6 عملياً: يغطي البرهان المواصفة، لا كل تصور ممكن لـ«الصحة».
الجزء 2 · خطأ Orchard: ننتقل إلى قصة 2026 الحقيقية كاملة. أخفى نظام خصوصية المبالغ باستخدام براهين تشفيرية، وكان سطر واحد ناقص القيود في رياضياته يعني إمكان جعل تلك البراهين تكذب، مما يسمح بتزوير غير محدود وغير مرئي. سنرى بالضبط ما تعنيه «دائرة ناقصة القيود»، ولماذا يمكن لهذه الفئة من الأخطاء أن تظل مخفية إلى الأبد، ولماذا حدثت أكثر من مرة.
جزء من سلسلة التحقق الشكلي لـZecHub.