💻 computer science

zkFuzz: Foundation and Framework for Effective Fuzzing of Zero-Knowledge Circuits

تقدم هذه الورقة البحثية zkFuzz، وهو إطار عمل جديد للفحص القائم على الطفرات (mutation-based fuzzing) يستند إلى اختبار اتساق تتبع القيود (TCCT) النظري، والذي يكتشف بفعالية ثغرات القيود الناقصة والقيود الزائدة في دوائر المعرفة الصفرية من خلال التغلب على قيود أدوات التحليل الاستاتيكي والتحليل الرسمي الحالية.

المؤلفون الأصليون: Hideaki Takahashi, Jihwan Kim, Suman Jana, Junfeng Yang

نُشر 2026-05-26

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Hideaki Takahashi, Jihwan Kim, Suman Jana, Junfeng Yang

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك تبني خزنة سحرية تثبت من خلالها معرفتك بكلمة مرور سرية دون أن تظهر الكلمة نفسها أبداً. هذا هو بالضبط ما تفعله "دوائر المعرفة الصفرية (ZK circuits)" في العالم الرقمي؛ فهي تعمل كحراس أمن لتقنيات الحفاظ على الخصوصية مثل العملات الرقمية المجهولة وأنظمة التصويت الآمنة.

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

السماح لأي شخص بالدخول (حتى لو لم يعرف كلمة المرور).
قفل الباب في وجه المالك الحقيقي (حما حتى لو كان يمتلك كلمة المرور الصحيحة).

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

المشكلة: "المخطط" مقابل "الواقع"

في هذه الأنظمة، يكتب المطورون برنامجاً يقوم بشيئين في آن واحد:

الحوسبة (The Computation): العمليات الرياضية الفعلية لاستنتاج السر (مثل حساب مسار على خريطة).
القيود (The Constraints): القواعد التي تثبت أن الحسابات تمت بشكل صحيح (مثل قائمة مراجعة للتحقق من وجود المسار).

المشكلة تكمن في أن هذين الجزأين غالباً ما يفقدان التزامن.

ضعف القيود (Under-constrained): القواعد فضفاضة للغاية. يمكن للمخترق خداع النظام لقبول مسار مزيف.
إفراط في القيود (Over-constrained): القواعد صارمة للغاية. يرفض النظام مساراً صحيحاً تماماً بسبب قاعدة صغيرة غير ضرورية.

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

الحل: ZKFUZZ (المُحوّر العشوائي - Mutation Fuzzer)

ابتكر المؤلفون إطار عمل جديداً يسمى ZKFUZZ. وبدلاً من مجرد قراءة الكود، يعمل ZKFUZZ كـ مهندس اختبار مشاكس يحاول كسر النظام عن قصد.

إليك التشبيه:
تخيل أن لديك وصفة طعام (الحوسبة) و اختبار تذوق (القيود).

الأدوات القديمة: تنظر إلى الوصفة وتقول: "هذا يبدو مريباً لأن الوصفة تستخدم الملح". (هي تخمن بناءً على قواعد).
ZKFUZZ: يقوم فعلياً بطبخ الطبخة، ولكنه بعد ذلك يُجري تحويراً (Mutation) على الوصفة. يتبدل "السكر" بـ "الملح"، أو يغير وقت الطبخ. ثم يقدم هذا الطبق المتحور إلى اختبار التذوق.
- إذا قال اختبار التذوق: "لذيذ!" لطبق يُفترض أن يكون طعمه سيئاً (لأن الوصفة قد تغيرت)، فإن ZKFUZZ يدرك أن القيود فضفاضة جداً (Under-constrained).
- إذا قال اختبار التذوق: "مقزز!" لطبق يُفترض أن يكون لذيذاً (لأن الوصفة الأصلية كانت صحيحة)، فإن ZKFUZZ يدرك أن القيود صارمة جداً (Over-constrained).

السر الكامن: "اللياقة" و "الاستهداف"

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

يستخدم ZKFUFF خوارزمية جينية (مثل التطور):

