Towards System-Oriented Formal Verification of Local-First Access Control
تقدم هذه الورقة نهجاً من الأسفل إلى الأعلى للتحقق الرسمي من التحكم في الوصول في الأنظمة المحلية الأولوية (local-first) والمتسامحة مع الأخطاء البيزنطية، وذلك باستخدام إطار العمل Verus القائم على لغة Rust لتطوير دلالات وثوابت غير متغيرة (invariants) موثقة لنوع بيانات مكرر قائم على القدرة (capability-based).
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك ومجموعة من الأصدقاء تحاولون التعاون في دفتر ملاحظات رقمي مشترك. ومع ذلك، بدلاً من أن يقوم الجميع بتسجيل الدخول إلى خادم مركزي واحد ضخم (مثل مستندات جوجل)، يمتلك كل فرد نسخة خاصة به من دفتر الملاحظات على جهازه الخاص. أنت لا تتزامن مع الآخرين إلا عندما يتوفر لديك اتصال بالإنترنت.
يُسمى هذا النوع من البرمجيات بـ "الأولوية للمحلي" (Local-First). وهي ميزة رائعة لأنها سريعة وتعمل دون اتصال بالإنترنت، ولكنها تخلق مشكلة كبيرة: كيف يمكنك التحكم فيمن يحق له تعديل ماذا إذا لم يكن هناك "رئيس" (خادم مركزي) يراقب الجميع؟
تستكشف هذه الورقة كيفية استخدام الرياضيات وعلوم الحاسوب المتقدمة لبناء "حارس أمن رقمي" لهذه الأنظمة اللامركزية، بحيث يكون غير قابل للاختراق وذكياً للغاية.
المشكلة: "الفوضى في دردشة المجموعة"
في النظام العادي (مثل فيسبوك)، إذا قمت بطرد شخص ما من مجموعة، فإن الخادم المركزي يقول: "أنت خارج المجموعة!" ويعرف الجميع ذلك فوراً.
أما في نظام "الأولوية للمحلي"، فلا يوجد خادم مركزي. تخيل دردشة جماعية حيث:
- الصديق المخادع (أخطاء بيزنطية - Byzantine Faults): أحد الأشخاص في المجموعة يتصرف بسوء نية. قد يحاول "تزوير تاريخ" رسالة، مدعياً أنه أرسل أمراً بالأمس لإلغاء قاعدة وضعتها اليوم.
- المسافر عبر الزمن (التزامن - Concurrency): شخصان يقومان بأشياء في نفس اللحظة تماماً. الشخص (أ) يمنح حقوق "محرر" لتشارلي، وفي اللحظة ذاتها، يقوم الشخص (ب) بسحب هذه الحقوق من تشارلي. ولأنه لا توجد ساعة مركزية، قد يرى أشخاص مختلفون في المجموعة نسخاً مختلفة من الواقع.
بدون خطة رياضية صارمة، ستنهار "قواعد" المجموعة في النهاية، وسيتحول دفتر الملاحظات إلى فوضى من التصاريح المتضاربة.
الحل: "كتاب القواعد الرياضي"
لم يكتفِ الباحثون بكتابة الكود البرمجي فحسب؛ بل كتبوا "مواصفات رسمية" (Formal Specification). فكر في هذا الأمر كأنك تكتب قوانين الفيزياء لكونٍ صغير جداً. فبدلاً من قول: "حاول التأكد من أن المسؤولين فقط يمكنهم تغيير الاسم"، كتبوا صيغة رياضية تحدد بدقة معنى كلمة "مسؤول" وكلمة "تغيير" في كل سيناريو محتمل.
لقد ركزوا على ثلاثة "قوانين أساسية للكون":
- سلامة التفويض (Authorization Safety): بمجرد وضع قاعدة ما في الحجر (مثل إنشاء المجموعة)، لا ينبغي أن تتغير عشوائياً.
- سلامة الاستعلام (Query Safety): إذا سألت النظام: "من هو المسؤول؟"، يجب ألا تتغير الإجابة إلا إذا قام شخص ما بالفعل بعمل مصرح به.
* سلامة الإلغاء (Revocation Safety): إذا تم سحب تصريح ما، فيجب أن يظل مسحوباً، حتى لو حاول "صديق مخادع" التظاهر بأن عملية الإلغاء لم تحدث قط.
الأداة: "المجهر فائق القدرة" (Verus)
للتأكد من أن الكود الخاص بهم يتبع هذه القوانين فعلياً، استخدموا أداة تسمى Verus.
فكر في البرمجة العادية كبناء منزل والأمل في ألا ينهار. أما استخدام Verus فهو يشبه بناء منزل داخل محاكي عالي التقنية يختبر كل ذرة من هيكل المنزل ضد قوانين الجاذبية وسرعة الرياح قبل أن تطأ قدمك داخله. إذا كانت هناك حتى فرصة بنسبة 0.00001% بأن يتمكن "صديق مخادع" من كسر قاعدة ما، فإن المحاكي ("مثبت النظريات" - Theorem Prover) سيصرخ في وجه المهندسين حتى يقوموا بإصلاحها.
لماذا يهم هذا الأمر؟
يتخذ الباحثون نهجاً "من الأسفل إلى الأعلى". هم لا يحاولون إصلاح الإنترنت بأكل، بل يبنون "لبنة بناء" صغيرة ومحققة بدقة.
إذا استطاعوا إثبات أن هذه اللبنة الصغيرة غير قابلة للتدمير وتتبع القواعد بشكل مثالي، فيمكنهم في النهاية تكديس هذه اللبنات معاً لبناء أنظمة لامركزية ضخمة وآمنة—مثل ويكيبيديا لامركزية أو تطبيق مراسلة فائق الأمان (مثل Matrix) يمكن للحكومات أو المستشفيات استخدامه دون القلق أبداً من أن يتمكن طرف سيئ واحد من كسر قواعد المجموعة.
باختصار: إنهم يضعون المخططات الرياضية لعالم يمكننا فيه التعاون بحرية دون الحاجة إلى خادم "الأخ الأكبر" (Big Brother) ليفرض علينا النظام.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.