Loading...
Серия: Серия о формальной верификации · Часть 1 из 3 Для кого: для абсолютных новичков. Предполагается, что у вас нет знаний в математике, программировании или криптографии. Что вы узнаете: чёткое понимание того, что значит доказать корректность программного обеспечения, почему это принципиально отличается от тестирования, что представляет собой машинно проверяемое доказательство и каковы точные (и честные) пределы того, что такое доказательство может гарантировать.
Большинству программного обеспечения доверяют, потому что его тестировали: мы запускаем его на множестве входных данных и наблюдаем за его поведением. Формальная верификация ставит более смелый вопрос. Можно ли доказать с математической достоверностью, что система делает то, что должна, для каждого возможного входа, включая те, которые никому и в голову не пришло попробовать? Эта статья объясняет эту идею с самых основ. Сначала интуитивное понимание, без символов, пока они не понадобятся.
Вот реальная история — и причина существования этой серии.
В 2022 году криптовалюта, ориентированная на конфиденциальность, Zcash запустила новый экранированный пул под названием Orchard, позволявший людям проводить транзакции со скрытыми суммами. Четыре года он работал безупречно и прошёл неоднократные профессиональные аудиты. Затем, в мае 2026 года, исследователь безопасности, тщательно анализируя лежащую в основе математику (с помощью инструментов ИИ), обнаружил единственное недоопределённое место в математике системы. Этот пробел мог позволить злоумышленнику создать неограниченное количество поддельных денег, а поскольку суммы были скрыты, никто бы этого не заметил. Уязвимость существовала всё это время.
Её не выявило тестирование. Все тесты успешно проходили в течение четырёх лет. Её обнаружил человек, рассуждавший о математике. И когда команда исправила проблему, она не просто внесла исправление и пошла дальше. Она написала машинно проверяемое математическое доказательство, охватывающее более 2700 отдельных теорем, что замена вообще не может содержать уязвимость такого класса.
Это и есть формальная верификация; вот что она даёт: не «мы испробовали много случаев, и они сработали», а «мы доказали, что это верно для каждого случая». Для систем, где один упущенный случай имеет катастрофические последствия (деньги, самолёты, медицинские устройства, криптография), эта разница решает всё.
Слепую зону тестирования десятилетия назад назвал специалист по информатике Эдсгер Дейкстра, и это по-прежнему верно:
Тестирование может показать наличие ошибок, но никогда их отсутствие.
Если тест прошёл, вы узнали, что система работает на этих входных данных. Вы не узнали ничего о входных данных, которые не пробовали, а опасные ошибки почти всегда находятся в случаях, которые никто не проверил.
Представьте, что вы отвечаете за здание с тысячей дверей, и ваша задача — гарантировать, что ночью каждая дверь заперта.
Разница состоит в выборочном наблюдении за реальностью и доказательстве свойства конструкции. Тестирование берёт выборки. Формальная верификация доказывает. В этом вся идея, а всё остальное — инструменты для её строгой реализации.
Любая формальная верификация, какой бы продвинутой она ни была, строится ровно на трёх компонентах. Чётко удерживайте их в уме — остальное лишь детали.
| Основа | Простое значение | Аналогия со зданием |
|---|---|---|
| Спецификация | Точное утверждение того, что означает «корректность» | «Каждая дверь должна быть заперта ночью» |
| Система | Реальный объект проверки (программа, схема, протокол) | Здание и его механизм запирания |
| Доказательство | Строгий аргумент, что система всегда соответствует спецификации | Логическая демонстрация того, что нажатие «запереть» запирает все двери |
И четвёртый, менее заметный компонент делает всё это заслуживающим доверия:
Среди ассистентов доказательств, названия которых вы можете услышать, — Lean, Rocq (ранее Coq) и Isabelle. По сути, это исключительно строгие механизмы проверки логики. Доказательство Zcash из нашей вступительной истории было написано в Lean. Примечательно, что современные модели ИИ всё чаще используются, чтобы помогать писать такие доказательства под руководством людей; это сократило работу, которая раньше занимала годы, до недель. Машина всё равно проверяет каждый шаг, поэтому ускорение не снижает достоверность.
Слово «доказательство» может пугать, поэтому разберём его на конкретном проверяемом примере. Никакой криптографии, только школьная арифметика.
Утверждение: для каждого целого неотрицательного числа n сумма 0 + 1 + 2 + ... + n равна n(n+1)/2.
Можно было бы проверить это. n = 5 даёт 0+1+2+3+4+5 = 15, и 5 × 6 / 2 = 15. ✓ Совпадает. Попробуем n = 10: сумма равна 55, а формула даёт 10 × 11 / 2 = 55. ✓ (Это было вычислено и подтверждено; утверждение действительно верно для каждого n от 0 до 999 при прямой проверке.)
Но проверка значений, даже тысячи из них, никогда не достигает утверждения «для каждого целого неотрицательного числа». Их бесконечно много. Доказательство закрывает этот бесконечный разрыв конечным аргументом с помощью метода под названием индукция:
n = 0 сумма равна просто 0, а формула даёт 0 × 1 / 2 = 0. Они совпадают. ✓k. Теперь прибавим следующее число, k+1. Сумма до k+1 равна (sum up to k) + (k+1) = k(k+1)/2 + (k+1). Одна строка алгебраических преобразований сводит это к (k+1)(k+2)/2, что в точности является формулой с k+1 вместо k. ✓Поскольку это верно в начале (при 0) и каждый шаг переносит утверждение к следующему числу, оно верно для всех целых неотрицательных чисел навсегда — в одном конечном аргументе. Это и есть доказательство. Ассистент доказательств выполняет точно такое же рассуждение, но механически проверяет, что каждый шаг, включая «строку алгебры», действительно следует из предыдущего.
Важный вывод: доказательство превращает «бесконечно много случаев» в конечный, проверяемый аргумент. Это сверхспособность, которой тестирование структурно лишено.
Формальная верификация сильна отчасти благодаря проясняющему пониманию того, откуда вообще берутся ошибки. Любая уязвимость в системе проверки правил восходит к одному из трёх источников:
| Источник ошибки | Что это означает | Можем ли мы доказательно устранить её? |
|---|---|---|
| Спецификация | Сама математика или правила неверны (пропущено условие, ошибочно дано определение) | Да, напрямую; это ключевая область формальной верификации |
| Реализация | Код не выполняет корректную спецификацию в точности | Частично; часто такие сбои оставляют обнаружимые следы |
| Нарушенное предположение | Оказывается ложным то, на что опирается вся система | Нет; предположения — неустранимый фундамент |
Эта классификация важнее, чем кажется, и на ней строятся части 2 и 3. Самые глубокие и опасные ошибки, которые могут оставаться скрытыми вечно, обычно находятся в спецификации: математическом описании того, что система должна делать. А спецификацию машинно проверяемое доказательство может исследовать непосредственно, сразу для всех случаев. Поэтому серьёзные усилия по формальной верификации прежде всего направлены именно туда.
Формальная верификация сильна, но её обещание строго определено, и неверное его понимание вводит людей в заблуждение. Поэтому сформулируем его осторожно:
Доказательство гарантирует, что система соответствует спецификации при указанных предположениях. Ничего более.
Из этого следуют четыре последствия, и важно каждое из них:
Эта точность не ослабляет формальную верификацию, а является её силой. Она сообщает вам точно, что вы получаете. Как мы увидим в части 3, команда Zcash, ясно обозначающая свою область охвата и предположения («мы доказали корректность эмиссии при этих названных предположениях, но не конфиденциальность»), является образцом такой честности.
Чтобы сохранить понятность текста, мы упростили изложение. Реальные спецификации пишутся на точных формальных языках, а не английскими предложениями; существует несколько стилей формальной верификации (интерактивное доказательство теорем, проверка моделей, методы на основе SMT), подходящих для различных задач; а написание этих доказательств остаётся работой, требующей навыков и усилий, даже с помощью ИИ. Мы также не рассмотрели, как ассистент доказательств внутренне представляет логику. Ничто из этого не меняет сути: спецификация, система и машинно проверяемое доказательство того, что они согласованы при указанных предположениях. Мы вернёмся к деталям, когда они понадобятся.
| Термин | Простое значение |
|---|---|
| Formal verification | Математическое доказательство того, что система соответствует спецификации во всех случаях |
| Specification | Точное утверждение того, что означает «корректное поведение» |
| System | Реальная проверяемая программа, схема или протокол |
| Proof | Конечная цепочка логических шагов, устанавливающая утверждение для всех случаев |
| Proof assistant / theorem prover | Программное обеспечение (Lean, Rocq, Isabelle), которое проверяет каждый шаг доказательства |
| Machine-checked | Проверенное компьютером шаг за шагом, а не только при чтении человеком |
| Induction | Метод доказательства: утверждение верно в начале, и каждый шаг переносит его к следующему |
| Assumption | Условие, на которое опирается доказательство; если оно ложно, гарантия может не выполняться |
Заменяет ли формальная верификация тестирование? Нет. Они дополняют друг друга. Тестирование недорого выявляет практические проблемы и ошибочные предположения; верификация исключает целые классы ошибок, которые тестирование может никогда не проверить.
Если она настолько сильна, почему не всё проходит формальную верификацию? Она дорога и требует специализированных навыков, хотя помощь ИИ снижает эту стоимость. Её применяют к системам, где редкая ошибка имела бы катастрофические последствия, — именно там её затраты оправданы.
Может ли формально верифицированная система всё же отказать? Да, если спецификация была неверной, определение было ошибочно сформулировано, предположение не выполнилось или сбой находится вне описанного в спецификации. Доказательство покрывает лишь то, что оно заявляет.
Машинно проверяемое доказательство надёжнее человеческого? Для больших и сложных доказательств, как правило, да. Машина не пропустит незаметный пробел и не примет рассуждение «на словах», хотя она всё ещё доверяет переданным ей спецификации и определениям.
Если ИИ помогает писать доказательство, почему ему можно доверять? Потому что ассистент доказательств механически проверяет каждый шаг. ИИ предлагает шаги; машина их проверяет. Неверный шаг просто отклоняется, поэтому ИИ ускоряет работу, не ослабляя гарантию.
Вы доказываете, что банковское программное обеспечение «никогда не допускает отрицательного баланса счёта». Год спустя деньги всё ещё исчезают. Как оба утверждения могут быть верны одновременно? (Ответ ниже.)
Доказательство гарантировало ровно одно свойство: балансы никогда не становятся отрицательными. Деньги могут исчезать способами, которых это свойство не касается: например, из-за ошибки, переводящей средства на неверный (но всё ещё с неотрицательным балансом) счёт, или из-за уязвимости в части системы, которая никогда не была описана в спецификации. Верификация в точности выполнила обещанное и ничего более. Это действие оговорки из раздела 6: доказательство покрывает спецификацию, а не все мыслимые представления о «корректности».
Часть 2 · Ошибка Orchard: мы подробно рассмотрим реальную историю 2026 года. Система конфиденциальности скрывала суммы с помощью криптографических доказательств, и одна недоопределённая строка в её математике означала, что эти доказательства можно было заставить лгать, позволяя неограниченную незаметную подделку денег. Мы точно увидим, что означает «недоопределённая схема», почему ошибки этого класса могут оставаться скрытыми вечно и почему это случалось не один раз.
Часть серии Formal Verification для ZecHub.