التحوير (Mutation): ينشئ آلاف النسخ المعطلة قليلاً من البرنامج.
درجة اللياقة (Fitness Score): يقيم هذه النسخ المعطلة. إذا اقتربت نسخة معطلة من اجتياز الاختبار (حتى لو فشلت)، فإنها تحصل على "درجة جيدة". هذا يخبر النظام: "أنت تقترب من الهدف!".
الاستهداف (Targeting): هو لا يخمن عشوائياً فح. فهو يعلم أن الأخطاء غالباً ما تحدث عند "الحالات الحدية" (مثل عندما تكون الأرقام صفراً، أو كبيرة للغاية). لذا، يحاول تحديداً تغذية النظام بهذه الأرقام الصعبة ليرى ما إذا كان سينهار.

النتائج: كشف المستور

اختبر الفريق ZKFUFF على 452 دائرة حقيقية مستخدمة في مشاريع فعلية.

النتيجة: وجد 85 خطأً.
الثغرات الصفرية (Zero-Days): 59 منها كانت أخطاء جديدة تماماً وغير معروفة (Zero-Days) لم يكن أحد يعلم بوجودها.
التأثير: أكد المطورون 39 من هذه الأخطاء، وتم إصلاح 14 منها بالفعل. ويشمل ذلك أخطاء في مشاريع كبرى مثل zkSync (منصة كريبتو) و passport-zk-circuits (أنظمة الهوية الرقمية).
لا إنذارات كاذبة: على عكس الأدوات الأخرى، لم يحدد ZKFUFF أي شيء كخطأ ما لم يكن خطأً بالفعل.

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

هذه النظرية الجديدة كشفت عن الأخطاء التي تحدث عندما "يتعطل" الكمبيوتر أو يتوقف بشكل غير متوقع، وهي الأخطاء التي تجاهلتها الأدوات السابقة تماماً.

باخت صريح

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

ملخص تقني: ZKFUZZ: أساس وإطار عمل فعال لفحص دوائر المعرفة الصفرية (Zero-Knowledge)

1. بيان المشكلة

تعد دوائر المعرفة الصفرية (ZK) حجر الزاوية في الحسابات التي تحافظ على الخصوصية، مما يتيح براهين موجزة وتحققاً فعالاً في تطبيقات تتراوح من العملات الرقمية المجهولة إلى تعلم الآلة القابل للتحقق. ومع ذلك، فإن تطوير دوائر معرفة صفرية صحيحة أمر صعب للغاية بسبب عدم التوافق بين منطق الحوسبة العام وقيود كثيرات الحدود في الحقول المحدودة (finite-field polynomials).

هناك فئتان رئيسيتان من الثغرات الأمنية:

الدوائر ناقصة القيود (Under-constrained circuits): تكون القيود فضفاضة للغاية، مما يسمح للمبرمجين الخبيثين بإنشاء براهين صالحة لشهادات (witnesses) غير صالحة (مما ينتهك "السلامة" - soundness).
الدوائر مفرطة القيود (Over-constrained circuits): تكون القيود صارمة للغاية، مما يتسبب في رفض النظام للشهادات الصالحة من مقدمي الشهادات الشرفاء (مما ينتهك "الاكتمال" - completeness).

تواجه طرق الكشف الحالية قيوداً كبيرة:

التحليل الساكن (Static Analysis): تعاني أدوات مثل Circomspect وZKAP غالباً من معدلات عالية من الإيجابيات الكاذبة وتفشل في رصد المشكلات الدلالية العميقة، لا سيالما تلك المتعلقة بالحسابات الوسيطة أو التوقف غير الطبيعي للبرنامج.
الأسال विध (Formal Methods): تواجه الأدوات التي تعتمد على حلول SMT (مثل Picus وConsCS) صعوبة في التوسع لتشمل أحجام الدوائر في العالم الحقيقي، وغالباً ما تعتمد على تعريفات غير مكتملة للثغرات، حيث تركز فقط على عدم الحتمية في القيود بينما تتجاهل الحالات التي يتوقف فيها الحساب أو الحالات التي تختلف فيها القيم الوسيطة.
فجوات التعريف: التعريفات الرسمية السابقة لثغرات المعرفة الصفرية غير مكتملة؛ فهي تتجاهل "التوقف غير الطبيعي" (حيث يفشل الحساب ولكن تظل القيود مستوفاة) وتفشل في مراعاة مجموعة كاملة من مسارات التنفيذ، بما في ذلك القيم الوسيطة.

