Loading...
Серия: Серия о формальной верификации · Часть 2 из 3 Для кого: для новичков. В части 1 была представлена формальная верификация; здесь мы рассмотрим реальную ошибку, которая сделала её необходимой. Всё необходимое объясняется с нуля. Что вы узнаете: интуитивное, но точное представление о том, как в криптографической системе доказательств может возникнуть брешь в корректности, чем именно была ошибка «Orchard» 2026 года в Zcash, почему этот класс ошибок может скрываться годами и почему это уже случалось раньше.
В части 1 мы говорили, что тестирование может показать наличие ошибок, но никогда не их отсутствие, и что самые опасные ошибки живут в спецификации системы, её базовой математике. Эта статья — практический пример. В 2026 году в экранированном пуле Zcash Orchard был найден дефект, который мог позволить злоумышленнику незаметно создавать неограниченное количество фальшивых денег. Он пережил четыре года и неоднократные аудиты. Понимание этой ошибки и её предшественников — наиболее наглядная причина доказывать корректность систем.
Zcash — криптовалюта с приватным режимом. В её экранированном пуле суммы, отправители и получатели транзакций скрыты. Эта приватность создаётся с помощью доказательств с нулевым разглашением: криптографических доказательств того, что транзакция соблюдает все правила, без раскрытия её содержимого.
У такой конструкции две стороны. В прозрачном реестре, таком как у Bitcoin, если бы кто-то создал монеты из ничего, увеличенные числа были бы видны всем, и сеть могла бы обнаружить это и отменить операцию. В экранированном пуле числа намеренно скрыты. Поэтому, если бы в самой системе доказательств был дефект, позволяющий недействительной транзакции выглядеть действительной, подделка была бы необнаружимой. Её нельзя было бы заметить, изучая реестр, поскольку реестр намеренно непрозрачен.
Именно этот риск реализовался в 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, или вообще что угодно и всё равно удовлетворить оставшимся ограничениям. Эта единственная отсутствующая строка — брешь в корректности: у ложных утверждений теперь есть удовлетворяющие свидетели.
Это не гипотетический пример. Отсутствующее булево ограничение именно такого типа было найдено в первом экранированном дизайне Zcash, Sprout, во время разработки и исправлено до запуска. Недостаточное ограничение — одна из самых распространённых и опасных ошибок при создании таких схем.
Такова вся структура ошибки Orchard в малом масштабе. Теперь — реальная ситуация.
Экранированные доказательства Zcash построены на эллиптических кривых — математических объектах, точки которых можно комбинировать и «умножать» на числа; эти операции схема должна обеспечивать ограничениями. Схема содержит гаджеты, выполняющие умножение на эллиптической кривой и проверяющие, что оно выполнено корректно.
Согласно раскрытию информации Shielded Labs и исследователя Taylor Hornby, дефект Orchard заключался именно в следующем:
Недостаточно ограниченный элемент схемы Orchard позволял передавать произвольные ложные входные данные в умножение на эллиптической кривой и при этом успешно проходить проверку умножения.
Проще говоря, в контрольном списке схемы отсутствовали пункты, которые должны были однозначно зафиксировать это умножение. Из-за этой бреши достаточно квалифицированный злоумышленник мог построить доказательство транзакции, которое система приняла бы, хотя транзакция создавала стоимость из ничего. Это подделка, и, поскольку суммы в экранированном пуле скрыты, она была бы необнаружимой по реестру. Позже команда Tachyon описала тот же дефект на уровне кода как отсутствующие строки в схеме, незаметно искажавшие базовые уравнения.
Параллели с нашей историей о контрольном списке точны:
| История о контрольном списке | Ошибка Orchard |
|---|---|
| Отсутствует пункт «паспорт не просрочен» | Отсутствует ограничение на умножение на эллиптической кривой |
| Путешественник с просроченным паспортом всё равно проходит | Произвольные ложные входные данные проходят проверку умножения |
| На остальных это не влияет, поэтому ничего не выглядит неправильным | Обычные транзакции работали безупречно, скрывая дефект |
| Брешь находит только тот, кто специально её ищет | Потребовался эксперт, целенаправленно исследовавший математику схемы |
Чтобы было ясно, насколько это серьёзно: исследователь с помощью ИИ написал полностью работающий эксплойт и подтвердил в локальной тестовой сети, что он создаёт неограниченное количество необнаружимых фальшивых монет. Это был реальный, эксплуатируемый дефект, а не теоретическая тревога.
Ошибка существовала в Orchard с её активации в мае 2022 года до экстренного исправления в июне 2026 года, пережив неоднократные профессиональные аудиты, проведённые одними из лучших криптографов мира. Как?
Потому что, как предупреждала часть 1, тестирование выбирает отдельные случаи, а этот дефект находился в случае, который никто не выбрал. Обычные транзакции никогда не задействовали отсутствующее ограничение, поэтому все тесты проходили и каждый день нормальной работы выглядел безупречно. Дефект был достижим только при намеренном построении необычного свидетеля, точно нацеленного на брешь. В конечном счёте он был обнаружен не запуском тестов, а рассуждением о математике схемы.
Само обнаружение показывает, куда движется безопасность. В апреле 2026 года Shielded Labs привлекла исследователя безопасности Taylor Hornby специально для поиска именно такого рода дефектов. Вскоре после выхода новой передовой модели ИИ (Claude Opus 4.8 от Anthropic) в конце мая 2026 года Hornby использовал её вместе со специальной средой анализа и традиционными методами для целевого обзора схемы Orchard. 29 мая 2026 года обзор обнаружил уязвимость.
Два трезвых факта из раскрытия стоит сформулировать прямо:
Ошибка Orchard относится к повторяющемуся семейству, и именно понимание этого семейства делает формальную верификацию не просто желательной, а неизбежной. Ошибка подделки всегда восходит к одному из трёх источников (таксономия из части 1): спецификации (самой математике), реализации (коду, не следующему корректной математике) или нарушенному предположению. И, что особенно важно:
Ошибка подделки необнаружима, только если она находится в спецификации. Ошибки реализации оставляют постоянные публичные следы, поскольку каждый блок записывает полное содержимое каждой транзакции; следовательно, повторное воспроизведение истории через исправленное программное обеспечение выявит любую транзакцию, которую ошибочный код неправильно принял.
Собственная история Zcash иллюстрирует эту закономерность:
| Ошибка (год) | Источник | Обнаружима? |
|---|---|---|
| Дефект обязательства 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? Доказательств эксплуатации не найдено, и команда считает её маловероятной. Но поскольку дефект был бы необнаружим по реестру, один лишь реестр не может полностью доказать, что этого никогда не случалось; именно поэтому ответные меры были столь основательными.
Почему сокрытие сумм делает ошибку хуже? В прозрачной цепочке созданные монеты видны, их можно обнаружить и отменить. Когда суммы скрыты ради приватности, ошибка подделки не создаёт видимой аномалии и может оставаться незамеченной.
Почему годы аудитов её не выявили? Аудиты и тесты в основном изучают поведение в реалистичных случаях. Этот дефект проявлялся только при намеренно составленном необычном входе, нацеленном на математический крайний случай, который обычная проверка не затрагивала. Его нашли целенаправленным рассуждением о схеме, а не тестированием.
Разве одного отсутствующего ограничения действительно достаточно? Да. Система доказательств настолько сильна, насколько силён её полный набор ограничений. Одного пропущенного необходимого условия достаточно, чтобы пропустить недействительные утверждения.
Какую роль сыграл ИИ? Исследователь использовал передовую модель ИИ вместе со специальной средой и традиционными методами, чтобы изучить математику схемы и найти дефект. ИИ всё чаще используется обеими сторонами в сфере безопасности; это одна из причин, почему сейчас так важно доказывать корректность систем.
Предположим, экранированная транзакция должна доказать, что «сумма входов равна сумме выходов», но схема забывает ограничить одно выходное значение. Что может сделать нечестный доказывающий и почему публичный реестр будет выглядеть совершенно нормально? (Ответ ниже.)
При отсутствии ограничения на этот выход доказывающий мог бы задать ему значение большее, чем позволяют реальные входы, создавая стоимость из ничего — подделку. Доказательство всё равно прошло бы проверку, поскольку отсутствующее ограничение — единственное, которое обнаружило бы дисбаланс. А поскольку экранированный пул скрывает суммы, реестр показывает лишь, что «произошла действительная транзакция», без видимого дисбаланса, который мог бы вызвать тревогу. Подделка реальна, но невидима — именно поэтому корректность схемы настолько важна и почему она должна быть доказана, а не протестирована.
Часть 3 · Ironwood: исправление было не просто заплаткой. Инженеры Zcash создали новый экранированный пул и сопроводили его машинно проверяемым математическим доказательством — более 2 700 теорем, записанных в помощнике доказательств Lean, — того, что при заявленных предположениях он не может создавать фальшивые деньги. Мы увидим, что означают «целостность баланса» и «корректность знания», что именно охватывает и не охватывает доказательство и как старый пул был безопасно выведен из эксплуатации.
Часть серии о формальной верификации для ZecHub.