↶ Машина на глиняних ногах
14 / 18

Розділ 13. Математика в ядрі

Стара мрія

Уявімо, що ти написав програму. Як дізнатися, чи вона правильна?

Звичайний шлях — тестування. Запускаєш програму на сотнях прикладів. Якщо всі дають правильну відповідь — ти впевнений. Не на сто відсотків, але достатньо.

Проблема: тестування може показати наявність помилок, але не їх відсутність. Це знаменита фраза 1969 року Едгара Дейкстри, голландського комп’ютерного вченого і лауреата премії Тьюринга. Якщо програма приймає число від 1 до мільярда — ти не зможеш протестувати її на всіх можливих входах. Завжди залишається ймовірність, що десь у неперевіреному закутку є помилка.

А що, якби була інша можливість — математично довести, що твоя програма правильна? Не “ймовірно правильна”, а доведено, як теорема Піфагора?

Це — серце формальної верифікації. Стара мрія комп’ютерної науки, якій уже 60 років. Реалізована частково, недосконало, але реальна. І саме вона дає нам надію на майбутнє довірених систем — у тому числі для штучного інтелекту, про який буде розмова у двох наступних розділах.

Тоні Хоар і його прозріння

У 1969 році Тоні Хоар — англійський комп’ютерний учений, той самий, хто винайшов алгоритм QuickSort у 1959-му — опублікував статтю з академічно нудною назвою: “An Axiomatic Basis for Computer Programming”.

Ідея у статті була проста, але революційна. Хоар запропонував формальний спосіб міркувати про програми. Кожен крок програми можна записати як трійку:

{P} код {Q}

Де: - P — це передумова (precondition): що вірно перед виконанням коду. - Q — це постумова (postcondition): що вірно після. - код — те, що виконується.

Наприклад: {x = 5} x := x + 1 {x = 6} означає: якщо до початку x був 5, то після виконання x := x + 1 гарантовано x буде 6.

Це здається банальним. Але якщо так формалізувати кожен крок програми, можна шар за шаром доводити, що вся програма робить те, що задумано. Це називається логіка Хоара (Hoare logic), і вона лежить в основі сучасної формальної верифікації.

За цю роботу Хоар отримав премію Тьюринга у 1980 році. Але до 2000-х його ідея залишалась переважно академічною.

Чому це важко

Ти можеш запитати: якщо ідея проста, чому формальна верифікація не використовується скрізь?

Бо це дорого. Дуже дорого.

Уяви програму на тисячу рядків. Щоб формально довести її правильність, треба: 1. Написати специфікацію — формальний опис того, що програма має робити. Не словами (“повертає максимум”), а математичною мовою (forall i, list[i] <= result). 2. Написати доведення — послідовність кроків, які ведуть від специфікації до коду. Кожен крок має бути перевірений строго. 3. Перевірити це доведення в спеціальному інструменті (proof assistant) — типу Coq, Isabelle/HOL, Lean.

Для тисячі рядків коду доведення може займати сотні тисяч рядків. Співвідношення зазвичай 10:1 до 30:1. На один рядок коду — десять-тридцять рядків доведення.

І ці доведення треба писати руками. Вони не пишуться автоматично. Інструмент перевіряє, що твоє доведення коректне, але не вгадує його за тебе.

Це означає: - Програма на 10 тисяч рядків — місяці-роки роботи доказувача. - Програма на 100 тисяч — десятиліття. - Програма на мільйон — практично неможливо.

Звідси правило: формальна верифікація працює тільки для маленького критичного коду. Зокрема — для ядер ОС, шифрувальних бібліотек, авіоніки, медичного обладнання. Там, де ціна помилки — людські життя.

Інструменти

Є кілька основних інструментів формальної верифікації, з якими варто познайомитись.

Coq (1989, Франція). Один з найвідоміших і найстарших proof assistant. Розробляється у INRIA. Має дуже виразну систему типів (Calculus of Inductive Constructions). Використовується для: - Верифікації CompCert — оптимізаційного компілятора C, про який доведено, що він правильно компілює C-код. - Верифікації частини математики (теорема про чотири кольори, теорема Файта про прості скінченні групи). - Деяких частин Linux-ядра.

Isabelle/HOL (1989, Великобританія/Німеччина). Інший популярний proof assistant. Використовує higher-order logic (логіка вищого порядку — функції можуть приймати функції). На Isabelle написане доведення seL4 (про яке буде наступний розділ).

