محققان Zcash مجموعهای از بیش از ۲۷۰۰ قضیه بررسیشده توسط ماشین را منتشر کردهاند که برای حذف باگهای جعل غیرقابل تشخیص در ارتقاء پروتکل آینده Ironwood طراحی شدهاند. این کار که توسط تیم پشت این ارز دیجیتال متمرکز بر حریم خصوصی منتشر شده، هدفش اثبات ریاضی این است که کد جدید نمیتواند برای ایجاد سکههای جعلی بدون شناسایی مورد سوءاستفاده قرار گیرد.
هدف قضایا چیست
این قضایا بر Ironwood، یک ارتقاء برنامهریزیشده برای قوانین اجماع Zcash، متمرکز هستند. باگهای جعل دستهای از آسیبپذیریها هستند که به مهاجم اجازه میدهند سکهها را از هیچ خلق کند — یک شکست فاجعهبار برای هر ارز دیجیتال. با استفاده از تأیید صوری، محققان میتوانند به صورت ریاضی اثبات کنند که ویژگیهای خاصی برای هر اجرای ممکن کد برقرار است، نه اینکه تنها به ممیزی دستی یا آزمایش متکی باشند.
۲۷۰۰ قضیه، منطق اصلی تراکنشهای محافظتشده Ironwood را پوشش میدهند، جایی که موجودیها و مقادیر تراکنش رمزگذاری میشوند. اثباتها بررسی میکنند که سیستم ثابتهای عرضه را اعمال میکند — به این معنی که هیچ Zcash بیشتری نسبت به آنچه پروتکل اجازه میدهد ایجاد نمیشود — حتی در شرایط مخرب. محققان میگویند این رویکرد موارد لبهای را که بازبینی کد سنتی ممکن است از دست بدهد، شناسایی میکند.
چرا اثباتهای بررسیشده توسط ماشین اهمیت دارند
تأیید صوری در توسعه ارزهای دیجیتال نادر است زیرا زمانبر است و به تخصص خاصی نیاز دارد. بیشتر پروژهها به پاداش باگ و ممیزی دستی متکی هستند که ممکن است شکافهایی باقی بگذارند. Zcash قبلاً از روشهای صوری استفاده کرده است — برای ارتقاء اصلی Sapling خود — اما Ironwood بزرگترین کاربرد از این نوع تا به امروز برای این شبکه است.
قضایا به زبانی به نام Lean نوشته شدهاند، یک دستیار اثبات که هر مرحله از استدلال را بررسی میکند. اگر یک قضیه تأیید شود، به این معنی است که ویژگی برای همه ورودیها تضمین شده است. محققان مجموعه کامل اثباتها را همراه با مشخصات Ironwood منتشر کردند و امکان تأیید مستقل توسط جامعه را فراهم کردند.
«این درباره ارائه قویترین تضمین ممکن است که ریاضیات پشت Ironwood صحیح است،» تیم در بیانیهای گفت. «ما میخواهیم کاربران بدانند که عرضه به طور اثباتپذیر ثابت است، نه فقط فرضی.»
Ironwood هنوز در حال توسعه است. کار تأیید صوری یک نقطه عطف کلیدی است، اما ارتقاء همچنان باید از فرآیند حاکمیتی Zcash عبور کند و توسط ماینرها و اپراتورهای گره پذیرفته شود. محققان قصد دارند با افزودن ویژگیهای جدید، مجموعه قضایا را گسترش دهند.
انتشار قضایا چیزی را برای کاربران فعلی Zcash تغییر نمیدهد. شبکه همچنان بر روی پروتکل موجود اجرا میشود. اما این کار یک پیشینه برای نحوه اعتبارسنجی ارتقاءهای آینده ایجاد میکند — با قطعیت ریاضی به جای صرفاً اطمینان.
مرحله بعدی یک دوره بازبینی جامعه است، پس از آن کد Ironwood برای فعالسازی پیشنهاد خواهد شد. هنوز تاریخی تعیین نشده است.
