Loading...
Серія: Серія про формальну верифікацію · Частина 2 з 3 Для кого: новачків. У частині 1 ми представили формальну верифікацію; тут ми розглянемо реальний баг, який зробив її нагальною. Усе необхідне пояснено з нуля. Що ви отримаєте: інтуїтивне, але точне уявлення про те, як криптографічна система доказів може містити діру в коректності, чим саме був баг Zcash «Orchard» 2026 року, чому цей клас багів може приховуватися роками та чому таке вже траплялося раніше.
У частині 1 ми сказали, що тестування може показати наявність багів, але ніколи — їхню відсутність, і що найнебезпечніші баги живуть у специфікації системи, її базовій математиці. Ця стаття — практичний приклад. У 2026 році в shielded pool Zcash Orchard було виявлено ваду, яка могла дозволити зловмиснику непомітно створювати необмежену кількість фальшивих грошей. Вона пережила чотири роки та повторні аудити. Розуміння її та її попередників — найпереконливіша можлива причина доводити правильність систем.
Zcash — це криптовалюта з приватним режимом. У її shielded pool суми, відправники та отримувачі транзакцій приховані. Ця приватність забезпечується доказами з нульовим розголошенням: криптографічними доказами того, що транзакція дотримується всіх правил, не розкриваючи її вміст.
Ця конструкція має дві сторони. У прозорому реєстрі, як-от у Bitcoin, якщо хтось створить монети з нічого, завищені числа будуть видимі всім, а мережа зможе це виявити й скасувати. У shielded pool числа навмисно приховані. Тож якби сама система доказів мала ваду, яка дозволяє недійсній транзакції виглядати дійсною, підробка була б невиявною. Її неможливо було б помітити, переглядаючи реєстр, оскільки реєстр навмисно непрозорий.
Саме цей ризик реалізувався в Orchard. Щоб зрозуміти його, нам потрібно зазирнути всередину того, що насправді перевіряє доказ із нульовим розголошенням.
Уявіть прикордонника, який має схвалювати мандрівників, не бачачи їхніх документів безпосередньо. Натомість кожен мандрівник заповнює контрольний список, а прикордонник схвалює кожного, чий список повністю позначений. Список спроєктовано так, що лише законний мандрівник може позначити кожен пункт.
Тепер припустімо, що в списку бракує одного критично важливого пункту, наприклад «паспорт не прострочений». Майже всі все одно заповнюють його чесно, і ніщо не виглядає неправильним. Але людина з простроченим паспортом також може позначити всі решту пунктів і безперешкодно пройти. У щоденному використанні система виглядає нормально. Діра має значення лише для того, хто цілеспрямовано її шукає.
Доказ із нульовим розголошенням працює як такий контрольний список. Він не розкриває приватні деталі; він перевіряє, чи відповідають вони фіксованому набору умов. І якщо одну необхідну умову випадково пропущено, деякі недійсні входи також можуть пройти, тоді як усе й далі виглядає нормально.
Зробімо «контрольний список умов» точним, адже саме там жив баг.
Під капотом твердження «ця транзакція дійсна» кодується як схема: фіксований набір арифметичних умов, які називаються обмеженнями та записуються як рівняння над числами. Щоб створити дійсний доказ, доводник має надати секретні значення (свідка), які задовольняють кожне обмеження. Доказ переконує верифікатора, що такий свідок існує, не розкриваючи його.
Властивість, яка нам потрібна від цієї системи, має назву:
Коректність: має бути неможливо створити дійсний доказ для хибного твердження. Лише істинні твердження повинні мати свідків, які задовольняють усі обмеження.
Коректність — це гарантія проти підробки. Якщо коректність зберігається, дійсний доказ справді означає: «відбулася реальна транзакція, що дотримується правил». Якщо в коректності є прогалина, дійсний доказ може взагалі нічого не означати.
Обмеження часто мають змушувати значення бути простим. Поширений приклад: змусити значення b бути одним бітом, тобто 0 або 1. Стандартний спосіб зробити це — одне обмеження:
b × (b − 1) = 0
Чому це працює? Добуток дорівнює нулю лише тоді, коли один із його множників дорівнює нулю. Отже, b × (b − 1) = 0 примушує b = 0 або b = 1, і нічого іншого. Якщо перевірити кожне значення від 0 до 16 (в арифметиці, яка переходить до початку після 17), єдиними значеннями, що його задовольняють, будуть рівно 0 і 1. ✓
А тепер уявіть, що цей рядок випадково пропущено зі схеми. Раптом b не має обмежень. Нечесний доводник може встановити b у 5, або 9, або будь-що взагалі, і все одно задовольнити решту обмежень. Цей один пропущений рядок — це прогалина коректності: хибні твердження тепер мають свідків, які задовольняють умови.
Це не гіпотетичний випадок. Відсутнє булеве обмеження саме такого виду було виявлено в найпершій shielded-конструкції Zcash, Sprout, під час розробки й виправлено до запуску. Недостатнє накладання обмежень є однією з найпоширеніших і найнебезпечніших помилок у побудові таких схем.
Це вся форма бага Orchard у малому масштабі. Тепер — реальний випадок.
Shielded-докази Zcash побудовані на еліптичних кривих — математичних об’єктах, чиї точки можна поєднувати та «множити» на числа; ці операції схема має забезпечувати обмеженнями. Схема містить компоненти, які виконують множення на еліптичній кривій та перевіряють, що воно виконане правильно.
Згідно з розкриттям Shielded Labs і дослідника Taylor Hornby, вада Orchard була саме такою:
Недостатньо обмежений елемент схеми Orchard уможливлював подання довільних хибних входів до множення на еліптичній кривій, і перевірка множення все одно проходила.
Простими словами, у контрольному списку схеми бракувало пунктів, які мали однозначно визначати це множення. Через прогалину достатньо досвідчений зловмисник міг сконструювати доказ транзакції, який система прийняла б, хоча транзакція створювала вартість із нічого. Це підробка, і оскільки суми у shielded pool приховані, її неможливо було б виявити з реєстру. Пізніше команда Tachyon описала ту саму ваду на рівні коду як відсутні рядки у схемі, які непомітно спотворювали базові рівняння.
Паралелі з нашою історією про контрольний список точні:
| Історія про контрольний список | Баг Orchard |
|---|---|
| Відсутній пункт «паспорт не прострочений» | Відсутнє обмеження на множення на еліптичній кривій |
| Мандрівник із простроченим паспортом усе одно проходить | Довільні хибні входи проходять перевірку множення |
| На всіх інших це не впливає, тому ніщо не виглядає неправильним | Звичайні транзакції працювали ідеально, приховуючи ваду |
| Діру знаходить лише той, хто її шукає | Знадобився експерт, який навмисно досліджував математику схеми |
Щоб було зрозуміло, наскільки це серйозно: дослідник за допомогою AI написав повний робочий експлойт і підтвердив у локальній тестовій мережі, що він створює необмежену кількість невиявних фальшивих монет. Це була реальна й придатна до експлуатації вада, а не теоретична загроза.
Баг існував у Orchard від його активації у травні 2022 року до екстреного виправлення у червні 2026 року, переживши повторні професійні аудити одних із найкращих криптографів світу. Як?
Тому що, як попереджала частина 1, тестування вибирає окремі випадки, а ця вада існувала у випадку, який ніхто не вибрав. Звичайні транзакції ніколи не задіювали відсутнє обмеження, тому кожен тест проходив і кожен день нормальної роботи виглядав бездоганно. Вада була досяжною лише через навмисне конструювання незвичайного свідка, націленого безпосередньо на прогалину. Зрештою її знайшли не запуском тестів, а міркуванням про математику схеми.
Саме відкриття є ознакою того, куди рухається безпека. У квітні 2026 року Shielded Labs залучила дослідника безпеки Taylor Hornby спеціально для полювання саме на такі вади. Невдовзі після виходу нової передової AI-моделі (Claude Opus 4.8 від Anthropic) наприкінці травня 2026 року Hornby застосував її разом із власним інструментарієм аналізу та традиційними методами для цільового огляду схеми Orchard. 29 травня 2026 року огляд виявив уразливість.
Варто прямо сказати про два тверезі факти з розкриття:
Баг Orchard належить до повторюваної родини, і розуміння цієї родини робить формальну верифікацію не просто бажаною, а неминучою. Вада підробки завжди походить з одного з трьох джерел (таксономія з частини 1): специфікації (самої математики), реалізації (коду, який не дотримується правильної математики) або зламаного припущення. І найважливіше:
Баг підробки є невиявним, лише якщо він живе у специфікації. Баги реалізації залишають постійні публічні докази, оскільки кожен блок записує повний вміст кожної транзакції, тож повторне відтворення історії виправленим програмним забезпеченням виявило б будь-яку транзакцію, яку помилково прийняв багований код.
Власна історія Zcash ілюструє цю закономірність:
| Баг (рік) | Джерело | Виявний? |
|---|---|---|
| Вада commitment Zerocash (2016, до запуску) | Специфікація (усічений хеш зламав властивість зв’язування) | Невиявний |
| Вада коректності довіреного налаштування (2018) | Специфікація (помилка в базовій статті про zk-SNARK) | Невиявний |
| Колізія запитів системи доказів (2025) | Специфікація (відсутня перевірка у системі доказів) | Виявний |
| Баг перевірки підгрупи кривої (2016) | Реалізація (відсутня перевірка підгрупи) | Виявний |
| Недостатньо обмежене множення Orchard (2026) | Специфікація (схема) | Невиявний |
Спільна лінія разюча: вади, які могли б приховуватися вічно, — це вади в математиці. Саме цей клас може усунути машинно перевірений доказ специфікації, одразу для всіх випадків. Тестування та аудит вибирають зразки; лише доведення математики охоплює кожен вхід.
Розробники Zcash діяли швидко та поетапно:
Саме на цьому другому кроці формальна верифікація входить в історію, і це тема частини 3. Варто заздалегідь розглянути усвідомлення, за яким діяла команда, бо воно пов’язує всю цю серію:
Невиявна вада підробки може існувати лише у специфікації протоколу. Тож якщо ви можете довести, що специфікація виключає підробку, ви усуваєте цілий клас багів, який тут ховався чотири роки.
Саме це є ідеєю першого стовпа з частини 1: верифікуйте специфікацію — і ви закриєте прогалину, яку тестування ніколи не могло закрити.
Ми навмисно спростили. Реальна схема містить сотні областей і багато тисяч обмежень, а фактична вада технічно складніша за одну відсутню перевірку біта; ми використали перевірку біта, оскільки вона точно показує форму недостатньо обмеженої схеми і тому, що саме така помилка реально була в історії Zcash. Точною вадою Orchard було недостатньо обмежене множення на еліптичній кривій, як сказано в офіційному розкритті. Ми також стисло виклали хронологію розкриття та усунення. Щоб ознайомитися з авторитетним технічним описом, зверніться до розкриття Shielded Labs і матеріалів Project Tachyon.
b(b−1)=0 примушує b бути 0 або 1; приберіть його — і b може бути будь-чим. Саме цей клас бага реальний в історії Zcash.)| Термін | Значення простою англійською |
|---|---|
| Shielded pool | Приватний режим Zcash, у якому суми та сторони приховані |
| Zero-knowledge proof | Доказ того, що приховане твердження дійсне, без розкриття будь-чого іншого |
| Circuit | Фіксований набір арифметичних умов, яким має відповідати дійсна транзакція |
| Constraint | Одна умова (рівняння) всередині схеми |
| Witness | Секретні значення, які задовольняють обмеження |
| Soundness | Гарантія, що лише істинні твердження можуть створити дійсний доказ |
| Soundness gap | Відсутнє обмеження, яке дозволяє хибним твердженням пройти |
| Under-constrained | Схема, у якій бракує потрібної умови, першопричина бага Orchard |
| Detectable / undetectable | Чи залишить експлуатація докази у публічному реєстрі |
Чи було насправді створено фальшиві Zcash? Доказів експлуатації не виявлено, і команда вважає її малоймовірною. Але оскільки вада була б невиявною з реєстру, сам реєстр не може повністю довести, що цього ніколи не сталося, тому відповідь була настільки ретельною.
Чому приховування сум робить баг гіршим? У прозорому ланцюзі створені монети видно, їх можна виявити та скасувати. Коли суми приховані заради приватності, баг підробки не створює видимої аномалії, тож він може існувати непоміченим.
Чому роки аудитів не виявили його? Аудити й тести здебільшого перевіряють поведінку на реалістичних випадках. Ця вада проявлялася лише за навмисно сконструйованого, незвичайного входу, націленого на математичний граничний випадок, який звичайний огляд не перевіряв. Її знайшли цільовим міркуванням про схему, а не тестуванням.
Невже одного відсутнього обмеження справді достатньо? Так. Система доказів настільки сильна, наскільки сильний її повний набір обмежень. Однієї пропущеної необхідної умови достатньо, щоб пропустити недійсні твердження.
Яку роль відіграв AI? Дослідник використав передову AI-модель разом із власним інструментарієм і традиційними методами, щоб перевірити математику схеми та знайти ваду. AI дедалі частіше застосовується з обох боків безпеки, і це є частиною причини, чому доведення правильності систем зараз має таке велике значення.
Припустімо, shielded-транзакція має довести, що «гроші на вході дорівнюють грошам на виході», але схема забуває накласти обмеження на одне вихідне значення. Що може зробити нечесний доводник і чому публічний реєстр виглядатиме цілком нормально? (Відповідь нижче.)
Коли цей вихід не має обмежень, доводник може встановити його більшим, ніж дозволяють реальні входи, створивши вартість із нічого — підробку. Доказ усе одно пройде перевірку, оскільки відсутнє обмеження є єдиним, що могло б виявити дисбаланс. А оскільки shielded pool приховує суми, реєстр показує лише, що «відбулася дійсна транзакція», без видимого дисбалансу, який міг би викликати тривогу. Підробка реальна, але невидима — саме тому коректність схеми настільки важлива й чому її потрібно доводити, а не тестувати.
Частина 3 · Ironwood: виправлення було не просто латкою. Інженери Zcash побудували новий shielded pool і супроводили його машинно перевіреним математичним доказом, що складається з понад 2 700 теорем, написаних у помічнику доведень Lean, що він не може створювати фальшиві гроші за заявлених припущень. Ми побачимо, що означають «цілісність балансу» та «коректність знання», що саме доказ охоплює і чого не охоплює, а також як старий pool було безпечно виведено з експлуатації.
Частина серії про формальну верифікацію для ZecHub.