Исследователи Zcash опубликовали набор из более чем 2700 теорем, проверенных машиной, предназначенных для устранения необнаруживаемых ошибок подделки в предстоящем обновлении протокола Ironwood. Работа, выполненная командой, стоящей за криптовалютой, ориентированной на конфиденциальность, направлена на математическое доказательство того, что новый код не может быть использован для создания фальшивых монет без обнаружения.
Что проверяют теоремы
Теоремы сосредоточены на Ironwood — запланированном обновлении консенсусных правил Zcash. Ошибки подделки — это класс уязвимостей, позволяющих злоумышленнику создавать монеты «из воздуха», что является катастрофическим сбоем для любой криптовалюты. Используя формальную верификацию, исследователи могут математически доказать, что определённые свойства выполняются для любого возможного выполнения кода, а не полагаться только на ручные аудиты или тестирование.
2700 теорем охватывают основную логику shielded-транзакций Ironwood, где балансы и суммы транзакций зашифрованы. Доказательства проверяют, что система обеспечивает инварианты эмиссии — то есть не может быть создано больше Zcash, чем разрешено протоколом, даже в условиях атаки. Исследователи утверждают, что такой подход выявляет граничные случаи, которые могут быть пропущены при традиционном ревью кода.
Почему важны проверенные машиной доказательства
Формальная верификация редко используется в разработке криптовалют, поскольку она требует много времени и специальных знаний. Большинство проектов полагаются на баг-баунти и ручные аудиты, которые могут оставлять пробелы. Zcash уже применял формальные методы ранее — для оригинального обновления Sapling, — но работа над Ironwood является крупнейшим таким применением для сети на сегодняшний день.
Теоремы написаны на языке Lean — ассистенте доказательств, который проверяет каждый шаг рассуждений. Если теорема проходит проверку, это означает, что свойство гарантировано для всех входных данных. Исследователи опубликовали полный набор доказательств вместе со спецификацией Ironwood, что позволяет сообществу провести независимую верификацию.
«Речь идёт о том, чтобы дать максимально сильную гарантию, что математика, лежащая в основе Ironwood, безупречна», — заявила команда. «Мы хотим, чтобы пользователи знали: эмиссия проверимо фиксирована, а не просто предполагается таковой».
Ironwood всё ещё находится в разработке. Формальная верификация — важная веха, но обновление ещё должно пройти через процесс управления Zcash и быть принято майнерами и операторами узлов. Исследователи планируют расширять набор теорем по мере добавления новых функций.
Публикация теорем ничего не меняет для текущих пользователей Zcash. Сеть продолжает работать на существующем протоколе. Однако эта работа создаёт прецедент для того, как будущие обновления могут валидироваться — с математической определённостью, а не просто с уверенностью.
Следующий шаг — период общественного обсуждения, после которого код Ironwood будет предложен для активации. Дата пока не назначена.
