Формальная верификация

Формальная верификация может применяться для доказательства корректности таких систем, как криптографические протоколы, комбинационные схемы, цифровые устройства с внутренней памятью, а также программное обеспечение, представленное в виде исходного кода на одном из языков программирования. К известным примерам верифицированных программных систем относятся CompCert — проверенный компилятор языка C и микрокернель операционной системы высокого доверия seL4.

Верификация этих систем проводится путём доказательства существования формального доказательства математической модели исследуемого объекта^[3]. В качестве математических объектов для моделирования систем используются: конечные автоматы, отмеченные системы переходов, клаузулы Хорна, сети Петри, системы сложения векторов, тайм-автоматы, гибридные автоматы, алгебра процессов, формальные семантики языков программирования, такие как операционная семантика, денотационная семантика, аксиоматическая семантика и логика Хора^[4].

Модельное проверение заключается в систематическом и полном исследовании математической модели системы. Такой анализ возможен для конечных моделей, а также для некоторых видов бесконечных моделей, если удаётся эффективно задать бесконечные множества состояний путём абстрагирования или использования симметрии. Обычно процедура сводится к перебору всех состояний и переходов в модели, где для ускорения расчётов применяют специальные предметно-ориентированные методы абстрагирования, позволяющие рассматривать целые группы состояний единой операцией. К числу техник реализации относятся: перебор пространства состояний, символьный перебор пространства состояний, абстрактная интерпретация, символическое моделирование, уточнение абстракций. Свойства, подлежащие проверке, часто описываются при помощи темпоральных логик, например, линейная темпоральная логика (LTL), Property Specification Language (PSL), SystemVerilog Assertions (SVA)^[5], или компьютерная древовидная логика (CTL). Главным преимуществом модельного проверения считается высокая степень автоматизации; основной недостаток — трудности масштабирования на крупные системы: символьные модели обычно ограничиваются несколькими сотнями бит состояния, тогда как явный перебор требует сравнительно небольшого размера пространства состояний.

Другим подходом является дедуктивная верификация^[6][7]. Она включает в себя построение по системе и её спецификации (а иногда и по дополнительным аннотациям) набора математических «обязательств к доказательству» (proof obligations), истинность которых гарантирует соответствие системы спецификации, а затем — доказательство этих обязательств с помощью помощников доказательств (интерактивных проверяющих теорем), таких как HOL, ACL2, Isabelle, Rocq (ранее известный как Coq), PVS, либо при помощи автоматических доказателей теорем, в частности решателей задачи выполнимости по теориям (SMT). Недостатком этого способа является то, что от пользователя может потребоваться глубокое понимание причин корректности системы и уточнение этой информации для инструмента проверки — в виде последовательности теорем для доказательства или посредством формализации спецификаций (инвариантов, предусловий, постусловий) для компонентов и, возможно, их подкомпонентов.

Формальная верификация программ заключается в доказательстве того, что программа удовлетворяет формальной спецификации её поведения. К направлениям формальной верификации относятся дедуктивная верификация, абстрактная интерпретация, автоматическое доказательство теорем, типовые системы, а также облегчённые формальные методы. Одним из перспективных подходов, основанных на типах, выступает программирование с зависимыми типами, при котором типы функций (частично или полностью) включают формальные спецификации, а успешная проверка типов эквивалентна доказательству корректности реализованного кода относительно спецификаций. Полноценные языки с поддержкой зависимых типов позволяют воспринимать дедуктивную верификацию как частный случай проверки типов.

Другим дополнительным подходом является выведение программ, когда эффективный код строится по функциональной спецификации через последовательность преобразований, сохраняющих корректность. Примером такого подхода служит формализм Бёрд—Мертенс, рассматриваемый также как одна из форм синтеза программ.

