Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL
تقدم هذه الورقة صياغة رسمية باستخدام Isabelle/HOL لبروتوكول إثبات شفاف من طراز STARK، يتميز بنموذج قابل للتنفيذ للمُثبت والمُتحقق، وموناد حالة احتمالية مع حساب الشرط الأضعف، ونظريات مُحققة رسميًا حول كمال الأمان والنزاهة (honest completeness) وصحة الإثبات (soundness) مع حدود احتمالية صريحة.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تحاول إثبات معرفتك بكلمة سر سرية لفتح خزنة ضخمة ومغلقة، ولكنك تريد القيام بذلك دون أن تخبر أحداً بكلمة السر فعلياً، ودون أن يضطروا للانتظار ساعات بينما تقوم أنت بكتابتها. هذا هو عالم التشفير، وهو علم الاتصالات الآمنة. في هذا الركن تحديداً، نحن ننظر إلى نوع من الإثبات الرقمي يسمى STARK. فكر في الـ STARK كأنه "إيصال سحري". إذا قمت بتشغيل برنامج حاسوبي معقد، فإن الـ STARK هو ملاحظة صغيرة غير قابلة للتزوير تقول: "لق Cur لقد قمت بتشغيل هذا البرنامج بشكل صحيح، وإليك النتيجة"، دون الكشف عن التفاصيل الفوضوية لكيفية عمل البرنامج.
لفهم كيفية عمل هذه الإيصالات، تحتاج إلى معرفة ثلاثة أشياء بسيطة. أولاً، غالباً ما يحول الكمبيوتر المشكلات إلى ألغاز رياضية تتضمن كثيرات الحدود (تلك الخطوط المنحنية التي قد تتذكرها من الجبر). ثانياً، لإثبات صحة الرياضيات، لا يتم فحص كل رقم؛ بل تأخذ عينات عشوائية قليلة، مثل تذوق ملعقة من الحساء لمعرفة ما إذا كان القدر بأكمله مالحاً أم لا. ثالثاً، لضمان عدم قيام أحد بتغيير الحساء بعد تذوقه، تستخدم شجرة ميركل (Merkle tree)، وهي تشبه بصمة رقمية لمجموعة ضخمة من البيانات. إذا تغيرت حتى حبة أرز واحدة في المجموعة، تتغير البصمة تماماً.
السؤال الكبير في هذا المجال هو: "هل يمكننا التأكد تماماً من أن هذه الإيصالات السحرية مستحيلة التزوير؟" لفترة طويلة، كتب الناس قواعد الـ STARKs، لكن كتابة القواعد تختلف عن إثبات أنها تعمل. وهنا يأتي دور التحقق الرسمي (formal verification). إنه يشبه أخذ برهان رياضي وتغذيته لمحامٍ آلي صارم للغاية، يقوم بفحص كل خطوة منطقية للتأكد من عدم وجود ثغرات، أو "ربما"، أو حيل خفية. وهذا بالضبط ما تفعله ورقة البحث "Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL".
لقد قام المؤلف، دييجو مارمولر، بأخذ بروتوكول STARK معقد وترجمته إلى لغة يمكن للحاسوب فهمها والتحقق منها بيقين بنسبة 100%. هم لم يكتفوا فقط بكتابة قصة حول كيف يجب أن يعمل، بل بنوا نموذجاً يعمل داخل أداة تسمى Isabelle/HOL. تعمل هذه الأداة كمدرس رياضيات صارم يرفض قبول أي إجابة ما لم يتم تبرير كل خطوة فيها.
إليك ما وجدوه. أولاً، بنوا نسخة قابلة للتشغيل من النظام. لقد أنشأوا "مُثبتاً" رقمياً (الذي يصنع الإيصال) و"مُحقِّقاً" (الذي يفحص الإيصال) يمكن تشغيلهما فعلياً على الحاسوب. لقد أثبتوا أنه إذا كان المُثبت صادقاً ويتبع القواعد، فإن المُحقِّق سوف يقبل دائماً الإثبات. لا توجد فرصة لصفر في فشل المُثبت الصادق. هذا يشبه إثبات أنه إذا اتبعت الوصفة بدقة، فإن الكعكة ستنتفخ دائماً.
ثانياً، والأهم من ذلك، تناولوا الجزء المخيف: ماذا لو حاول شخص ما التصرف بشكل غير نزيه؟ لقد أنشأوا سيناريو حيث يحاول "خصم" مخادع خداع المُحقِّق لقبول إيصال مزيف. تثبت الورقة أنه إذا كانت فرصة نجاح هذا الخصم ليست صفراً، إلا أنها صغيرة جداً من الناحية الرياضية. هم لم يقولوا فقط إن الأمر "غير مرجح"؛ بل كتبوا معادلة محددة تحسب بالضبط مدى صغر هذه الفرصة. هذه المعادلة تجمع كل الطرق المختلفة التي يمكن للخصم من خلالها التصرف بشكل غير نزيه — مثل تخمين الأرقام العشوائية الصحيحة، أو إيجاد ثغرة في البصمة الرقمية، أو تزييف معادلة رياضية — وتظهر أن الاحتمال الإجمالي للنجاح محدود برقم صغير جداً.
كما استبعدت الورقة صراحة بعض الطرق "السهلة" للإثبات. قد تعتقد: "ألا يمكننا فقط النظر إلى كومة البيانات بأكملها لنرى ما إذا كانت مزيفة؟" يقول المؤلف لا. في العالم الحقيقي، ينظر المُحقِّق فقط إلى بضعة أماكن عشوائية (اختبار التذوق). تثبت الورقة أنه لا يمكنك افتراض أن المُحقِّق يرى الصورة الكاملة. بدلاً من ذلك، يجب أن يعمل الإثبات حتى عندما يرى المُحقِّر لمحة جزئية ضئيلة فقط. كما رفضوا فكرة مجرد افتراض أن الرياضيات تعمل؛ لقد فككوا الإثبات إلى طبقات صغيرة يمكن إدارتها، حيث تم فحص منطق "البصمة" بشكل منفصل عن منطق "أخذ العينات العشوائية"، ثم إظهار كيفية ترابطهما معاً.
أحد أروع أجزاء هذا العمل هو أنهم لم يكتفوا بإثبات ذلك لعالم نظري لانهائي. لقد بنوا مثالاً صغيراً يعمل باستخدام عالم رياضي صغير جداً (حقل يحتوي على 5 أرقام فقط، مثل ساعة لا تتجاوز الخمسة). قاموا بتشغيل المُثبت والمُحقِّق الصادقين على هذه الساعة الصغيرة وشاهدوهم وهم ينجحون. هذا يوضح أن الكود ليس مجرد نظرية؛ بل هو يعمل بالفعل.
إذاً، ما هي الخلاصة؟ لا تدعي الورقة أنها اخترعت نوعاً جديداً من الـ STARK أو أنها جعلت النظام أسرع. بدلاً من ذلك، تدعي أنها أغلقت الباب على الرياضيات. إنها تقدم ضماناً تم التحقق منه آلياً بأن بروتوكول STARK سليم. إذا اتبعت القواعد، ستحصل على إيصال. وإذا حاولت كسر القواعد، فإن الرياضيات تقول إن فرصتك في النجاح شبه معدومة، وأن الحاسوب قد فحص كل خطوة من ذلك المنطق للتأكد. إنها تحول وعداً تشفيرياً معقداً إلى حقيقة مُحققة، مما يمنحنا مستوى من الثقة يأتي من محامٍ آلي يصحح الواجب المنزلي، بدلاً من مجرد إنسان يقول: "أعتقد أن الأمر يبدو صحيحاً".
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.