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 | Правило, ограничивающее выходы пула его проверяемыми депозитами |
Означает ли доказательство, что Ironwood не содержит ошибок? Нет, и оно этого не утверждает. Оно доказывает одно точное свойство — целостность баланса — при заявленных предположениях. Это исключает незаметную подделку, но не все мыслимые ошибки.
Гарантирует ли доказательство конфиденциальность моих транзакций? Нет. Верификация охватывает надёжность эмиссии (отсутствие фальшивых денег), а не отдельные гарантии конфиденциальности пула. Они обосновываются иначе.
Почему следует доверять доказательству, написанному людьми (и ИИ)? Потому что оно проверяется машиной. Помощник доказательств Lean механически проверяет каждый шаг, поэтому доверие основано на спецификации и названных предположениях, а не на внимательности человека или ИИ на каждом шаге.
Что происходит с монетами, всё ещё находящимися в старом пуле Orchard? Их можно вывести, но лишь в пределах суммы, которая проверяемо поступила в пул, что обеспечивается турникетом. Это одновременно защищает целостность эмиссии и помогает показать, что старый недостаток никогда не был использован.
Это конец истории? Это важная веха, а не финишная черта. Будущая архитектура Zcash — Tachyon с инструментарием Ragu — создаётся с формальной верификацией как стандартной практикой, расширяя этот подход дальше.
Кто-то утверждает: «Поскольку Ironwood формально верифицирован, теперь уже невозможно, чтобы с Zcash когда-либо что-то пошло не так». Используя идеи всех трёх частей, назовите две разные причины, по которым это утверждение слишком сильно. (Ответ ниже.)
Во-первых, доказательство охватывает конкретное свойство — целостность баланса — при заявленных предположениях (сложность дискретного логарифма и стандартное моделирование хеша). Если криптографическое предположение будет нарушено или проблема возникнет за пределами описанного — например, в конфиденциальности, программном обеспечении кошелька или каком-либо недоказанном компоненте, — доказательство ничего об этом не говорит. Во-вторых, формальная верификация гарантирует, что система соответствует написанной спецификации; если сама спецификация не охватила какое-либо реальное требование, доказательство добросовестно сертифицирует неверную вещь. Оба пункта повторяют оговорку части 1: доказательство точно и ограничено, оно сильно именно потому, что его область действия честно определена, а не потому, что даёт всеобъемлющую гарантию невозможности любых проблем.
За три части мы прошли путь от общей идеи к работающему применению: от того, что значит доказать корректность программного обеспечения, а не тестировать его (часть 1), через то, как реальная недостаточно ограниченная схема могла бы создавать незаметные деньги (часть 2), к тому, как машино-проверяемое доказательство целостности баланса навсегда устранило этот класс ошибок (часть 3). Сквозная тема — одно честное обещание: не «ошибок никогда не будет», а «это точное свойство выполняется во всех случаях при заявленных предположениях». Для денег, скрывающих собственные суммы, именно такое обещание и стоит доказать.
Часть серии «Формальная верификация» для ZecHub.
| High-assurance cryptography |
| Создание криптографии, где формальная верификация является стандартным этапом |