Loading...
Серія: Формальна верифікація · Частина 3 із 3 Для кого: новачків. Частини 1 і 2 пояснюють формальну верифікацію та баг Orchard; ця фінальна частина показує, як ці дві ідеї зустрічаються в реальній системі. Усе необхідне ми нагадаємо в процесі. Що ви дізнаєтеся: точне розуміння того, що саме Zcash довела щодо свого нового пулу «Ironwood», як структуровано доказ, що він охоплює, а чого не охоплює, як старий пул було безпечно виведено з експлуатації та чому це вказує на новий стандарт створення криптографічних грошей.
У Частині 1 ми дізналися, що означає довести правильність системи. У Частині 2 ми побачили реальну ваду, яку тестування не помічало чотири роки: недостатньо обмежене множення на еліптичній кривій, що могло дозволити необмежену невидиму підробку грошей. Ця стаття є розв’язанням: як Zcash відповіла не просто виправленням, а машинно перевіреним доказом того, що весь клас таких багів усунено.
Коли баг загрожує грошам, звичайна реакція — виправити його й рухатися далі. Zcash зробила щось амбітніше. Разом із новим захищеним пулом під назвою Ironwood, активованим 28 липня 2026 року, її інженери опублікували машинно перевірений математичний доказ із понад 2 700 теорем, написаних у помічнику для доведень Lean, який встановлює, що новий пул не може створювати підроблені монети за заявлених припущень. Доказ є публічним, у репозиторії ironwood з відкритим кодом, і для його завершення трьом командам дослідників і криптографів знадобилося значно більше місяця.
Це важливо не лише для Zcash. Це одна з найчіткіших реальних демонстрацій того, що можна взяти діючу фінансову систему, точно записати, що означає «без підробок», і довести це, а не сподіватися, що тести були достатньо ретельними. Це перетворює обіцянку на теорему.
Частина 2 завершилася ідеєю, яка зробила це можливим. Пригадайте її, адже на ній ґрунтується все далі:
Баг невиявної підробки може існувати лише у специфікації протоколу — математичному описі того, що має забезпечувати схема. Усе, що можна виявити, проявилося б у публічному обліку. Отже, доведення коректності специфікації одразу усуває весь клас багів прихованої підробки.
Чому «лише у специфікації»? Тому що кожен блок назавжди зберігає повний вміст кожної транзакції, зокрема її докази. Якби програмне забезпечення помилково прийняло некоректну транзакцію, будь-хто міг би повторно прогнати історію через виправлене програмне забезпечення й побачити це. Ці докази є постійними та публічними. Лише вада в базовій математиці може ховатися назавжди, бо немає «правильної версії», з якою можна повторно зіставити дані. Саме на таку ваду спрямована формальна верифікація.
Тестування перевіряє поведінку на вибраних вхідних даних, а баг Orchard ховався саме тому, що жоден вибраний вхід не потрапив у нього. Доказ щодо специфікації охоплює всі входи одночасно, зокрема крайні випадки, які ніхто не здогадався б спробувати. Це єдиний тип гарантії, достатньо сильний, щоб упевнено усунути чотирирічну невидиму ваду.
Доказ установлює одну головну властивість, побудовану на глибшій властивості під нею.
Цілісність балансу: прихована вартість, що зберігається в захищеному пулі, ніколи не перевищує чисту публічну вартість, яка до нього надійшла.
Це властивість протидії підробці у простій формі. Гроші можуть входити до захищеного пулу (публічно видимо) та виходити з нього (публічно видимо), але всередині, де суми приховані, жодну вартість не можна створити з нічого. Розгляньмо це на прикладі невеликої книги обліку (перевірена арифметика):
5 + 3 = 8 створюють виходи вартістю 4 + 4 = 8. Вартість на вході дорівнює вартості на виході. Цілісність балансу зберігається. ✓8, але виходи на 4 + 4 + 2 = 10. Це створило б 2 одиниць із нічого. Цілісність балансу забороняє це: пул ніколи не може виплатити більше, ніж до нього надійшло. ✗Цілісність балансу — це математичне твердження, що другий сценарій ніколи не може створити дійсну транзакцію.
Щоб гарантувати цілісність балансу, дослідники спочатку мали довести глибшу й тоншу властивість самої системи доказів із нульовим розголошенням. Звичайної обґрунтованості (з Частини 2: «лише істинні твердження мають свідка») виявляється недостатньо для захищеного пулу з цікавої причини: оскільки прихована транзакція може містити що завгодно, майже кожне твердження технічно має певного свідка. Тому дослідники довели сильнішу властивість:
Обґрунтованість знання: кожен, хто може створити дійсний доказ транзакції, мусить насправді володіти дійсним свідком, тобто справжніми монетами, правильно виведеними й на правильній адресі.
Формальним інструментом для цього є екстрактор: процедура, яка, маючи будь-якого довідника, здатного переконати перевіряча, може витягти з нього фактичного свідка. Якщо свідка завжди можна вилучити, то переконливий довідник справді мусив його мати. Мовою Частини 2, обґрунтованість знання — це формальна обіцянка, що немає прогалини обґрунтованості, немає пропущеного обмеження, яке дозволило б хибному твердженню пройти перевірку. Це саме та властивість, відсутність якої була багом Orchard. Доведення її наявності для всіх можливих довідників остаточно зачиняє ці двері.
Верифікація була серйозною людською працею, а не результатом натискання однієї кнопки:
ironwood.Для міркування про цю властивість модель Lean описує цілу книгу обліку як список транзакцій, кожна з яких містить свої дії, заявлену публічну вартість і підписи. Предикат, який дослідники називають ValidLedger, безпосередньо відтворює правила консенсусу мережі: свідок кожної дії має задовольняти необхідні умови, жоден маркер витрати (nullifier) не може з’являтися двічі, кожен згаданий стан дерева має бути тим, якого система справді досягла, а кожен підпис має пройти перевірку. Потім теореми квантифікують кожну дійсну книгу обліку. Ця фраза, «кожна дійсна книга обліку», і є суттю: не вибірка, а всі вони — надмножина всього, що реальний зловмисник міг би будь-коли зібрати.
Результат щодо цілісності балансу складається з кількох теорем рівня книги обліку, кожна з яких доводить, що один шлях до підробки закрито: кожна витрата відповідає реальному попередньому виходу, загальна вартість зберігається, отримана нота залишається придатною для витрати й не може бути викрадена, а витрачання потребує належної авторизації. Окрема частина — зв’язувальний підпис — пов’язує приховані вартості кожної транзакції з публічною сумою, яку вона заявляє, тому прихований і публічний облік не можуть непомітно розійтися.
Тонке й чесне запитання: доказ стосується математичної моделі, але мережа виконує код Rust. Як ми знаємо, що код відповідає моделі?
Команда провела ретельну межу, яку називає відбитком перевіряча. Вище межі докази Lean міркують про перевіряча як про точний математичний об’єкт. Нижче розташована звичайна реалізація на Rust. Ключовий аргумент той самий, що в Частині 2:
Будь-який спосіб, у який реальне програмне забезпечення могло б відхилитися від доведеної моделі, був би багом реалізації, а баги реалізації можуть породжувати лише виявну підробку, оскільки кожен прийнятий доказ назавжди записується й може бути повторно перевірений виправленим програмним забезпеченням.
Отже, доказ охоплює невиявний клас (специфікацію), а постійний публічний запис охоплює виявний клас (реалізацію). Між ними не залишається місця, де міг би сховатися невиявний баг підробки. Команда також виконала перехресну перевірку: запустила реальний перевіряч і підтвердила, що він точно відтворює відбиток на зафіксованих випадках.
Частина 1 наполягала, що доказ гарантує відповідність системи специфікації за заявлених припущень і ніколи не означає «жодних багів узагалі». Команда Zcash була похвально точною саме щодо цього, і чесний освітній матеріал має бути таким самим.
Доказ зводить безпеку Ironwood до невеликого набору стандартних, чітко названих припущень. Зокрема, його обґрунтованість спирається на складність задачі дискретного логарифма на еліптичній кривій, яку використовує Ironwood (це добре досліджене припущення; найкраща відома атака потребувала б порядку 2^126 операцій, що значно перевищує будь-які здійсненні обчислення), разом зі стандартними припущеннями моделювання хеш-функції. Варто прямо зазначити дві межі:
Далеко не применшуючи досягнення, називання цих меж робить його гідним довіри. Твердження є точним: за стандартних криптографічних припущень цей пул не може створювати невиявні підроблені монети. Це теорема, а не сподівання, і її точний обсяг відкрито заявлено.
Доведення коректності нового пулу все ще залишає запитання: а як щодо старого пулу Orchard, де вада існувала чотири роки? Його минуле неможливо зробити видимим. Але можна обмежити його майбутнє.
Zcash запровадила механізм під назвою турнікет. Правило просте й потужне:
Вартість може залишати старий пул лише в межах суми, яка перевірно надійшла до нього.
Оскільки рух грошей у захищений пул і з нього публічно видимий (прихованою є лише діяльність усередині), турнікет дає всій мережі змогу перевірити, що назовні не виходить більше, ніж будь-коли зайшло. Якби в старому пулі було створено підроблені монети, вони досягли б цього обмеження й не змогли б вийти. А коли чесні кошти мігрують назовні й надлишок не з’являється, спільнота отримує переконливі публічні докази того, що ваду ніколи не було використано. Це найближче до аудиту запасу приватного пулу без порушення його приватності, і це наближає цілісність емісії до прозорої моделі ланцюга на кшталт Bitcoin, зберігаючи приватність Zcash.
Сам Ironwood повторно використовує виправлену схему доказу, починає заново з порожнім пулом і додає перспективні механізми захисту (зокрема положення, завдяки яким кошти могли б залишатися відновлюваними, якщо майбутні квантові комп’ютери колись загрожуватимуть сучасній криптографії). Нова захищена активність тепер проходить через Ironwood, тоді як старий пул Orchard обмежений виведеннями коштів.
Ironwood є частиною ширшої зміни в тому, як будує Zcash. Її зусилля з масштабування нового покоління (архітектура під назвою Tachyon, побудована на рекурсивних доказах та інструментарії під назвою Ragu) розробляються відповідно до філософії, яку іноді називають криптографією з високим рівнем гарантій: машинно перевірена формальна верифікація розглядається не як запізніла думка, а як стандартна частина запуску нових криптографічних систем.
Логіка переконлива. Передова криптографія — саме та сфера, де людська інтуїція найслабша і де тонкий, неперевірений крайній випадок може ховатися роками, як показала Orchard. Доведення специфікації — це єдина техніка, що масштабується до «всіх можливих входів» і конструктивно закриває такі прогалини. Команда дала зрозуміти, що з часом має намір поширити цей контроль далі — на реалізацію та за її межі. Очікуйте, що цю планку ширше приймуть у Zcash і поза нею.
Для ясності ми спростили виклад. Реальна розробка в Lean значно детальніша за наведений тут нарис, із точними визначеннями дій, тверджень, комітментів, nullifier-ів і підписів; «цілісність балансу» та «обґрунтованість знання» мають точні формальні визначення, які ми подали лише словами; зведення до складності дискретного логарифма проходить через кілька проміжних моделей (алгебраїчну модель довідника та модель випадкового оракула для хешу), які ми стиснули до «стандартних припущень»; а відбиток і турнікет ми описали на концептуальному рівні. Ніщо з цього не змінює суттєвої історії: специфікація «без підробок», машинно перевірений доказ для всіх дійсних книг обліку, явний і чесний виклад обсягу та припущень і безпечне виведення дефектного пулу з експлуатації. Щоб ознайомитися з авторитетним викладом, зверніться до опублікованих матеріалів Project Tachyon про верифікацію та репозиторію доказів ironwood.
| Термін | Значення простими словами |
|---|---|
| Ironwood | Новий захищений пул Zcash (2026), що замінює дефектний пул Orchard |
| Balance integrity | Пул ніколи не виплачує більше вартості, ніж до нього надійшло публічно |
| Knowledge soundness | Дійсний доказ вимагає, щоб довідник мав справжнього свідка |
| Extractor | Процедура, що витягає свідка з будь-якого переконливого довідника |
| Lean | Помічник для доведень, використаний для машинної перевірки верифікації |
| ValidLedger | Формальна модель правил консенсусу, щодо якої міркують теореми |
| Fingerprint | Межа між доведеною математикою та запущеним програмним забезпеченням Rust |
| Under stated assumptions | Доказ діє за умови виконання названих криптографічних припущень |
| Turnstile | Правило, що обмежує виходи пулу його перевірними депозитами |
| High-assurance cryptography |
Чи означає доказ, що Ironwood не має багів? Ні, і він цього не стверджує. Він доводить одну точну властивість, цілісність балансу, за заявлених припущень. Це виключає невиявну підробку, а не кожен мислимий баг.
Чи гарантує доказ приватність моїх транзакцій? Ні. Верифікація охоплює обґрунтованість емісії (відсутність фальшивих грошей), а не окремі гарантії приватності пулу. Вони обґрунтовуються інакше.
Чому варто довіряти доказу, написаному людьми (та AI)? Тому що він машинно перевірений. Помічник для доведень Lean механічно перевіряє кожен крок, тому довіра спирається на специфікацію та названі припущення, а не на ретельність людини чи AI на кожному кроці.
Що відбувається з монетами, які залишилися у старому пулі Orchard? Їх можна вивести, але лише в межах суми, яка перевірно надійшла до пулу; це забезпечує турнікет. Це одночасно захищає цілісність емісії та допомагає продемонструвати, що стару ваду ніколи не було використано.
Чи це кінець історії? Це важлива віха, а не фінішна пряма. Майбутня архітектура Zcash (Tachyon з інструментарієм Ragu) будується з формальною верифікацією як стандартною практикою, що поширює цей підхід далі.
Хтось стверджує: «Оскільки Ironwood формально верифіковано, тепер неможливо, щоб із Zcash будь-коли щось пішло не так». Використовуючи ідеї з усіх трьох частин, наведіть дві різні причини, чому це твердження надто сильне. (Відповідь нижче.)
По-перше, доказ охоплює конкретну властивість (цілісність балансу) за заявлених припущень (складність дискретного логарифма та стандартне моделювання хешу). Якщо криптографічне припущення буде зламано або проблема виникне поза межами того, що було специфіковано (наприклад, у приватності, програмному забезпеченні гаманця чи якомусь недоведеному компоненті), доказ нічого про це не каже. По-друге, формальна верифікація гарантує, що система відповідає написаній специфікації; якщо сама специфікація не охопила якусь реальну вимогу, доказ бездоганно засвідчить неправильну річ. Обидва пункти повторюють застереження з Частини 1: доказ є точним і обмеженим, потужним саме тому, що його обсяг чесно визначено, а не загальною гарантією, що ніколи нічого не може піти не так.
У трьох частинах ми перейшли від загальної ідеї до застосування в діючій системі: що означає довести правильність програмного забезпечення замість тестувати його (Частина 1), як реальна недостатньо обмежена схема могла карбувати невидимі гроші (Частина 2), і як машинно перевірений доказ цілісності балансу назавжди усунув цей клас багів (Частина 3). Спільна лінія — одна чесна обіцянка: не «жодних багів ніколи», а «ця точна властивість виконується для кожного випадку за заявлених припущень». Для грошей, які приховують власні суми, це саме та обіцянка, яку варто довести.
Частина серії Formal Verification для ZecHub.
| Створення криптографії з формальною верифікацією як стандартним кроком |