التحقق الرسمي المتقدم من براهين المعرفة الصفرية: كيفية التحقق من تعليمات ZK

المصدر: مجتمع CertiK الصيني

من أجل الفهم العميق لكيفية تطبيق تقنية التحقق الرسمية على zkVM (الجهاز الظاهري صفر المعرفة)، ستركز هذه المقالة على بشأن التحقق من تعليمات واحدة. للاطلاع على الوضع العام للتحقق الرسمي المتقدم من ZKP (إثبات المعرفة الصفرية)، يرجى الرجوع إلى مقالة "التحقق الرسمي المتقدم من سلسلة الكتل المقاومة للمعرفة الصفرية" التي نشرناها في نفس الوقت.

ما هو التحقق من تعليمات ZK؟

يمكن لـ zkVM (آلة افتراضية ذات معرفة صفرية) إنشاء كائنات إثبات قصيرة كدليل على أن برنامجًا معينًا يمكن تشغيله على مدخلات معينة وينتهي بنجاح. في مجال Web3.0، يؤدي تطبيق zkVM إلى زيادة الإنتاجية لأن عقدة L1 تحتاج فقط إلى التحقق من الدليل القصير لانتقال العقد الذكي من حالة الإدخال إلى حالة الإخراج، ويمكن إكمال تنفيذ كود العقد الفعلي خارج السلسلة .

يقوم مُثبت zkVM أولاً بتشغيل البرنامج لإنشاء سجل تنفيذ لكل خطوة، ثم يقوم بتحويل بيانات سجل التنفيذ إلى مجموعة من الجداول الرقمية (تسمى هذه العملية "الحساب"). يجب أن تلبي هذه الأرقام مجموعة من القيود (أي الدوائر)، والتي تشمل معادلات الاتصال بين خلايا جدول معينة، والثوابت الثابتة، وقيود البحث في قاعدة البيانات بين الجداول، والقيود التي يجب استيفاؤها بين كل زوج من صفوف الجدول المتجاورة المعادلات (ويعرف أيضا باسم "البوابات"). يمكن أن يؤكد التحقق عبر السلسلة أن هناك بالفعل جدولًا يلبي جميع القيود، مع ضمان عدم رؤية الأرقام المحددة في الجدول.

يواجه تنفيذ كل تعليمات VM العديد من هذه القيود ونشير هنا إلى مجموعة القيود الخاصة بتعليمات VM باسم "تعليمات ZK". فيما يلي مثال لقيود تعليمات تحميل الذاكرة zkWasm المكتوبة بلغة Rust.

يتم التحقق الرسمي من تعليمات ZK من خلال إجراء تفكير رسمي على هذه الرموز، والتي نترجمها أولاً إلى لغة رسمية.

حتى لو كان قيد واحد فقط يحتوي على خطأ، فمن الممكن للمهاجم إرسال دليل ZK ضار. لا يتوافق جدول البيانات المطابق للدليل الخبيث مع التشغيل القانوني للعقد الذكي. على عكس السلاسل التي لا تنتمي إلى ZK مثل Ethereum، والتي تحتوي على العديد من العقد التي تقوم بتشغيل تطبيقات EVM (جهاز Ethereum الظاهري) المختلفة، مما يجعل من غير المحتمل حدوث نفس الخطأ في نفس الوقت وفي نفس المكان، فإن سلسلة zkVM تحتوي على جهاز افتراضي واحد فقط تطبيق. ومن هذا المنظور وحده، تعتبر سلسلة ZK أكثر هشاشة من نظام Web3.0 التقليدي.

الأمر الأسوأ هو أنه، على عكس السلاسل غير التابعة لـ ZK، نظرًا لعدم تقديم تفاصيل حساب معاملات zkVM وتخزينها على السلسلة، بعد حدوث الهجوم، ليس من الصعب جدًا اكتشاف التفاصيل المحددة فحسب للهجوم، حتى تحديد الهجوم نفسه يمكن أن يصبح أمرًا صعبًا للغاية.

يتطلب نظام zkVM فحصًا صارمًا للغاية، ولسوء الحظ، من الصعب ضمان صحة دائرة zkVM.

لماذا يصعب التحقق من تعليمات ZK؟

يعد VM (الجهاز الظاهري) أحد الأجزاء الأكثر تعقيدًا في بنية نظام Web3.0. تعد الوظائف القوية للعقود الذكية هي جوهر دعم إمكانات Web3.0، وتأتي قوتها من الأجهزة الافتراضية الأساسية، والتي تتميز بالمرونة والتعقيد: من أجل إكمال مهام الحوسبة والتخزين العامة، يجب أن تكون هذه الأجهزة الافتراضية قادرة على دعم العديد من التعليمات. والدول. على سبيل المثال، يتطلب تنفيذ geth الخاص بـ EVM أكثر من 7500 سطرًا من كود لغة Go. وبالمثل، فإن دائرة ZK التي تقيد تنفيذ هذه التعليمات هي أيضًا كبيرة ومعقدة. كما هو الحال في مشروع zkWasm، يتطلب تنفيذ دائرة ZK أكثر من 6000 سطر من كود Rust.

