Loading...
Серія: Серія про формальну верифікацію · Частина 1 з 3 Аудиторія: цілковиті новачки. Не передбачається знання математики, програмування чи криптографії. Що ви зрозумієте: чітке розуміння того, що означає довести правильність програмного забезпечення, чому це докорінно відрізняється від його тестування, що таке машинно-перевірений доказ і які точні (та чесні) межі того, що такий доказ може гарантувати.
Більшості програмного забезпечення довіряють, бо його тестували: ми запускаємо його на багатьох вхідних даних і спостерігаємо за його поведінкою. Формальна верифікація ставить сміливіше запитання. Чи можемо ми довести з математичною точністю, що система робить те, що повинна, для кожних можливих вхідних даних, включно з тими, які ніхто й не подумав спробувати? Ця стаття пояснює цю ідею з самих основ. Спочатку інтуїтивно — жодних символів, доки вони не стануть потрібними.
Ось правдива історія — і причина існування цієї серії.
У 2022 році криптовалюта, орієнтована на приватність, Zcash запустила новий захищений пул під назвою Orchard, що дозволяв людям здійснювати транзакції з прихованими сумами. Протягом чотирьох років він працював бездоганно та пройшов численні професійні аудити. Потім, у травні 2026 року, дослідник безпеки, ретельно аналізуючи базову математику (за допомогою інструментів AI), знайшов одну недостатньо обмежену ділянку в математиці системи. Ця єдина прогалина могла дозволити зловмиснику створити необмежену кількість підроблених грошей, і, оскільки суми були приховані, ніхто б не помітив цього. Вада існувала весь цей час.
Її не виявили тестуванням. Усі тести проходили чотири роки. Її знайшли завдяки тому, що хтось міркував про математику. А коли команда її виправила, вона не просто внесла латання й рушила далі. Вона написала машинно-перевірений математичний доказ, що охоплював понад 2 700 окремих теорем, який засвідчив, що заміна взагалі не може містити цього класу вад.
Ось що таке формальна верифікація і що вона дає вам: не «ми випробували багато випадків, і вони спрацювали», а «ми довели, що це виконується для кожного випадку». Для систем, де один пропущений випадок є катастрофічним (гроші, літаки, медичні пристрої, криптографія), ця різниця означає все.
Сліпу пляму тестування десятиліття тому назвав фахівець із комп'ютерних наук Едсгер Дейкстра, і це досі правда:
Тестування може показати наявність помилок, але ніколи їхню відсутність.
Якщо тест проходить, ви дізналися, що система працює на цих вхідних даних. Ви не дізналися нічого про вхідні дані, які не випробували, а небезпечні помилки майже завжди є у випадках, яких ніхто не спробував.
Уявіть, що ви відповідаєте за будівлю з тисячею дверей і маєте гарантувати, що вночі кожні двері замкнені.
Різниця полягає між вибірковим дослідженням реальності та доведенням властивості конструкції. Тестування робить вибірку. Формальна верифікація доводить. У цьому вся ідея, а все інше — механізми для її суворого втілення.
Кожна формальна верифікація, якою б складною вона не була, будується рівно з трьох складників. Чітко зрозумійте їх — і все інше буде деталями.
| Опора | Просте значення | Аналогія з будівлею |
|---|---|---|
| Специфікація | Точне твердження того, що означає «правильно» | «Уночі всі двері мають бути замкнені» |
| Система | Фактична річ, яку перевіряють (програма, схема, протокол) | Будівля та її механізм замикання |
| Доказ | Суворий аргумент, що система завжди відповідає специфікації | Логічна демонстрація того, що натискання «замкнути» замикає всі двері |
А четвертий, менш помітний складник робить усе це надійним:
Серед асистентів доказів, назви яких ви можете почути, — Lean, Rocq (раніше Coq) та Isabelle. Фактично це надзвичайно суворі механізми перевірки логіки. Доказ Zcash з нашої вступної історії було написано в Lean. Примітно, що сучасні моделі AI дедалі частіше використовують для допомоги в написанні цих доказів під керівництвом людей, що скоротило роботу, яка колись займала роки, до кількох тижнів. Машина все одно перевіряє кожен крок, тож прискорення не зменшує певності.
Слово «доказ» може здаватися лячним, тож розвіємо цю таємничість конкретним прикладом, який можна перевірити. Жодної криптографії — лише шкільна арифметика.
Твердження: для кожного цілого невід'ємного числа 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), придатних для різних завдань; і написання цих доказів навіть за допомогою AI все ще потребує навичок і зусиль. Ми також не розглянули, як асистент доказів внутрішньо подає логіку. Ніщо з цього не змінює суті: специфікація, система та машинно-перевірений доказ того, що вони узгоджуються за вказаних припущень. Ми повернемося до деталей, коли вони знадобляться.
| Термін | Просте пояснення |
|---|---|
| Formal verification | Математичне доведення того, що система відповідає специфікації в усіх випадках |
| Specification | Точне твердження того, що означає «правильна поведінка» |
| System | Фактична програма, схема або протокол, що перевіряється |
| Proof | Скінченний ланцюг логічних кроків, що встановлює твердження для всіх випадків |
| Proof assistant / theorem prover | Програмне забезпечення (Lean, Rocq, Isabelle), що перевіряє кожен крок доказу |
| Machine-checked | Перевірений комп'ютером крок за кроком, а не лише прочитаний людиною |
| Induction | Метод доведення: істинно на початку, а кожен крок переносить це на наступний |
| Assumption | Умова, на яку спирається доказ; якщо вона хибна, гарантія може не виконуватися |
Чи замінює формальна верифікація тестування? Ні. Вони доповнюють одне одного. Тестування недорого виявляє практичні проблеми та хибні припущення; верифікація виключає цілі класи помилок, які тестування може ніколи не охопити.
Якщо вона така потужна, чому формально не верифікують усе? Вона дорога й потребує спеціалізованих навичок, хоча допомога AI знижує цю вартість. Її застосовують для систем, де рідкісна помилка була б катастрофічною, — саме там її вартість виправдовується.
Чи може формально верифікована система все одно відмовити? Так, якщо специфікація була неправильною, визначення було хибно сформульовано, припущення не виконалося або причина відмови лежить поза межами того, що було специфіковано. Доказ охоплює лише те, що він стверджує.
Чи машинно-перевірений доказ надійніший за людський? Для великих, складних доказів — загалом так. Машина не пропустить тонку прогалину й не прийме необґрунтоване твердження, хоча вона все одно довіряє наданим їй специфікації та визначенням.
Якщо AI допомагає писати доказ, чому йому довіряти? Тому що асистент доказів механічно перевіряє кожен крок. AI пропонує кроки, а машина їх перевіряє. Неправильний крок просто відхиляється, тож AI прискорює роботу, не послаблюючи гарантії.
Ви довели, що програмне забезпечення банку «ніколи не дозволяє балансу рахунку стати від'ємним». Через рік гроші все ще зникають. Як обидва твердження можуть бути правдивими водночас? (Відповідь нижче.)
Доказ гарантував рівно одну властивість: баланси ніколи не стають від'ємними. Гроші можуть зникати способами, яких ця властивість ніколи не охоплювала, наприклад через помилку, що переміщує кошти на неправильний (але все ще невід'ємний) рахунок, або через ваду в частині системи, яку ніколи не було специфіковано. Верифікація виконала рівно те, що обіцяла, і нічого більше. Це застереження з Розділу 6 у дії: доказ охоплює специфікацію, а не кожне можливе поняття «правильності».
Частина 2 · Помилка Orchard: ми докладно розглянемо справжню історію 2026 року. Система приватності приховувала суми за допомогою криптографічних доказів, а один недостатньо обмежений рядок у її математиці означав, що ці докази можна було змусити брехати, дозволяючи необмежену невидиму підробку. Ми точно побачимо, що означає «недостатньо обмежена схема», чому цей клас помилок може залишатися прихованим назавжди та чому це траплялося вже не раз.
Частина серії Formal Verification для ZecHub.