Это обзорная статья, в которой очень поверхностно и не подробно рассказывается о том, что такое формальная верификация программного кода, зачем она нужна и чем она отличается от аудита и тестирования.
Формальная верификация — это доказательство с использованием математических методов корректности программного обеспечения.
Формальная верификация молода. На сегодняшний день, на сайте хабр, например, нет (пока) специализации «Формальная верификация», нет специальности «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 сейчас?
Комментарии (27)
tzlom
05.08.2023 11:08+3А есть формальное доказательство что программа на rust переписанная и верифицированная в coq является верифицированной и на rust ?
18741878
05.08.2023 11:08-1Всякий человек есть животное, но не всякое животное есть человек :) Так что вопрос остается открытым
vassabi
05.08.2023 11:081) я думаю что такое доказательство должно быть (но я не пишу на расте :) )
2) иногда код - 100% идеален. Но есть баги в компидяторе, в ОС, в железе. И если вдруг даже всё это работает идельно и безошибочно - иногда прилетают еще космические лучи %)
0xd34df00d
05.08.2023 11:08+3Нет и не может быть (внутри всяких coq, по крайней мере). То есть, вы можете построить модель раста и транслятора из [модели] раста в кок внутри кока и доказать что-то про эти модели, но вы не сможете никак доказать, что они соответствуют «настоящим» расту и транслятору.
rsashka
05.08.2023 11:08+1Разве можно доказать отсутствие?
А если в рамках данной статьи, то даже железное доказательство правильности кода может разбиться об обычный аппаратный сбой в ячейке памяти.0xd34df00d
05.08.2023 11:08+5Разве можно доказать отсутствие?
Да. Это просто функция из типа, соответствующего несуществующему объекту, в боттом.
А если в рамках данной статьи, то даже железное доказательство правильности кода может разбиться об обычный аппаратный сбой в ячейке памяти.
Более того, железное доказательство основано на вере в консистентность ZF[C].
Смысл всех этих упражнений в том, чтобы максимально уменьшить поверхность вещей, которым нужно доверять.
rsashka
05.08.2023 11:08Да. Это просто функция из типа, соответствующего несуществующему объекту, в боттом.
Вы немного лукавите
А вот средствами формальной верификации как раз можно доказывать отсутствие конкретных видов ошибок в коде (ниже мы приведем пример)
Поэтому правильнее будет написать, что:
Формальная верификация — это доказательство с использованием математических методовкорректностиотсутствия конкретных видов ошибок в программном обеспечении.0xd34df00d
05.08.2023 11:08Вы немного лукавите
Почему?
Поэтому правильнее будет написать, что
Важно помнить, что не существует средств, дающих больше гарантий.
rsashka
05.08.2023 11:08Почему?
корректность ПО != отсутствию конкретных видов ошибок
Важно помнить, что не существует средств, дающих больше гарантий.
Статистика (например, результатов тестирования) может дать хоть и не больший, но зато более точный ответ. Причем, с учетом надежности используемого оборудования.
Сразу скажу, что я написал это не для того, чтобы сказать, что формальная верификация ПО не нужна. Нет, конечно нужна! Но это вовсе не панацея от наличия ошибок программах, как бы не хотелось это представить, а всего лишь один из инструментов повышения качества программного кода и не более.
0xd34df00d
05.08.2023 11:08+1корректность ПО != отсутствию конкретных видов ошибок
А, я вас не так понял изначально. Впрочем, этот тезис зависит от вашего определения корректности.
Статистика (например, результатов тестирования) может дать хоть и не больший, но зато более точный ответ.
А как же частицы? :]
Формально вы можете построить модель с резервированием и потом реализовать её в железе, раз подобные события вам важны.
andreykl
05.08.2023 11:08+1Доказать отсутствие вполне можно. Например, ознакомившись со школьным курсом геометрии, в общем-то по моему вполне можно доказать что нет треугольников с суммой углов больше 180 градусов.
Ну и да, вполне можно доказывать отсутствие ошибок в программах, чем инженеры по формальной верификации и занимаются :).
ImagineTables
05.08.2023 11:08+5Объясните, пожалуйста, как формальная верификация (ФВ) сочетается с проблемой остановки. Если в общем случае нельзя даже доказать, что программа не зависнет, то как ФВ вообще работает? Все наши программы принадлежат к какому-то отдельном узкому классу, или что? Спасибо.
DirectoriX
05.08.2023 11:08Скорее, ФВ не имеет одного универсального алгоритма для проверки любой программы, это лишь набор методов/приёмов/техник, которые применяются в каждом случае по-своему. А в частных случаях и проблема останова разрешима.
Aleshonne
05.08.2023 11:08Проблема останова — это как вероятность умереть от прямого попадания метеорита, которая не равна нулю, но настолько мала, что ею все пренебрегают. Есть очень узкий класс программ, для которых невозможно определить, завершатся ли они когда-нибудь, который и не позволяет решить проблему останова в общем виде, и широкий класс программ, для которых всё ясно. Я совершенно не удивлюсь, если абсолютно все программы, для которых проблема останова неразрешима, специально созданы именно с целью показать неразрешимость этой проблемы, а не получены в результате решения какой-либо практической задачи.
Системы формальной верификации используют предположение о том, что программа должна за конечный промежуток времени решать поставленную пред ней задачу и люди не пытаются верифицировать то, что верифицировать невозможно в принципе. В этом предположении можно смело заменять утверждение «функция либо выдаст верный результат, либо никогда не завершит свою работу» на утверждение «функция выдаст верный результат».
0xd34df00d
05.08.2023 11:08+2Конечно нет, системы формальной верификации (по крайней мере те, о которых пишет ОП, и сходные) не имеют такого предположения. На самом деле получить незавершимые вычисления в доказательствах очень легко и ненароком, и лемовские сепульки тому отличный пример.
Aleshonne
05.08.2023 11:08Я, конечно, не специалист по теории вычислений и могу ошибаться, но мне кажется, что проблема останова — это не про незавершимые вычисления, а про вычисления, про которые невозможно сказать, завершимы они или нет. Для сепулек незавершимость легко доказать, там состояние повторяется спустя несколько итераций. Хорошим примером проблемы останова мне видится программа, которая в десятичном представлении числа √2 (или ещё какой-нибудь непериодической бесконечной дроби) ищет последовательность цифр, переданную на вход, и возвращает её позицию.
0xd34df00d
05.08.2023 11:08Я говорил о том, что легко получить незавершимые вычисления и на практике, поэтому уметь их определять и отбрасывать очень полезно. И когда у вас какая-нибудь хитрая взаимная индукция по чему-то сложнее, чем натуральные числа, то (не)завершимость становится не столь очевидной.
vkni
05.08.2023 11:08Объясните, пожалуйста, как формальная верификация (ФВ) сочетается с проблемой остановки.
Пытаемся доказать, что подпрограмма принадлежит к узкому классу. Иногда доказательство не удаётся, иногда это можно исправить подправив подпрограмму.
Если в общем случае нельзя даже доказать, что программа не зависнет, то как ФВ вообще работает?
Более того, есть очень известный класс программ, которые по ТЗ могут выполняться бесконечно долго — диалоговые программы для взаимодействия с пользователем (MS Word, к примеру).
0xd34df00d
05.08.2023 11:08+2Да. Все программы, которые типизируемы в коке/агде/идрисе, заведомо останавливаются (или, учитывая коданные, производят следующий юнит работы за конечное время), поэтому эти языки не тьюринг-полны (что, конечно, можно отключить, но тогда вы ничего не доказали).
Termination checker тупой и не может проверить любую наперёд заданную функцию на предмет того, что она останавливается, без false negative'ов (зато у него нет false positive'ов!), но это обходится финтами вроде таких.
Natasha_Klaus Автор
05.08.2023 11:08+1Спасибо за вопрос.
Проверка завершаемости в Coq консервативна. Это означает, что Coq
принимает только функции определенного вида, про которые он точно может
сказать, что эта функция завершается. Речь идет о рекурсивных функциях (Fixpoint). Остальные функции не проходят проверку завершаемости, даже если такая функция на самом деле завершается. Но для функций Fixpoint, Coq требует, чтобы рекурсивные вызовы осуществлялись только на параметрах, которые синтаксически уменьшаются на каждом шаге итерации. Такой парамер Coq как правило может найти сам, его можно также явно указать.Проверку завершаемости в Coq над функцией можно отключить (установить над ней флажок
#[bypass_check(guard)])Я писала о проблеме остановки в этой статье.
Natasha_Klaus Автор
05.08.2023 11:08Я писала о проблеме остановки: https://habr.com/ru/articles/749662/
Можно доказать, что программа не зависнет.
Но универсального алгоритма не существует.
andreykl
05.08.2023 11:08+1Я, пожалуй, дополню ответы выше.
Программы не принадлежат к отдельному узкому классу.
Проблему останова действительно нельзя решить (по крайней мере на устройстве "одного ранга" что ли.. про гипотетические устройства более других "рангов" можно глянуть википедию).
Однако её нельзя решить в общем случае. Для каждого конкретного частного случая её можно попытаться решить. Построенное решение (если удалось его построить, конечно) и есть доказательство завершаемости алгоритма. Те математики которые анализируют алгоритмы, время от времени развлекаются решением проблемы останова (каждый раз в частном случае разумеется). Этим же занимаются и инженеры по формальной верификации.
Чуть более подробно, ситуация такая: для части случаев Coq (и другие подобные системы) может автоматически решать проблему останова. Конкретно Coq определяет что рекурсивный вызов рассматриваемой функции происходит на структурно меньшем аргументе. И если это так, то это значит что алгоритм завершится (поскольку так определяются индуктивные типы в Coq). Но это работает только для примитивно-рекурсивных функций. В общем случае приходится формулировать и доказывать утверждения о завершаемости руками.
Один из подходов к доказательству завершаемости общерекурсивных функций средствами Coq описан у автора в одной из публикаций.
ivanrt
05.08.2023 11:08+2Формально верефицированную программу нужно компилировать формально проверенным компилятором, который скомпилирован формально проверенным компилятором...? Ещё нужно процессор небось формально verified и операционную систему при её наличии.
Ну или всё зависит от задачи?
Natasha_Klaus Автор
05.08.2023 11:08+1На практике многие утверждения приходится аксиоматизировать. Что-то остается недоказанным. Что-то приходится допускать. Все те ссылки, что приведены в статье о текущих разработках в сфере ФВ, это исследовательские работы на базе университетов. Компилятор С (проект CompCert) верифицирован не полностью (верифицированы его основные части). Хота, на данный момент, возможно (не уверена), они уже завершили эту работу, и верифицировали оставшиеся блоки.
shuhray
05.08.2023 11:08Я довольно много пробовал всего и моё мнение - пока хорошего пруфчекера нет. И перспективней всех Metamath, если бы там удалось решить проблемы с подстановкой (в Metamath есть только простая подстановка, не заботящаяся о переименовании связанных переменных в случае коллизий, поэтому формализовать логику с кванторами или лямбда-исчисление приходится крайне нестандартными способами). Проблемы эти математические, не программистские.
18741878
Э.Дейкстра "Дисциплина программирования": основополагающая работа.
Д.Грис "Наука программирования": в сущности, пересказ книги Дейкстра, но на более формальном языке.
Обе книги достаточно "древние", что, однако, не умаляет их ценности и интересности. Главный посыл: прежде чем тыкать в клавиатуру пальчиками, пытаясь соорудить нечто более-менее работающее, лучше, пользуясь аппаратом математической логики, вывести алгоритм, гарантированно соответствующий тому, что от него ожидается. Обе книги просто великолепны. Первая - больше философская, вторая - больше техническая. Ищутся легко. Читаются отнюдь не просто