Это обзорная статья, в которой очень поверхностно и не подробно рассказывается о том, что такое формальная верификация программного кода, зачем она нужна и чем она отличается от аудита и тестирования.
Формальная верификация — это доказательство с использованием математических методов корректности программного обеспечения.
Формальная верификация молода. На сегодняшний день, на сайте хабр, например, нет (пока) специализации «Формальная верификация», нет специальности «Proof инженер» или «Специалист по формальной верификации». А люди, работающие по этой специальности — есть.
Программное обеспечение, которое прошло формальную верификацию считается надежным. Формальная верификация дает (с математической точностью) гарантии того, что программный код не будет содержать конкретных ошибок, что функции будут вести себя так, как ожидается.
В основе формальной верификации лежат математические методы. Слово «формальный» в названии - это отсылка к математике. Для доказательства утверждений о программном коде используются формальные методы математики: математическая логика, лямбда исчисление, теория категорий, математический анализ, алгоритмы для работы с функциональными и императивными структурами данных.
Инструменты для верификации — это программные средства для доказательства теорем (Coq, Isabelle ...), а также SAT-solvers.
В 70х годах предки формальной верификации — это доказательства простых утверждений о программе (конкретной функции) с помощью ручки и листка бумаги. Сегодня — это (иногда многолетние) исследовательские проекты для конкретного программного обеспечения, вот некоторые из них:
CompCert - верифицирован компилятор С
Project Everest — формальная верификация HTTPS. Включает формальную верификацию протокола TLS и лежащих в его основе криптографических алгоритмов
sel4 — формальная верификация микроядра OS
доказательство теоремы о четырех красках, проверенное с помощью компьютера формально
автоматический переводчик кода Ocaml на Coq для последующей формальной верификации
автоматический переводчик кода Rust на Coq для последующей формальной верификации
автоматический переводчик кода Solidity на Coq (для верификации смарт-контрактов, написанных на Solidity, работа над ним идет)
перевод кода Rust на Isabelle (правда, вся документация на китайском)
... и много, много других интересных проектов
Во многих технических университетах мира сегодня появляется все больше и больше курсов, посвященных формальной верификации.
В первую очередь формальная верификация важна для цифровых аппаратных систем и программного обеспечения, где безопасность превыше всего и ошибка в программном коде может стоить очень дорого: космическая отрасль, автономный транспорт, банковские системы, криптовалюты, и т. д.
Подходов к валидации программного обеспечения (позволяющих убедиться, что программа ведет себя так, как ожидается) много. Помимо формальной верификации об отсутствии уязвимостей и багов в исходном коде пекутся, например, еще такие отрасли как тестирование и аудит.
Тестирование и аудит
Тестирование программного кода — это целая наука со множеством подходов и практик. Современные языки программирования включают в себя поддержку для разработки автоматизированных тестов для программ, а также поддержку модульных и интеграционных тестов.
Но еще в далеком 1972 году в своем эссе “The Humble Programmer,” Эдсгер Дейкстра писал:
“Тестирование программ может быть очень эффективным средством, выявляющем наличие ошибок в коде, но оно безнадежно и неадекватно в доказательстве их отсутствия”.
А вот средствами формальной верификации как раз можно доказывать отсутствие конкретных видов ошибок в коде (ниже мы приведем пример)
То же можно сказать и об аудите кода. Разные организации имеют собственные подходы к аудиту, в основном это:
построчный ручной разбор исходного кода на предмет распространенных уязвимостей, повторяемости блоков кода, качество архитектуры кода, рекомендации к использованию лучших практик
документация кода: проверка на качество и достаточность документации
использование автоматических средств аудита. Например, для языка программирования Rust, к автоматическим средствам аудита можно отнести:
Cargo audit (проверяет Cargo.lock файлы на зависимости от crates, содержащих уязвимости)
Cargo Clippy (выявление типичных ошибок, улучшение кода)
Cargo Upgrades (работа с зависимостями, выявление устаревших зависимостей, которые могут быть причиной уязвимости)
и другие...
Но и аудит сто процентной гарантии отсутствия ошибок дать не может.
Формальная верификация
Теперь о формальной верификации. Положим, наша задача подвергнуть формальной верификации некий программный код. Опишем один из возможных способов (сценариев) работы.
На первом шаге мы переводим этот код (каждую строчку верифицируемого кода) на язык интерактивного программного средства доказательства теорем, например Coq или Isabelle (их еще называют «пруверы», от слова «proof» и, как правило, они используют собственные языки программирования). Ссылки на автоматические переводчики с языка на прувер приведены в статье выше.
Далее, для каждой функции нужно написать несколько Лемм (Теорем) и доказать их в прувере. Эти леммы должны отражать суть функции, описывать ее поведение и доказывать, что она ведет себя так как ожидается для всех возможных входных параметров. А если мы не сможем что-то доказать — вероятно, мы нашли баг, ошибку, уязвимость, нужно смотреть в какой точке, с какими значениями параметров, функция начинает вести себя не так как ожидается и сообщать о найденном баге программистам в отчете.
Практика. Что доказывать?
Что функция никогда не вернет определенного вида ошибку. Для всех возможных входных параметров. Приведем дистиллированный пример.
Пусть в исходном коде есть типы ошибок:
Inductive Error_types : Type :=| Error_1| Error_2| Error_3.И есть функция, которую мы верифицируем (уже переведена на Coq)
Definition run (i : nat) : option Error_types :=match i with| O => None| S n => Some Error_1end.Сформулируем простую лемму о поведении нашей функции, и докажем ее. Будем доказывать, что для всех возможных n (а этот параметр в функции - натуральное число), наша функция не вернет результата равного (Some Error_2). Докажем, что для всей бесконечности натуральных чисел это так.
Lemma function_run_will_never_return_Some_error_2 : forall n, run n <> Some Error_2.Proof.intros.destruct n.{ (* n = 0 *)simpl.unfold "<>".intros.(* H : Some Error_1 = Some Error_2 - а это невозможно, это два разных конструктора *)inversion H.}{ (* n = S n *)simpl.unfold "<>".intros.inversion H.}Qed.Доказано, для всей бесконечности натуральных n. Нам даже не пришлось использовать математическую индукцию , потому как наша дистиллированная, приведенная только для примера, функция, проста как топор.
Что функция всегда будет возвращать конкретного вида результат (для всех возможных входящий значений).
Верифицировать совместимость функций. Например, есть функция, которая парсит некоторое значение, а есть обратная ей, так вот, значение, пропущенное через эти две взаимно-обратные операции не должно измениться.
Лемма будет выглядеть так:
Для всех n, unparse(parse n) = n.Что функция (если она рекурсивна) завершится (а не зависнет) для всех возможных входных параметров. Подробнее один из приемов мы разбирали в этой статье
И подобных лемм, про каждую функцию несколько, они должны описывать ее поведение, и доказывать, что она ведет себя как ожидается, возвращает, что от нее ждут. Надо сказать, что на практике функции, как правило, не просты. Они могут содержать сотни и даже тысячи строк кода, а их верификация, соответственно — много больше. То есть пруф-инженер должен не только владеть инструментами формальной верификации, но и неплохо знать язык, на котором написан верифицируемый код.
Если во время верификации мы видим, что что-то доказать не удается, пруф-инженер пишет предикаты валидности над каждой функцией и включает их в отчет для программистов. То есть, например, мы доказали, что для всех integer (n > 0) функция ведет себя правильно, как ожидалось. А если n <= 0 — функция возвращает неожиданные результаты.
Cовместимость версий кода, когда выходят новые версии.
... многое другое
Помимо описанного сценария, есть еще другие, где в основе работы лежат SAT-солверы (задача выполнимости булевых формул).
Ну вот мы и ковырнули вершину айсберга.
Заключение
Безопасность и надежность программного обеспечения - очень актуальный вопрос (статья о роковых ошибках в сфере IT, украдены миллионы: криптовалюты). Ни один из существующих на сегодняшний день подходов не может дать сто процентной гарантии полного отсутствия ошибок и уязвимостей в коде. Для обеспечения максимальной безопасности программного кода лучше всего использовать все доступные средства и формальная верификация — один из самых мощных, активно развивающихся и многообещающих подходов на сегодняшний день.
Про формальную верификацию злые, скептически настроенные языки говорят: это слишком дорого! Это слишком долго! Слишком сложно! Но ведь совсем недавно так говорили и про машинное обучение, а посмотрите-ка где GPT сейчас?
