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

قبل مناقشة نقاط الضعف في ZK ، دعنا أولا نفهم كيف يقوم CertiK بإجراء التحقق الرسمي من ZK. بالنسبة للأنظمة المعقدة مثل الجهاز الظاهري ZK (zkVM) ، فإن الخطوة الأولى في التحقق الرسمي (FV) هي تحديد ما يجب التحقق منه وخصائصه بوضوح. يتطلب ذلك مراجعة شاملة لتصميم نظام ZK وتنفيذ الكود وإعداد الاختبار. تتداخل هذه العملية مع عمليات التدقيق المنتظمة ولكنها تختلف في أنه بعد المراجعة ، يجب تحديد أهداف وخصائص التحقق. في CertiK، نشير إلى هذا على أنه تحقق موجه نحو التدقيق. عادة ما يتم دمج أعمال التدقيق والتحقق. بالنسبة إلى zkWasm ، أجرينا كلا من التدقيق والتحقق الرسمي في وقت واحد.

ما هي ثغرة ZK؟

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

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

جدول الحساب في zkWasm

إن دقة كل قيد أمر بالغ الأهمية. أي خطأ في القيد ، سواء كان ضعيفا جدا أو مفقودا ، قد يسمح للمتسلل بتقديم دليل مضلل. قد تبدو هذه الجداول وكأنها تمثل تنفيذا صالحا لعقد ذكي ولكنها لا تمثل في الواقع. بالمقارنة مع الأجهزة الظاهرية التقليدية، فإن عتامة معاملات zkVM تضخم هذه الثغرات الأمنية. في السلاسل غير ZK ، يتم تسجيل تفاصيل حسابات المعاملات علنا على blockchain ؛ ومع ذلك ، لا تقوم zkVMs بتخزين هذه التفاصيل على السلسلة. هذا النقص في الشفافية يجعل من الصعب تحديد تفاصيل الهجوم أو حتى ما إذا كان الهجوم قد وقع.

دائرة ZK التي تفرض قواعد تنفيذ تعليمات zkVM معقدة للغاية. بالنسبة إلى zkWasm ، يتضمن تنفيذ دائرة ZK الخاصة بها أكثر من 6000 سطر من كود Rust ومئات القيود. غالبا ما يعني هذا التعقيد أنه قد تكون هناك نقاط ضعف متعددة في انتظار اكتشافها.

زك وسم هندسة الدوائر

في الواقع ، من خلال التدقيق والتحقق الرسمي من zkWasm ، اكتشفنا العديد من نقاط الضعف هذه. أدناه ، سنناقش مثالين تمثيليين ونفحص الاختلافات بينهما.

ثغرة في التعليمات البرمجية: هجوم حقن البيانات Load8

تتضمن الثغرة الأمنية الأولى تعليمات Load8 في zkWasm. في zkWasm ، يتم إنجاز قراءات ذاكرة الكومة باستخدام مجموعة من تعليمات LoadN ، حيث N هو حجم البيانات المراد تحميلها. على سبيل المثال، يجب أن يقرأ Load64 بيانات 64 بت من عنوان ذاكرة zkWasm. يجب أن يقرأ Load8 بيانات 8 بت (أي بايت واحد) من الذاكرة ويضعها بأصفار لإنشاء قيمة 64 بت. داخليا ، يمثل zkWasm الذاكرة كمصفوفة من بايت 64 بت ، لذلك يحتاج إلى "تحديد" جزء من مجموعة الذاكرة. يتم ذلك باستخدام أربعة متغيرات وسيطة (u16_cells) ، والتي تشكل معا قيمة تحميل 64 بت الكاملة.

يتم تعريف قيود تعليمات LoadN هذه على النحو التالي:

ينقسم هذا القيد إلى ثلاث حالات: Load32 و Load16 و Load8. لا يحتوي Load64 على قيود لأن وحدات الذاكرة هي 64 بت بالضبط. بالنسبة لحالة Load32 ، تضمن التعليمات البرمجية أن 4 بايت (32 بت) عالية في وحدة الذاكرة يجب أن تكون صفرا.

بالنسبة لحالة Load16 ، تضمن التعليمات البرمجية أن تكون 6 بايت (48 بت) عالية في وحدة الذاكرة صفرا.

بالنسبة لحالة Load8 ، يجب أن تتطلب أن تكون 7 بايت (56 بت) عالية في وحدة الذاكرة صفرا. لسوء الحظ ، هذا ليس هو الحال في الكود.

كما ترى ، يقتصر فقط 9 إلى 16 بت على الصفر. يمكن أن تكون ال 48 بت العالية الأخرى أي قيمة ولا تزال تمر ك "قراءة من الذاكرة".