2. المنهجية

2.1 الأساس النظري: اختبار اتساق الأثر والقيود (TCCT)

قدم المؤلفون إطار عمل رسمي مستقل عن اللغة يسمى TCCT، والذي يعرّف ثغرات المعرفة الصفرية كاختلافات بين مجموعتين:

مجموعة الأثر $T(P)$ : مجموعة جميع مسارات التنفيذ الممكنة (المدخلات، القيم الوسيطة، المخرجات) التي ينتجها برنامج حساب الشهادة $P$ .
مجموعة استيفاء القيود $S(C)$ : مجموعة جميع الأزواج (المدخلات، القيم الوسيطة، المخرجات) التي تستوفي قيود الدائرة $C$ .

يعرّف TCCT الدائرة بأنها محكمة القيود إذا وفقط إذا:

لا يوجد نقص في القيود: أن يكون إسقاط $S(C)$ على أزواج المدخلات والمخرجات مجموعة جزئية من إسقاط $T(P)$ . وهذا يضمن عدم قبول أي آثار غير صالحة.
لا يوجد إفراط في القيود: أن تكون $T(P)$ مجموعة جزئية من $S(C)$ . وهذا يضمن قبول جميع الآثار الصالحة (بما في ذلك قيم وسيطة محددة).

يستوعب هذا الصياغة الثغرات الناتجة عن توقف الحساب (حيث يفشل $P$ ولكن يقبل $C$ المدخلات) والاختلافات في القيم الوسيطة، وهي أمور أغفلتها التعريفات السابقة. وقد أثبت المؤلفون أن تحديد ما إذا كانت الدائرة ناقصة أو مفرطة القيود هو مسألة من فئة NP-complete، وأن نظام TCCT الكامل هو مسألة من فئة co-NP-complete.

2.2 تصميم النظام: ZKFUZZ

ZKFUZZ هو إطار عمل للتحليل الديناميكي يكتشف انتهاكات TCCT باستخدام نهج الطفرات المشتركة للبرنامج وتوليد المدخلات. على عكس الفحص التقليدي الذي يغير المدخلات فقط، يقوم ZKFUZZ بتغيير كل من منطق البرنامج والمدخلات معاً.

سير العمل الأساسي:

