В контексте аппаратных и программных систем формальная верификация — это процесс доказательства или опровержения правильности системы по отношению к определенной формальной спецификации или свойству с использованием формальных математических методов . [1] Формальная верификация является ключевым стимулом для формальной спецификации систем и лежит в основе формальных методов . Он представляет собой важный аспект анализа и проверки в автоматизации проектирования электроники и является одним из подходов к проверке программного обеспечения . Использование формальной проверки обеспечивает самый высокий уровень гарантии оценки ( EAL7 ) в рамках общих критериев сертификации компьютерной безопасности .
Формальная проверка может быть полезна для доказательства правильности таких систем, как: криптографические протоколы , комбинационные схемы , цифровые схемы с внутренней памятью и программное обеспечение, выраженное в виде исходного кода на языке программирования . Яркими примерами проверенных программных систем являются проверенный CompCert компилятор C и высоконадежное ядро операционной системы seL4 .
Проверка этих систем осуществляется путем обеспечения существования формального доказательства математической модели системы. [2] Примерами математических объектов, используемых для моделирования систем, являются: конечные автоматы , системы помеченных переходов , предложения Хорна , сети Петри , системы векторного сложения , временные автоматы , гибридные автоматы , алгебра процессов , формальная семантика языков программирования, такая как операционная семантика. , денотационная семантика , аксиоматическая семантика и логика Хоара . [3]
Одним из подходов и форм является проверка модели , которая состоит из систематического исчерпывающего исследования математической модели (это возможно для конечных моделей , но также и для некоторых бесконечных моделей, где бесконечные наборы состояний могут быть эффективно представлены конечным образом, используя абстракцию или используя преимущества симметрия). Обычно это заключается в исследовании всех состояний и переходов в модели с использованием интеллектуальных и специфичных для предметной области методов абстракции для рассмотрения целых групп состояний за одну операцию и сокращения времени вычислений. Методы реализации включают перечисление пространства состояний , символическое перечисление пространства состояний, абстрактную интерпретацию , символическое моделирование , уточнение абстракции. [ нужна цитация ] Свойства, подлежащие проверке, часто описываются в темпоральной логике , такой как линейная темпоральная логика (LTL), язык спецификации свойств (PSL), утверждения SystemVerilog (SVA), [4] или вычислительная древовидная логика (CTL). Большим преимуществом проверки моделей является то, что она часто происходит полностью автоматически; его основной недостаток заключается в том, что он обычно не масштабируется для больших систем; символьные модели обычно ограничены несколькими сотнями битов состояния, в то время как явное перечисление состояний требует, чтобы исследуемое пространство состояний было относительно небольшим.
Другой подход – дедуктивная проверка. Он состоит из создания на основе системы и ее спецификаций (и, возможно, других аннотаций) набора математических обязательств доказательства , истинность которых подразумевает соответствие системы ее спецификации, и выполнения этих обязательств с использованием либо помощников по доказательству (интерактивных средств доказательства теорем) ( такие как HOL , ACL2 , Isabelle , Coq или PVS ) или автоматические средства доказательства теорем , включая, в частности, решатели теорий выполнимости по модулю (SMT). Этот подход имеет тот недостаток, что может потребовать от пользователя подробного понимания того, почему система работает правильно, и передачи этой информации в систему проверки либо в виде последовательности теорем, которые необходимо доказать, либо в виде спецификаций ( инварианты, предусловия, постусловия) компонентов системы (например, функций или процедур) и, возможно, подкомпонентов (таких как циклы или структуры данных).
Формальная верификация программ предполагает доказательство того, что программа удовлетворяет формальной спецификации своего поведения. Подобласти формальной проверки включают дедуктивную проверку (см. выше), абстрактную интерпретацию , автоматическое доказательство теорем , системы типов и облегченные формальные методы . Многообещающим подходом к проверке на основе типов является зависимо типизированное программирование , в котором типы функций включают (по крайней мере часть) спецификации этих функций, а проверка типов кода устанавливает его корректность по этим спецификациям. Полнофункциональные языки с зависимой типизацией поддерживают дедуктивную проверку как особый случай.
Другой дополнительный подход — это создание программ , при котором эффективный код создается на основе функциональных спецификаций с помощью ряда шагов, сохраняющих корректность. Примером такого подхода является формализм Берда-Меертенса , и этот подход можно рассматривать как еще одну форму корректности по построению.
Эти методы могут быть надежными , что означает, что проверенные свойства могут быть логически выведены из семантики, или ненадежными , что означает, что такой гарантии нет. Грамотная техника дает результат только тогда, когда она охватывает все пространство возможностей. Примером ненадежного метода является тот, который охватывает только подмножество возможностей, например, только целые числа до определенного числа, и дает «достаточно хороший» результат. Методы также могут быть разрешимыми , что означает, что их алгоритмические реализации гарантированно завершатся с ответом, или неразрешимыми, что означает, что они могут никогда не завершиться. Ограничивая объем возможностей, можно создать необоснованные методы, которые разрешимы, когда нет доступных разрешимых надежных методов.
Проверка — это один из аспектов проверки соответствия продукта назначению. Валидация является дополнительным аспектом. Часто общий процесс проверки называют V&V.
Процесс проверки состоит из статического/структурного и динамического/поведенческого аспектов. Например, для программного продукта можно проверить исходный код (статический) и выполнить определенные тестовые сценарии (динамический). Проверка обычно может выполняться только динамически, т. е. продукт тестируется путем его типичного и нетипичного использования («Отвечает ли он всем сценариям использования ?»).
Восстановление программы выполняется в отношении оракула , охватывая желаемую функциональность программы, которая используется для проверки сгенерированного исправления. Простым примером является набор тестов: пары ввода/вывода определяют функциональность программы. Используются различные методы, в первую очередь использование решателей теории выполнимости по модулю (SMT) и генетическое программирование [5] с использованием эволюционных вычислений для генерации и оценки возможных кандидатов на исправления. Первый метод является детерминированным, а второй – рандомизированным.
Восстановление программ сочетает в себе методы формальной проверки и синтеза программ . Методы локализации ошибок при формальной верификации используются для вычисления точек программы, которые могут быть возможными местами ошибок, на которые могут быть направлены модули синтеза. Системы восстановления часто фокусируются на небольшом заранее определенном классе ошибок, чтобы сократить пространство поиска. Промышленное использование ограничено из-за вычислительной стоимости существующих методов.
Рост сложности проектов увеличивает важность формальных методов проверки в аппаратной промышленности. [6] [7] В настоящее время формальная верификация используется большинством или всеми ведущими производителями оборудования, [8] но ее использование в индустрии программного обеспечения все еще томится. [ нужна цитата ] Это можно объяснить большей потребностью в аппаратной промышленности, где ошибки имеют большее коммерческое значение. [ нужна цитата ] Из-за потенциальных тонких взаимодействий между компонентами становится все труднее реализовать реалистичный набор возможностей путем моделирования. Важные аспекты проектирования аппаратного обеспечения поддаются автоматизированным методам проверки, что упрощает внедрение формальной проверки и делает ее более продуктивной. [9]
По состоянию на 2011 год [обновлять]официально проверено несколько операционных систем: микроядро Secure Embedded L4 компании NICTA, продаваемое OK Labs на коммерческой основе как seL4 ; [10] Операционная система реального времени ORIENTAIS на базе OSEK/VDX, разработанная Восточно-Китайским педагогическим университетом ; [ нужна ссылка ] Операционная система Integrity компании Green Hills Software ; [ нужна ссылка ] и PikeOS от SYSGO . [11] [12] В 2016 году команда под руководством Чжун Шао из Йельского университета разработала официально проверенное ядро операционной системы под названием CertiKOS. [13] [14]
С 2017 года формальная проверка стала применяться к проектированию больших компьютерных сетей с помощью математической модели сети [15] и как часть новой категории сетевых технологий — сетей на основе намерений. [16] Поставщики сетевого программного обеспечения, предлагающие формальные решения для проверки, включают Cisco [17] Forward Networks [18] [19] и Veriflow Systems. [20]
Язык программирования SPARK предоставляет набор инструментов, который позволяет разрабатывать программное обеспечение с формальной проверкой и используется в нескольких системах с высокой степенью интеграции . [ нужна цитата ]
Компилятор C CompCert является формально проверенным компилятором C, реализующим большую часть ISO C. [21] [22]