باستغلال هذه الثغرة الأمنية ، يمكن للمتسلل العبث بإثبات ZK لتسلسل التنفيذ الشرعي ، مما يتسبب في تحميل تعليمات Load8 لهذه البايتات غير المتوقعة ، مما يؤدي إلى تلف البيانات. علاوة على ذلك ، من خلال الترتيب الدقيق للرموز والبيانات المحيطة ، قد يؤدي ذلك إلى عمليات تنفيذ ونقل خاطئة ، مما يؤدي إلى سرقة البيانات والأصول. يمكن أن تجتاز هذه المعاملات المزورة فحوصات مدققي zkWasm ويتم التعرف عليها بشكل غير صحيح على أنها معاملات مشروعة بواسطة blockchain.

إصلاح هذه الثغرة الأمنية هو في الواقع بسيط للغاية.

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

ثغرة التصميم: هجوم عودة مزورة

دعونا نلقي نظرة على ثغرة أمنية أخرى ، هذه المرة تتعلق باستدعاء وعودة zkWasm. الاستدعاء والعودة هي تعليمات VM أساسية تسمح لسياق قيد التشغيل (على سبيل المثال، وظيفة) باستدعاء آخر واستئناف تنفيذ سياق الاستدعاء بعد أن يكمل المتصل تنفيذه. كل دعاء يتوقع عودة في وقت لاحق. تعرف البيانات الديناميكية التي تتبعها zkWasm أثناء دورة حياة الاستدعاء والعودة باسم "إطار الاستدعاء". نظرا لأن zkWasm ينفذ التعليمات بالتتابع ، يمكن طلب جميع إطارات المكالمات بناء على حدوثها أثناء وقت التشغيل. فيما يلي مثال على رمز الاستدعاء / الإرجاع الذي يعمل على zkWasm.

يمكن للمستخدمين الاتصال بوظيفة buy_token () لشراء الرموز (ربما عن طريق الدفع أو نقل العناصر القيمة الأخرى). تتمثل إحدى خطواته الأساسية في زيادة رصيد حساب الرمز المميز بمقدار 1 عن طريق استدعاء وظيفة add_token (). نظرا لأن ZK prover نفسه لا يدعم بنية بيانات إطار المكالمة ، فهناك حاجة إلى جدول التنفيذ (E-Table) وجدول القفز (J-Table) لتسجيل وتتبع السجل الكامل لإطارات المكالمات هذه.

يوضح الشكل أعلاه عملية استدعاء buy_token() add_token() والعودة من add_token() إلى buy_token(). يمكن ملاحظة أن رصيد حساب الرمز المميز يزيد بمقدار 1. في جدول التنفيذ، تشغل كل خطوة تنفيذ صفا واحدا، بما في ذلك رقم إطار الاستدعاء الحالي الذي يتم تنفيذه، واسم دالة السياق الحالية (لأغراض التوضيح فقط)، ورقم التعليمات قيد التشغيل الحالية داخل الدالة، والتعليمات الحالية المخزنة في الجدول (لأغراض التوضيح فقط). في جدول الانتقال السريع، يشغل كل إطار استدعاء صفا واحدا، ويخزن رقم إطار المتصل الخاص به، واسم سياق وظيفة المتصل (لأغراض التوضيح فقط)، وموضع التعليمات التالي لإطار المتصل (بحيث يمكن إرجاع الإطار). في كلا الجدولين ، يوجد عمود "jops" يتتبع ما إذا كانت التعليمات الحالية عبارة عن مكالمة / إرجاع (في جدول التنفيذ) والعدد الإجمالي لتعليمات الاتصال / الإرجاع لهذا الإطار (في جدول الانتقال السريع).

كما هو متوقع ، يجب أن يكون لكل مكالمة عائد مقابل ، ويجب أن يكون لكل إطار مكالمة واحدة فقط وإرجاع واحد. كما هو موضح في الشكل أعلاه ، فإن قيمة "jops" للإطار الأول في Jump Table هي 2 ، المقابلة للصفين الأول والثالث في جدول التنفيذ ، حيث تكون قيمة "jops" هي 1. كل شيء يبدو طبيعيا في الوقت الحالي.

ومع ذلك ، هناك مشكلة هنا: في حين أن مكالمة واحدة وإرجاع واحد ستزيد من عدد "jops" للإطار إلى 2 ، فإن مكالمتين أو عودتين ستؤدي أيضا إلى عدد 2. قد يبدو إجراء مكالمتين أو عائدين لكل إطار أمرا سخيفا ، ولكن من المهم أن تتذكر أن هذا هو بالضبط ما سيحاول المتسلل القيام به من خلال كسر التوقعات.

قد تشعر بالإثارة الآن ، لكن هل وجدنا المشكلة حقا؟

اتضح أن استدعاءين لا يمثلان مشكلة لأن قيود جدول التنفيذ وجدول الانتقال تمنع تشفير مكالمتين في نفس الصف من الإطار لأن كل مكالمة تولد رقم إطار جديد ، أي رقم إطار المكالمة الحالي بالإضافة إلى 1.

ومع ذلك ، فإن الوضع ليس محظوظا جدا لعودتين: نظرا لعدم إنشاء إطار جديد عند العودة ، يمكن للمتسلل بالفعل الحصول على جدول التنفيذ وجدول القفز لتسلسل تنفيذ شرعي وحقن عوائد مزورة (والإطارات المقابلة). على سبيل المثال، يمكن العبث بمثال جدول التنفيذ وجدول الانتقال السريع السابق لاستدعاء buy_token() add_token() بواسطة متسلل إلى السيناريو التالي:

قام المتسلل بحقن مرتجعين مزورين بين الاستدعاء الأصلي والعودة في جدول التنفيذ وأضاف صف إطار مزور جديد في جدول الانتقال السريع (يجب زيادة الإرجاع الأصلي وخطوات تنفيذ التعليمات اللاحقة في جدول التنفيذ بمقدار 4). نظرا لأن عدد "jops" لكل صف في Jump Table هو 2 ، يتم استيفاء القيود ، وسيقبل مدقق إثبات zkWasm "إثبات" تسلسل التنفيذ المزور هذا. كما يتضح من الشكل ، يزيد رصيد حساب الرمز المميز 3 مرات بدلا من 1. لذلك ، يمكن للمتسلل الحصول على 3 رموز بسعر 1.

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

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

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

مقارنة بين اثنين من نقاط الضعف

يتمتع كل من "Load8 Data Injection Vulnerability" و "ثغرة عودة التزوير" بالقدرة على السماح للمتسللين بالتلاعب ببراهين ZK ، وإنشاء معاملات خاطئة ، وخداع مدققي الإثبات ، والانخراط في السرقة أو الاختطاف. ومع ذلك ، فإن طبيعتها وطريقة اكتشافها مختلفة تماما.

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

تم اكتشاف "ثغرة عودة التزوير" أثناء التحقق الرسمي بعد التدقيق. أحد أسباب فشلنا في اكتشافه أثناء التدقيق هو أن zkWasm لديه آلية مشابهة ل "jops" تسمى "mops" ، والتي تتعقب تعليمات الوصول إلى الذاكرة المقابلة للبيانات التاريخية لكل وحدة ذاكرة أثناء وقت تشغيل zkWasm. القيود المفروضة على عدد المماسح صحيحة بالفعل لأنها تتعقب نوعا واحدا فقط من تعليمات الذاكرة ، وتكتب الذاكرة ، والبيانات التاريخية لكل وحدة ذاكرة غير قابلة للتغيير وتكتب مرة واحدة فقط (عدد المماسح هو 1). ولكن حتى لو لاحظنا هذه الثغرة الأمنية المحتملة أثناء التدقيق ، فلن نتمكن من تأكيد أو استبعاد كل سيناريو محتمل بسهولة دون تفكير رسمي صارم بشأن جميع القيود ذات الصلة ، حيث لا يوجد في الواقع سطر من التعليمات البرمجية غير صحيح.

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

أفضل الممارسات لاكتشاف الثغرات الأمنية في ZK

استنادا إلى خبرتنا في التدقيق والتحقق رسميا من zkVM وسلاسل ZK وغير ZK الأخرى ، إليك بعض الاقتراحات حول أفضل طريقة لحماية أنظمة ZK:

التحقق من الكود والتصميم

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

إجراء عمليات التدقيق والتحقق الرسمي

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

إذا كنت تجري تدقيقا وتحققا رسميا لنظام ZK ، فإن الطريقة المثلى هي إجراء كليهما في وقت واحد. وهذا يمكن المدققين ومهندسي التحقق الرسمي من التعاون بكفاءة ، مما قد يؤدي إلى اكتشاف المزيد من نقاط الضعف حيث أن مدخلات التدقيق عالية الجودة مطلوبة للتحقق الرسمي.

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

ضمان أمن الدوائر والعقود الذكية

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

تتضمن جهودنا في التدقيق والتحقق الرسمي ل zkWasm دائرة zkWasm فقط. ومع ذلك ، من منظور الأمان العام لتطبيقات ZK ، من الأهمية بمكان التدقيق والتحقق رسميا من عقودها الذكية أيضا. بعد كل شيء ، سيكون من المؤسف إذا أدى التراخي في تدقيق العقود الذكية ، بعد بذل جهد كبير لضمان أمن الدوائر ، إلى تسوية التطبيق.

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

دعونا نلخص تأثير التحقق الرسمي (FV) على أنظمة ZK ومكوناتها بالنقاط التالية.

بيان:

1. هذه المقالة مستنسخة من [panewslab] ، حقوق الطبع والنشر مملوكة للمؤلف الأصلي [CertiK] ، إذا كان لديك أي اعتراضات على إعادة الطباعة ، فيرجى الاتصال بفريق Gate Learn ، وسيقوم الفريق بالتعامل معها في أقرب وقت ممكن وفقا للإجراءات ذات الصلة.

2. إخلاء المسؤولية: الآراء ووجهات النظر الواردة في هذه المقالة تمثل فقط وجهات نظر المؤلف الشخصية ولا تشكل أي نصيحة استثمارية.

3. تتم ترجمة إصدارات اللغات الأخرى من المقالة من قبل فريق Gate Learn ولم يتم ذكرها في Gate.io ، ولا يجوز إعادة إنتاج المقالة المترجمة أو توزيعها أو سرقتها.