هندسة دوائر zkWasm

دوائر ZkVM أكبر حجمًا من دوائر ZK المتخصصة المستخدمة في أنظمة ZK المصممة لتطبيقات محددة مثل المدفوعات الخاصة أكثر من ذلك بكثير: عدد القيود قد تكون القواعد أكبر بدرجة أو اثنتين، وقد تتضمن الجداول الحسابية مئات الأعمدة بملايين الخلايا الرقمية.

ماذا يعني التحقق من تعليمات ZK؟

نريد هنا التحقق من صحة تعليمة XOR في zkWasm. من الناحية الفنية، يتوافق جدول تنفيذ zkWasm مع تسلسل تنفيذ Wasm VM القانوني. لذلك من منظور ماكرو، ما نريد التحقق منه هو أن كل تنفيذ لهذه التعليمات سيؤدي دائمًا إلى إنشاء حالة zkVM قانونية جديدة: كل صف في الجدول يتوافق مع الحالة القانونية للجهاز الافتراضي، ويتم إنشاء الصف التالي دائمًا بواسطة تنفيذ تعليمات VM المقابلة. يوضح الشكل أدناه النظرية الرسمية لصحة تعليمات XOR.

هنا يشير "state_rel i st" إلى أن الحالة "st" هي حالة zkVM القانونية للعقد الذكي في الخطوة "i". كما قد تتخيل، إثبات "state_rel (i+1) ..." ليس أمرًا تافهًا.

كيفية التحقق من تعليمات ZK؟

على الرغم من أن دلالات الحساب لتعليمة XOR بسيطة جدًا، وهي حساب عدد البتات XOR لعددين صحيحين وإرجاع نتيجة العدد الصحيح، إلا أنها تتضمن جوانب عديدة: أولاً، تحتاج إلى أخذ عددين صحيحين من كومة الذاكرة، وقم بإجراء حساب XOR، ثم قم بتخزين العدد الصحيح الجديد المحسوب مرة أخرى في نفس المكدس. بالإضافة إلى ذلك، يجب دمج خطوات تنفيذ هذه التعليمات في عملية تنفيذ العقد الذكي بأكملها، ويجب أن يكون ترتيب وتوقيت تنفيذها صحيحًا.

لذلك، يجب أن يكون تأثير تنفيذ تعليمات XOR هو إخراج رقمين من مكدس البيانات، ودفع نتائج XOR الخاصة بهما، وفي نفس الوقت زيادة عداد البرنامج للإشارة إلى التعليمات التالية للعقد الذكي.

ليس قبيحًا اتضح أن تعريف خصائص الصحة هنا يشبه بشكل عام الموقف الذي نواجهه عند التحقق من الأجهزة الافتراضية للرمز الثانوي التقليدي (مثل مترجم EVM في عقد Ethereum L1). يعتمد على تعريف تجريدي عالي المستوى لحالة الآلة (هنا ذاكرة المكدس وتدفق التنفيذ) وتعريف السلوك المتوقع لكل تعليمة (هنا المنطق الحسابي).

ومع ذلك، كما سنرى أدناه، نظرًا لخصائص ZKP وzkVM، غالبًا ما تكون عملية التحقق من صحتها مختلفة تمامًا عن تلك الخاصة بالأجهزة الافتراضية التقليدية. فقط للتحقق من تعليماتنا الوحيدة هنا تعتمد على صحة العديد من الجداول في zkWASM: من بينها جدول نطاق يستخدم لتحديد حجم القيمة، وجدول بت يستخدم للنتائج الوسيطة لحسابات البت الثنائية، وجدول تنفيذ يخزن حالة VM ذات حجم ثابت لكل صف (على غرار البيانات الموجودة في السجلات والمزالج في وحدة المعالجة المركزية الفعلية)، والذاكرة التي تمثل جداول حالة VM ذات الحجم المتغير ديناميكيًا (الذاكرة، ومكدس البيانات، ومكدس الاستدعاءات) وجداول الانتقال.

الخطوة 1: ذاكرة المكدس

على غرار الآلة الافتراضية التقليدية، نحتاج إلى التأكد من إمكانية قراءة المعلمتين الصحيحتين للتعليمات من المكدس وأن قيم نتائج XOR الخاصة بهما يتم إعادة الكتابة بشكل صحيح إلى المكدس. يبدو التمثيل الرسمي للمكدس أيضًا مألوفًا تمامًا (توجد أيضًا ذاكرة عامة وذاكرة كومة، لكن تعليمات XOR لا تستخدمهما).