Lean (2013, Microsoft Research, Леонардо де Моура). Сучасний proof assistant з дружнішим синтаксисом. Lean 4 (2021) — це і мова програмування, і система доведень одночасно. Це найгарячіший проект у формальній верифікації зараз. У 2023-2024 роках з Lean 4 пов’язаний цілий бум — математики почали використовувати його для верифікації сучасних теорем (включно з роботами Філдсівського лауреата Теренса Тао), а DeepMind почала використовувати AI для автоматизації Lean-доведень.

TLA+ (1999, Леслі Лампорт). Не зовсім proof assistant, а специфікаційна мова. Використовується для опису і перевірки розподілених систем. Amazon застосовує TLA+ для критичних компонентів AWS (DynamoDB, S3) — і це врятувало їх від багатомільйонних інцидентів.

SPARK (Ada). Підмножина мови Ada з вбудованою верифікацією. Використовується в авіоніці (Airbus), залізниці, медицині.

Frama-C. Інструмент для верифікації C-коду. Використовується для перевірки критичних компонентів Linux-ядра, відкритих SSL-бібліотек.

Що означає “доведено правильно”

Тут важливий нюанс. Коли кажуть “програма формально верифікована” — це не означає, що вона взагалі без помилок. Це означає, що вона відповідає своїй специфікації.

Якщо специфікація неправильна — програма теж буде “неправильна” в інтуїтивному сенсі. Класичний приклад — у 1996 році ракета Ariane 5 вибухнула на 39-й секунді польоту. Причина: програмний модуль, який добре працював у попередній моделі (Ariane 4), помилився у нових умовах (Ariane 5 був потужнішим). Модуль формально не перевіряли проти специфікації Ariane 5 — а специфікація Ariane 4 була, для тієї ракети, правильною.

Тобто формальна верифікація не звільняє від обов’язку правильно сформулювати, що програма має робити. Це окрема, теж дуже важка робота.

Інший нюанс: верифікація доводить логічну правильність коду, але не апаратну. Якщо процесор має помилку (як Pentium FDIV bug 1994 року, який неправильно ділив певні числа), формально верифікований код на ньому буде давати неправильні результати. Тому повна верифікація потребує і верифікації заліза. Так роблять — але рідко.

І ще: компілятор. Ти написав код на C, формально довів його правильним — але компілятор може ввести помилки. Тому проект CompCert — оптимізаційний C-компілятор, правильність якого доведено в Coq, — і є таким важливим: він дозволяє довести, що твій формально перевірений вихідний код стає формально правильним машинним кодом.

Великі віхи

Подивимось на кілька проектів, де формальна верифікація працювала на повну.

CompCert (2009). Перший повністю формально верифікований оптимізуючий C-компілятор. Розробив Xavier Leroy у INRIA. Протягом 8 років. Використовується в авіоніці і атомних електростанціях.

seL4 (2009). Перше формально верифіковане мікроядро операційної системи (буде окремий розділ).

CertiKOS (2016). Маленьке мікроядро, верифіковане на Coq, з підтримкою concurrent execution.

HACL* (2016+). Криптографічна бібліотека Mozilla і Microsoft, формально верифікована. Використовується у Firefox і Linux-ядрі.

Project Everest (Microsoft + INRIA). Спроба верифікувати весь стек TLS — крипто, протокол, парсинг — щоб гарантувати безпеку HTTPS. Часткові результати вже у Windows.

EverParse. Формально верифіковані парсери (для протоколів). Розв’язує клас buffer overflow атак.

Amazon S3. Замість повної верифікації — TLA+ специфікації для critical paths. Знайшли і виправили глибокі баги, які пройшли всі тести.

Lean Mathlib. Найбільший репозиторій формалізованої математики у світі. До 2024 року — близько мільйона рядків доведень, від базової теорії множин до сучасних теорем.

AI вривається у верифікацію

Останні два-три роки — справжня революція у формальній верифікації, спричинена AI.

Раніше доведення треба було писати вручну, рядок за рядком. Найвужче місце — час кваліфікованого фахівця. Людей, які можуть писати доведення на Coq чи Lean, — у світі тисячі, не мільйони.

Тепер AI вже може писати значну частину доведень автоматично. Кілька знакових результатів:

DeepMind AlphaProof (2024). AI, який вирішує математичні задачі олімпіадного рівня. Використовує Lean 4 як мову. На Міжнародній математичній олімпіаді 2024 року AlphaProof набрав 28 з 42 балів — рівень срібної медалі.