Перечисленные методы могут быть «корректными», то есть гарантировать логическое следование свойств программы из её семантики, или «некорректными», когда такой гарантии нет. Корректная методика возвращает результат только после анализа всего пространства возможностей; пример некорректной — покрывающей лишь их подмножество, например, только целые числа в определённом диапазоне, чаще всего выносящей «достаточно хороший» ответ. Техники могут также быть «разрешимыми» — их алгоритмы гарантированно завершаются выдачей результата, или неразрешимыми, когда вычисления теоретически могут идти бесконечно. При ограничении области рассмотрения возможна реализация некорректной, но разрешимой методики, если корректная разрешимость недостижима.

Верификация — это одна из сторон процесса проверки пригодности продукта к использованию; валидация — её дополнение. Всё вместе этот процесс называют V & V (Verification and Validation).

• Валидация: «Правильный ли продукт мы пытаемся создать?» — то есть, соответствует ли продукт реальным потребностям пользователя?
• Верификация: «Создали ли мы то, что планировали?» — то есть, соответствует ли продукт заявленным спецификациям?

Верификация может включать как статические / структурные, так и динамические / поведенческие аспекты. Например, для ПО можно проанализировать исходный код (статический аспект) или выполнить тесты по определённым сценариям (динамический аспект). Валидация, напротив, обычно возможна только динамически, то есть путём проверки, как продукт ведёт себя при типичных и нетипичных вариантах использования («Полностью ли удовлетворяет известным сценариям?»).

Ремонт программ осуществляется относительно оракула, задающего желаемую функциональность программы, который используется для валидации исправления. Простейший пример — это тестовый набор: пары вход—выход определяют корректное поведение программы. На практике применяются различные методы, например, с использованием SMT-решателей (решателей задачи выполнимости по теориям) и генетическое программирование^[8], когда возможные варианты исправлений генерируются и оцениваются с помощью методов эволюционного вычисления. Первый метод — детерминированный, второй — вероятностный.

Ремонт программ сочетает методы формальной верификации с синтезом программ. Для определения потенциальных локаций ошибок применяются техники локализации дефектов, используемые в формальной верификации, на которые затем нацеливаются модули синтеза. Системы ремонта обычно концентрируются на узких классах типов ошибок с целью уменьшения области поиска вариантов исправлений. Применение в промышленности ограничено из-за высокой вычислительной стоимости существующих методов.

Рост сложности проектируемых систем делает формальные методы анализа всё более востребованными в аппаратной сфере^[9][10]. В настоящее время формальная верификация используется большинством ведущих производителей аппаратного обеспечения^[11], тогда как в разработке программного обеспечения распространение этих методов остаётся низким. Это объясняется большей востребованностью формальных методов именно в аппаратной сфере, где ошибки часто приводят к ощутимым экономическим потерям. Кроме того, из-за возможности сложных взаимодействий между компонентами становится всё труднее охватить все сценарии поведения исключительно методом симуляции, тогда как многие задачи аппаратного проектирования формализуемы и поддаются автоматическим доказательствам, благодаря чему внедрение формальной верификации для аппаратных решений проще и эффективнее^[12].

По состоянию на 2011 год были формально верифицированы несколько операционных систем: Secure Embedded L4 microkernel, созданный NICTA (и реализуемый коммерчески как seL4 компанией OK Labs)^[13], ОС реального времени ORIENTAIS, созданная на базе OSEK/VDX в Восточно-Китайском педагогическом университете, Integrity от Green Hills Software, а также PikeOS от SYSGO^[14].^[15] В 2016 году команда под руководством Чжуна Шао в Йельском университете разработала формально верифицированный микроядро CertiKOS^[16].^[17]

По состоянию на 2017 год формальная верификация применяется при проектировании масштабных компьютерных сетей на основе строгого математического моделирования^[18], а также в рамках нового класса технологий — сетей на основе намерений^[19]. Крупные разработчики сетевого ПО, предлагающие решения формальной верификации, включают Cisco^[20], Forward Networks^[21][22] и Veriflow Systems^[23].

Язык программирования SPARK содержит инструменты, позволяющие вести разработку с формальной верификацией, и используется в ряде ответственных промышленных систем.

Компилятор CompCert реализует большую часть стандарта ISO C и формально верифицирован как корректный^[24][25].