الطفرات (Mutation): يقوم النظام بإنشاء طفرات ( $P'$ ) من برنامج الحساب الأصلي ( $P$ ). تشمل الطفرات إزالة التأكيدات (assertions)، وتحويل عمليات التعيين (مثل استبدال المعاملات أو القيم)، وتعديل التعيينات الضعيفة.
التنفيذ (Execution): يتم تنفيذ كل من البرنامج الأصلي ( $P$ ) والطافر ( $P'$ ) على مدخلات عينة ( $x$ ).
التحقق (Verification):
- كشف الإفراط في القيود: إذا أنتج $P(x)$ أثراً صالحاً فشل في استيفاء $C$ ، فإن الدائرة مفرطة القيود.
- كشف نقص القيود: إذا أنتج $P'(x)$ أثراً ذا مخرج مختلف ( $y' \neq y$ ) ولكنه لا يزال يستوفي $C$ ، فإن الدائرة ناقصة القيود (بما أن منطق الطفرة مختلف دلالياً، فلا ينبغي قبول المخرج).
البحث الموجه (Guided Search): للتنقل في مساحة البحث الشاسعة للحقول الأولية الكبيرة وإمكانيات الطفرات اللانهائية، يستخدم ZKFUZZ خوارزمية جينية:
- دالة اللياقة (Fitness Function): تقوم دالة الحد الأدنى لمجموع الخطأ (min-sum fitness function) المبتكرة بحساب مجموع أخطاء القيود عبر جميع القيود لأثر معين. يتم تقييم الطافر بناءً على الحد الأدنى لمجموع الخطأ عبر المدخلات المختارة. يختلف هذا عن الطرق السابقة التي تعتمد على الحد الأقصى فقط، وهو أفضل لعملية الطفرة المشتركة.
- محددات الأهداف (Target Selectors): يستخدم النظام التحليل الساكن لتوجيه الطفرات وتوليد المدخلات نحو الأنماط عالية المخاطر، مثل:
  - القسمة على صفر: توليد مدخلات يكون فيها البسط والمقام كلاهما صفراً.
  - فحص الهاش (Hash-Check): إجبار المدخلات على استيفاء قيود تساوي الهاش.
  - التوزيع المنحاز (Skewed Distribution): توجيه توليد المدخلات نحو الحالات الحدية (0، 1، والقيم القريبة من مودولوس الحقل $q$ ).
  - القائمة البيضاء (White-listing): تخطي القوالب المعروفة بأنها آمنة (مثل IsZero و Num2Bits) للتركيز على الكود الأكثر عرضة للخطأ.

3. المساهمات الرئيسية

إطار عمل TCCT: نموذج رسمي موحد ومستقل عن اللغة يستوعب التعريفات السابقة ويغطي المساحة الكاملة لثغرات المعرفة الصفرية، بما في ذلك تلك الناجمة عن التوقف غير الطبيعي والاختلاف في القيم الوسيطة.
نظام ZKFUZZ: إطار عمل فحص مبتكر يقوم بطفرة البرامج والمدخلات معاً لاكتشاف انتهاكات TCCT، مستخدماً دالة لياقة "الحد الأدنى للمجموع" وعمليات بحث موجهة.
التحقق التجريبي: التقييم على 452 دائرة من واقع مشاريع حقيقية بلغة Circom، مما أظهر أداءً متفوقاً على الأدوات الرائدة حالياً.
نموذج Noir الأولي: تنفيذ أولي للغة Noir، وهي لغة برمجة أخرى للمعرفة الصفرية، مما يثبت قدرة إطار العمل على الاستقلال عن اللغة.

4. النتائج

قام المؤلفون بتقييم ZKFUZZ على 452 دائرة حقيقية من لغة Circom، ومقارنته بأربع أدوات رائدة هي: Circomspect وZKAP وPicus وConsCS.

اكتشاف الثغرات: حدد ZKFUZZ 85 ثغرة فريدة، منها 59 ثغرة "يوم الصفر" (zero-day) لم تكن معروفة سابقاً. تم تأكيد 39 منها من قبل المطورين، وتم إصلاح 14 منها.
المقارنة: وجد ZKFUff 30% إلى 300% أكثر من الثغرات مقارنة بالأدوات الحالية عبر مختلف أحجام الدوائر.
الدقة: حقق ZKFUZZ دقة بنسبة 100% (صفر إيجابيات كاذبة)، بينما سجلت أدوات التحليل الساكن مثل Circomspect وZKAP معدلات إيجابية كاذبة عالية (تراوحت دقتها بين 0.06 و0.75).
السرعة: نجح ZKFUZZ++ (مع محددات الأهداف) في تحديد أكثر من 90% من الثغرات خلال 100 ثانية، متفوقاً بشكل كبير على الطرق الرسمية وأدوات التحليل الساكن.
الأثر: شملت الثغرات المكتشفة ثغرات خطيرة في نقص القيود في مشاريع مثل zk-regex وpassport-zk-circuits مما قد يسمح للمهاجمين بتزوير البراهين أو استخراج الأموال.

5. الأهمية والادعاءات

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

إن قدرة النظام على اكتشاف الثغرات دون إيجابيات كاذبة تجعل منه أداة عملية للمطورين، الذين غالباً ما يتجاهلون التنبيهات الصادرة عن أدوات التحليل الساكن ذات المعدلات العالية من الإيجابيات الكاذبة. علاوة على ذلك، فإن النجاح في اكتشاف الثغرات في دوائر Noir يشير إلى أن إطار عمل TCCT وبنية ZKFUZZ لا يقتبان على لغة Circom فحسب، بل يمكن تعميمهما على لغات المعرفة الصفرية الأخرى التي تُترجم إلى تنسيقات قيود معيارية.

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