نشر باحثو Zcash مجموعة تضم أكثر من 2,700 نظرية مدققة آليًا، صُممت للقضاء على أخطاء التزوير غير القابلة للكشف في ترقية البروتوكول القادمة Ironwood. يهدف العمل، الذي نشره الفريق المسؤول عن العملة الرقمية التي تركز على الخصوصية، إلى إثبات رياضيًا أن الكود الجديد لا يمكن استغلاله لإنشاء عملات مزيفة دون اكتشاف.
ما الذي تستهدفه النظريات
تركز النظريات على Ironwood، وهي ترقية مخطط لها لقواعد الإجماع في Zcash. أخطاء التزوير هي فئة من الثغرات التي تسمح للمهاجم بسك عملات من العدم — وهو فشل كارثي لأي عملة رقمية. باستخدام التحقق الرسمي، يمكن للباحثين إثبات رياضيًا أن خصائص معينة تنطبق على كل تنفيذ ممكن للكود، بدلاً من الاعتماد فقط على المراجعات اليدوية أو الاختبارات.
تغطي النظريات البالغ عددها 2,700 المنطق الأساسي للمعاملات المحمية في Ironwood، حيث يتم تشفير الأرصدة ومبالغ المعاملات. تتحقق البراهين من أن النظام يفرض ثوابت العرض — مما يعني أنه لا يمكن إنشاء المزيد من Zcash أكثر مما يسمح به البروتوكول — حتى في ظل ظروف معادية. يقول الباحثون إن هذا النهج يكتشف الحالات الحدودية التي قد تفوتها مراجعة الكود التقليدية.
لماذا تهم البراهين المدققة آليًا
التحقق الرسمي نادر في تطوير العملات الرقمية لأنه يستغرق وقتًا طويلاً ويتطلب خبرة متخصصة. تعتمد معظم المشاريع على مكافآت الأخطاء والمراجعات اليدوية، والتي قد تترك ثغرات. استخدمت Zcash الأساليب الرسمية من قبل — لترقيتها الأصلية Sapling — لكن جهد Ironwood هو أكبر تطبيق من هذا القبيل للشبكة حتى الآن.
النظريات مكتوبة بلغة تسمى Lean، وهي مساعد برهان يتحقق من كل خطوة من خطوات الاستدلال. إذا اجتازت النظرية، فهذا يعني أن الخاصية مضمونة لجميع المدخلات. نشر الباحثون المجموعة الكاملة من البراهين إلى جانب مواصفات Ironwood، مما يسمح بالتحقق المستقل من قبل المجتمع.
قال الفريق في بيان: "يتعلق الأمر بتقديم أقوى ضمان ممكن بأن الرياضيات وراء Ironwood سليمة. نريد أن يعرف المستخدمون أن العرض مثبت رياضيًا، وليس مجرد افتراض."
لا تزال Ironwood قيد التطوير. يمثل عمل التحقق الرسمي علامة فارقة رئيسية، لكن الترقية لا تزال بحاجة إلى المرور عبر عملية حوكمة Zcash واعتمادها من قبل المعدنين ومشغلي العقد. يخطط الفريق لمواصلة توسيع مجموعة النظريات مع إضافة ميزات جديدة.
نشر النظريات لا يغير شيئًا لمستخدمي Zcash الحاليين. تستمر الشبكة في العمل على البروتوكول الحالي. لكن العمل يضع سابقة لكيفية التحقق من الترقيات المستقبلية — بيقين رياضي بدلاً من مجرد الثقة.
الخطوة التالية هي فترة مراجعة مجتمعية، بعدها سيُقترح كود Ironwood للتفعيل. لم يتم تحديد موعد بعد.