OpenAI працює з Леонардо де Моурою і його командою над автоматизацією Lean-доведень. Деталі поки неоприлюднені, але уже видно прискорення.

Stanford-команда (Vincent Hellendoorn та ін.) показала, що сучасні LLM можуть генерувати валідні Coq-доведення для значної частини задач — без додаткового навчання.

Lean Copilot — інструмент, який пропонує наступний крок доведення в реальному часі (як GitHub Copilot, але для математики).

Це фундаментально змінює економіку формальної верифікації. Якщо раніше доведення на 1 рядок коду коштувало 10 рядків ручної роботи, то тепер може коштувати 1 рядок ручного підказування + AI-генерація. Це у 10-100 разів дешевше.

Прогноз: десь до 2030-го значна частина критичного коду буде формально верифікована, бо це стане економічно реальним. Це революція, яка проходить тихо, але матиме величезні наслідки.

Чи буде так у будь-якому коді

Скептики кажуть: формальна верифікація — це для критичного 1% програм. Решта 99% — веб-сайти, мобільні додатки, скрипти — ніколи не буде формально верифікованою. Зайве. Дорого. І вони праві… поки що.

Але є тенденція. Типи — це форма легкої верифікації. TypeScript додає типи до JavaScript, і це усуває цілий клас помилок. Rust додає систему власності, яка усуває помилки пам’яті. Кожна нова мова трохи більше схожа на формальну верифікацію.

Через 20 років, можливо, навіть звичайний веб-код матиме шар легкої верифікації. Не повне доведення, але підказки і перевірки, які гарантують відсутність деяких класів помилок.

Що зміниться, коли все стане доказувано

Уяви світ, де: - Кожне ядро ОС формально верифіковане. - Кожен критичний компонент мережі — теж. - Усі шифрувальні бібліотеки — гарантовано правильні. - Стек TLS, від firmware до браузера, доведено безпечний. - Драйвери для медичного, авіаційного, автомобільного обладнання — всі верифіковані.

У такому світі значна частина CVE просто перестає існувати. Атаки stack overflow — нема. Use-after-free — нема. Race conditions у критичному коді — нема.

Це не утопія. Це технічно можлива реальність 2040-х, якщо AI продовжує прискорювати верифікацію. Уряди вже готуються. CISA (Агентство кібербезпеки США) у 2023 році випустило гайд “Memory Safety Roadmap”, що рекомендує поступовий перехід на формально-безпечні мови для критичної інфраструктури. ЄС готує подібні рекомендації.

Але є умова: це працює тільки для маленького коду. Великі моноліти Linux чи Windows ніколи не будуть верифіковані повністю. Тому повертається тема Танненбаума з Розділу 11: щоб довірити автономному ШІ керувати ядерним реактором — потрібне маленьке верифіковане ядро, не великий моноліт.

І ось чому seL4 — наступний розділ — настільки важливе. Це не просто чергова ОС. Це єдине у світі ядро операційної системи, формально верифіковане від першого до останнього рядка. Те, чого Тоні Хоар у 1969-му навіть не міг мріяти. І ось, через 40 років після його теореми, у Сіднеї, Австралія, маленька команда дослідників зробила це насправді.

Що з цього винести

  1. Формальна верифікація — математичне доведення, що програма відповідає своїй специфікації.
  2. Ідея стара (Тоні Хоар, 1969), але стала практичною лише останні 15 років.
  3. Дорого: на один рядок коду — 10-30 рядків доведення. Тому застосовується тільки для маленького критичного коду.
  4. Основні інструменти: Coq, Isabelle/HOL, Lean, TLA+, SPARK, Frama-C.
  5. Великі досягнення: CompCert (компілятор C), seL4 (мікроядро), HACL* (криптографія), Amazon S3 (специфікації).
  6. AI прискорює верифікацію у 10-100 разів. До 2030-х це стане економічно реальним для широкого використання.
  7. У світі повної верифікації зникне цілий клас CVE-вразливостей. Це і є технічна основа для довіри автономним системам.

У наступному розділі — найважливіший приклад. seL4 — мікроядро, у якого кожен рядок коду має формальне доведення правильності. 10 тисяч рядків коду. Кілька сотень тисяч рядків доведення. Двадцять років роботи. І результат — єдине у світі ядро, якому реально можна довіряти.

Ходімо подивимось, як воно влаштоване.