Zcash звертається до формальної верифікації, щоб запобігти невиявленню помилок підробки

Розробники Zcash використовують формальну верифікацію для оновлення мережі Ironwood та захищеного пулу, щоб уникнути недосяжних помилок підробки після нещодавно виявленої вразливості в Orchard, яка продемонструвала обмеженість традиційних аудиторських перевірок.

У блозі, опублікованому у вівторок, розробник і криптодослідник Шон Бо розповів про цю ситуацію. Ironwood має на меті виправити облікову помилку, виявлену у захищеному пулі Orchard, та відновити довіру до цілісності поставок криптовалюти.

Цю помилку знайшов дослідник Shielded Labs Тейлор Хорнбі, а вона була виправлена до будь-якої відомої експлуатації. Розробники зазначили, що недосяжна підробка може виникнути лише внаслідок недоліків у математичній специфікації протоколу або через зламані криптографічні припущення, тоді як помилки в реалізації завжди залишають сліди, які можна виявити, повторюючи блокчейн з виправленим програмним забезпеченням. Команда підтвердила, що формальна верифікація зосередиться на доведенні правильності криптографічної специфікації Ironwood, а не на аудиті реалізаційного коду, вважаючи це достатнім для виключення недосяжних помилок підробки за стандартними криптографічними припущеннями. Робота проводиться за участі фахівців zkSecurity та Zcash Open Development Lab із використанням теоремного провідника Lean разом із традиційними аудитами та аналізом за допомогою штучного інтелекту. Очікується, що Ironwood запрацює в липні 2026 року, закриваючи старий захищений пул і запускаючи виправлену версію.

Користувачі зможуть перемістити свої кошти через механізм "турнікет", створений для того, щоб довести, що жоден підроблений ZEC не потрапив в обіг, при цьому обмеживши кількість вартості, яка залишиться в Orchard.