يستخدم zkVM مخططًا معقدًا لتمثيل البيانات الديناميكية لأن مُثبِّت ZK لا يدعم أصلاً هياكل البيانات مثل الأكوام أو المصفوفات. على العكس من ذلك، بالنسبة لكل قيمة يتم دفعها إلى المكدس، يسجل جدول الذاكرة صفًا منفصلاً، ويتم استخدام بعض الأعمدة للإشارة إلى الوقت الفعلي للإدخال. بالطبع، يمكن للمهاجمين التحكم في البيانات الموجودة في هذه الجداول، لذلك يجب فرض بعض القيود للتأكد من أن إدخالات الجدول تتوافق فعليًا مع تعليمات المكدس الفعلية في تنفيذ العقد. يتم تحقيق ذلك عن طريق حساب عدد دفعات المكدس بعناية أثناء تنفيذ البرنامج. عند التحقق من كل تعليمات، نحتاج إلى التأكد من أن هذا العدد صحيح دائمًا. بالإضافة إلى ذلك، لدينا سلسلة من الدروس التي تربط القيود الناتجة عن تعليمة واحدة بعمليات البحث في الجدول وعمليات التحقق من النطاق الزمني التي تنفذ عمليات المكدس. من المستوى الأعلى، يتم تعريف قيود العد لعمليات الذاكرة على النحو التالي.

الخطوة 2: العمليات الحسابية

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

ولكن بالنسبة لـ zkVM، فإن هذا ليس بالأمر السهل في الواقع. التعليمات الحسابية الوحيدة التي يدعمها مثبت ZK هي الجمع والضرب. من أجل تنفيذ عمليات البت الثنائية، يستخدم VM مخططًا معقدًا إلى حد ما، حيث يقوم أحد الجداول بتخزين نتائج العملية الثابتة على مستوى البايت، ويعمل الجدول الآخر بمثابة "لوحة الصفر" لإظهار كيفية تنفيذ العمليات على صفوف متعددة في الجدول. يتم تقسيم الرقم 64 بت إلى 8 بايت ثم يتم إعادة تجميعه لإعطاء النتيجة.

جزء من مواصفات الصورة النقطية zkWasm

بسيط جدًا في عمليات XOR بلغات البرمجة التقليدية، وهنا يلزم استخدام العديد من الجداول للتحقق من صحة هذه الجداول المساعدة. لتوجيهاتنا لدينا:

الخطوة 3: تدفق التنفيذ

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

نظرًا لأن zkWasm مصمم لتشغيل كود Wasm، فمن الضروري أيضًا التأكد من الحفاظ على الطبيعة الثابتة لذاكرة Wasm طوال عملية التنفيذ.

تتمتع لغات البرمجة التقليدية بدعم أصلي لأنواع البيانات مثل القيم المنطقية والأعداد الصحيحة 8 بت والأعداد الصحيحة 64 بت. ومع ذلك، في دوائر ZK، تكون المتغيرات دائمًا في نطاق الأعداد الصحيحة الكبيرة الأعداد الأولية (≈ 2254) التغييرات الداخلية. نظرًا لأن الأجهزة الافتراضية تعمل عادةً عند 64 بت، يحتاج مطورو الدوائر إلى استخدام نظام من القيود للتأكد من أن لديهم النطاقات الرقمية الصحيحة، ويحتاج مهندسو التحقق الرسمي إلى تتبع الخصائص الثابتة حول هذه النطاقات طوال عملية التحقق. يشمل التفكير في تدفقات التنفيذ وجداول التنفيذ جميع الجداول المساعدة الأخرى، لذلك نحتاج إلى التحقق من صحة نطاقات جميع بيانات الجدول.

على غرار حالة إدارة أرقام تشغيل الذاكرة، يتطلب zkVM مجموعة مماثلة من lemmas للتحقق من تدفق التحكم. على وجه التحديد، تتطلب كل تعليمات استدعاء وإرجاع استخدام مكدس الاستدعاءات. يتم تنفيذ مكدس الاستدعاءات باستخدام مخطط جدول مشابه لمكدس البيانات. بالنسبة لتعليمات XOR، لا نحتاج إلى تعديل مكدس الاستدعاءات، ولكن عند التحقق من التعليمات بأكملها، ما زلنا بحاجة إلى التتبع والتحقق مما إذا كان عدد عمليات تدفق التحكم صحيحًا أم لا.

التحقق من هذه التعليمات

دعونا نجمع كل الخطوات معًا ونتحقق من نظرية الصحة الشاملة لتعليمة zkWasm XOR. يتم إكمال عمليات التحقق التالية في بيئة إثبات تفاعلية، حيث تخضع كل خطوة رسمية في البناء والتفكير المنطقي لفحوصات آلية أكثر صرامة.

كما رأينا أعلاه، يعد التحقق الرسمي من دوائر zkVM ممكنًا. ولكن هذه مهمة صعبة تتطلب فهم وتتبع العديد من الخصائص الثابتة المعقدة. يعكس هذا مدى تعقيد البرنامج الذي يتم التحقق منه: يجب التعامل مع كل المسائل المتعلقة بالتحقق بشكل صحيح من قبل مطور الدائرة. ونظراً للمخاطر الكبيرة التي ينطوي عليها الأمر، فمن المفيد أن يتم فحصها آلياً من خلال نظام تحقق رسمي، بدلاً من الاعتماد فقط على المراجعة البشرية الدقيقة.