أعلنت خطة Tachyon الخاصة بـ Zcash في 29 يوليو، أنها أكملت التحقق الشكلي من حوض الحجب Ironwood، ونشرت شهادة تحقق آلية تضم أكثر من 2,700 نظرية مكتوبة بلغة البرمجة Lean. أرست عملية التحقق هذه خاصية أمنية تُسمى «سلامة الرصيد»، ما يستبعد ضمن افتراضاتها التشفيرية المعتمدة إمكانية وجود ثغرة تزوير غير قابلة للاكتشاف في Ironwood.
إتمام التحقق الشكلي لخطة Tachyon: أكثر من 2700 نظرية في Lean
تم إنجاز أعمال التحقق الشكلي في خطة Tachyon من خلال تعاون بين ثلاثة باحثين وفريق من خبراء التشفير، واستغرق أكثر من شهر؛ وتضم شهادة التحقق الآلية المنشورة في النهاية أكثر من 2,700 نظرية، وكلها مكتوبة بلغة البرمجة Lean. تكمن أهمية عملية التحقق في أنها «تحقق آلي»؛ أي أن الحاسوب يقوم تلقائياً بالتحقق من صحة كل خطوة من الخطوات المنطقية، بدل الاكتفاء بمراجعة بشرية فقط، ما يوفر درجة أعلى من اليقين.
توضح خطة Tachyon أن التحقق المكتمل يضع ضماناً رياضياً بأن حوض حجب Ironwood لا يحتوي، ضمن افتراضاته التشفيرية المعتمدة، على ثغرات تزوير غير قابلة للاكتشاف.
خاصية «سلامة الرصيد»: ضمان رياضي لمنع الدفع الزائد من تجمعات الأموال المحمية
«سلامة الرصيد (Balance Integrity)» هي الخاصية الأمنية الأساسية التي أرستها عملية التحقق الشكلي؛ ويعرّفها تعريفاً رياضياً مفاده أن المبلغ الذي تدفعه تجمعات أموال Ironwood المحمية لن يتجاوز المبلغ الذي تم إيداعه بشكل معلن. ولتحقيق هذه الخاصية، تشمل أعمال التحقق المكونات التالية:
· نظام إثباتات المعرفة الصفرية (ZK) لدى Ironwood
· قواعد الدارة: قواعد الحساب الأساسية التي تشكل منطق Ironwood
· المحاسبة على مستوى الدفاتر: آلية تتبع الأموال وتسجيلها على مستوى طبقة الشبكة بأكملها
ومن الجدير بالذكر أن هذا البرهان لا يشمل إجراءات الحماية الخصوصية المستقلة في Ironwood؛ إذ ذكر الباحثون أن ضمانات الخصوصية تمثل خاصية أمنية مستقلة تحتاج إلى تحقق منفصل.
خلفية ثغرة Orchard وآلية المحاسبة العامة لـ «الباب الدوّار»
كان السبب المباشر لطرح حوض حجب Ironwood هو اكتشاف ثغرة في حوض الأمان Orchard — إذ قد تؤدي نظرياً إلى عدم اكتشاف عمليات تزوير ZEC، وبالتالي تهدد سلامة إمدادات Zcash. وقد أدخلت Zcash Ironwood ضمن ترقية الإصدار NU6.3؛ وذكر المطورون أنه لا توجد حتى الآن أدلة على استغلال أي ثغرة بالفعل، ويهدف حوض الحجب الجديد إلى استعادة ثقة العالم في سلامة إمدادات Zcash.
يجب أن تمر الأموال المحولة من Orchard عبر نقطة تحقق محاسبية عامة تُسمى «الباب الدوّار (Revolving Door)» بهدف منع أي رموز افتراضية محملة بزيادة من دخول Ironwood؛ ومع استمرار تدفق الأموال من Orchard، قد توفر هذه العملية أيضاً أدلة إضافية تدريجياً لتقييم ما إذا كان حوض الأموال القديم قد تم إساءة استخدامه من قبل.
الأسئلة الشائعة
كم عدد النظريات التي يتضمنها التحقق الشكلي لـ Ironwood في خطة Tachyon، وما الأداة المستخدمة لإتمامه؟
بحسب إعلان خطة Tachyon، يتضمن هذا التحقق الشكلي أكثر من 2,700 نظرية، وجميعها مكتوبة بلغة Lean؛ وقد استغرق إنجازه أكثر من شهر بالتعاون بين ثلاثة باحثين وفريق من خبراء التشفير؛ وتتمثل النتيجة النهائية في برهان رياضي للإنجاز، حيث يتحقق الكمبيوتر تلقائياً من كل خطوة من خطوات المنطق.
ماذا تضمنه خاصية «سلامة الرصيد» على وجه التحديد؟
تضمن «سلامة الرصيد» أن المبلغ الذي تدفعه تجمعات أموال Ironwood المحمية لن يتجاوز المبلغ الذي تم إيداعه بشكل معلن؛ وقد شمل هذا التحقق جميع المكونات اللازمة لتحقيق هذه الخاصية، بما في ذلك نظام إثباتات المعرفة الصفرية في Ironwood، وقواعد الدارة، والمحاسبة على مستوى الدفاتر؛ لكنه لا يشمل إجراءات الحماية الخصوصية المستقلة في Ironwood.
لماذا تحتاج Zcash إلى إدخال Ironwood، وهل تم استغلال ثغرة Orchard بالفعل؟
تم إدخال Ironwood في ترقية الإصدار NU6.3 من Zcash بهدف معالجة ثغرة تم اكتشافها في حوض الأمان Orchard — إذ قد تؤدي نظرياً إلى عدم اكتشاف عمليات تزوير ZEC؛ ويذكر مطورو Zcash أنه لم يتم العثور بعد على أي دليل على الاستغلال الفعلي لهذه الثغرة، ويهدف حوض الحجب الجديد إلى استعادة ثقة العالم في سلامة إمدادات Zcash.
