Формальная проверка
В контексте аппаратных и программных систем — формальная верификация это процесс доказательства или опровержения правильности системы по отношению к определенной формальной спецификации или свойству с использованием формальных математических методов . [1] Формальная верификация является ключевым стимулом для формальной спецификации систем и лежит в основе формальных методов . Он представляет собой важный аспект анализа и проверки в автоматизации проектирования электроники и является одним из подходов к проверке программного обеспечения . Использование формальной проверки обеспечивает самый высокий уровень гарантии оценки ( EAL7 ) в рамках общих критериев сертификации компьютерной безопасности .
Формальная проверка может быть полезна для доказательства правильности таких систем, как: криптографические протоколы , комбинационные схемы , цифровые схемы с внутренней памятью и программное обеспечение, выраженное в виде исходного кода на языке программирования . Яркими примерами проверенных программных систем являются CompCert проверенный C компилятор и seL4 высоконадежное ядро операционной системы .
Проверка этих систем осуществляется путем обеспечения существования формального доказательства математической модели системы. [2] Примерами математических объектов, используемых для моделирования систем, являются: конечные автоматы , системы помеченных переходов , предложения Хорна , сети Петри , системы сложения векторов , временные автоматы , гибридные автоматы , алгебра процессов , формальная семантика языков программирования, такая как операционная семантика , денотационная семантика. , аксиоматическая семантика и логика Хоара . [3]
Подходы [ править ]
Одним из подходов и форм является проверка модели , которая состоит из систематического исчерпывающего исследования математической модели (это возможно для конечных моделей , но также и для некоторых бесконечных моделей, где бесконечные наборы состояний могут быть эффективно представлены конечным образом, используя абстракцию или используя преимущества симметрия). Обычно это заключается в исследовании всех состояний и переходов в модели с использованием интеллектуальных и специфичных для предметной области методов абстракции для рассмотрения целых групп состояний за одну операцию и сокращения времени вычислений. Методы реализации включают перечисление пространства состояний , символическое перечисление пространства состояний, абстрактную интерпретацию , символическое моделирование , уточнение абстракции. [ нужна цитата ] Свойства, подлежащие проверке, часто описываются в темпоральной логике , такой как линейная темпоральная логика (LTL), язык спецификации свойств (PSL), утверждения SystemVerilog (SVA), [4] или вычислительная древовидная логика (CTL). Большим преимуществом проверки моделей является то, что она часто происходит полностью автоматически; его основной недостаток заключается в том, что он обычно не масштабируется для больших систем; символьные модели обычно ограничены несколькими сотнями битов состояния, в то время как явное перечисление состояний требует, чтобы исследуемое пространство состояний было относительно небольшим.
Другой подход – дедуктивная проверка. Он состоит из создания на основе системы и ее спецификаций (и, возможно, других аннотаций) набора математических обязательств доказательства , истинность которых подразумевает соответствие системы ее спецификации, и выполнения этих обязательств с использованием либо помощников по доказательству (интерактивных средств доказательства теорем) ( такие как HOL , ACL2 , Isabelle , Coq или PVS ) или автоматические средства доказательства теорем , включая, в частности, решатели теорий выполнимости по модулю (SMT). Этот подход имеет тот недостаток, что может потребовать от пользователя подробного понимания того, почему система работает правильно, и передачи этой информации в систему проверки либо в виде последовательности теорем, которые необходимо доказать, либо в виде спецификаций ( инварианты, предусловия, постусловия) компонентов системы (например, функций или процедур) и, возможно, подкомпонентов (таких как циклы или структуры данных).
Программное обеспечение [ править ]
Формальная верификация программ предполагает доказательство того, что программа удовлетворяет формальной спецификации своего поведения. Подобласти формальной проверки включают дедуктивную проверку (см. выше), абстрактную интерпретацию , автоматическое доказательство теорем , системы типов и облегченные формальные методы . Многообещающим подходом к проверке на основе типов является зависимо типизированное программирование , в котором типы функций включают (по крайней мере часть) спецификации этих функций, а проверка типов кода устанавливает его корректность по этим спецификациям. Полнофункциональные языки с зависимой типизацией поддерживают дедуктивную проверку как особый случай.
Другой дополнительный подход — это создание программ , при котором эффективный код создается на основе функциональных спецификаций с помощью ряда шагов, сохраняющих корректность. Примером такого подхода является формализм Берда-Меертенса , и этот подход можно рассматривать как еще одну форму корректности по построению .
Эти методы могут быть надежными , что означает, что проверенные свойства могут быть логически выведены из семантики, или ненадежными , что означает, что такой гарантии нет. Грамотная техника дает результат только тогда, когда она охватывает все пространство возможностей. Примером ненадежного метода является тот, который охватывает только подмножество возможностей, например, только целые числа до определенного числа, и дает «достаточно хороший» результат. Методы также могут быть разрешимыми , что означает, что их алгоритмические реализации гарантированно завершатся с ответом, или неразрешимыми, что означает, что они могут никогда не завершиться. Ограничивая объем возможностей, можно создать необоснованные методы, которые разрешимы, когда нет доступных разрешимых надежных методов.
Проверка и валидация [ править ]
Проверка — это один из аспектов проверки соответствия продукта назначению. Валидация является дополнительным аспектом. Часто общий процесс проверки называют V&V.
- Проверка : «Пытаемся ли мы сделать правильно?», т. е. соответствует ли продукт реальным потребностям пользователя?
- Проверка : «Сделали ли мы то, что пытались сделать?», т. е. соответствует ли продукт спецификациям?
Процесс проверки состоит из статического/структурного и динамического/поведенческого аспектов. Например, для программного продукта можно проверить исходный код (статический) и выполнить определенные тестовые сценарии (динамический). Проверка обычно может выполняться только динамически, т. е. продукт тестируется путем его типичного и нетипичного использования («Отвечает ли он всем сценариям использования ?»).
Автоматизированное восстановление программы [ править ]
Восстановление программы выполняется в отношении оракула , охватывая желаемую функциональность программы, которая используется для проверки сгенерированного исправления. Простым примером является набор тестов: пары ввода/вывода определяют функциональность программы. Используются различные методы, в первую очередь использование решателей теории выполнимости по модулю (SMT) и генетического программирования . [5] использование эволюционных вычислений для генерации и оценки возможных кандидатов на исправления. Первый метод является детерминированным, а второй – рандомизированным.
Восстановление программ сочетает в себе методы формальной проверки и синтеза программ . Методы локализации ошибок при формальной верификации используются для вычисления точек программы, которые могут быть возможными местами ошибок, на которые могут быть направлены модули синтеза. Системы восстановления часто фокусируются на небольшом заранее определенном классе ошибок, чтобы сократить пространство поиска. Промышленное использование ограничено из-за вычислительной стоимости существующих методов.
Промышленное использование
 | Этот раздел может потребовать очистки Википедии , чтобы соответствовать стандартам качества . Конкретная проблема заключается в следующем: необходим более всесторонний обзор предмета; фильтровать то, что на самом деле используется в промышленности; упоминайте только известные статьи. ( Октябрь 2022 г. ) |
Рост сложности проектов увеличивает важность формальных методов проверки в аппаратной промышленности . [6] [7] В настоящее время формальная верификация используется большинством или всеми ведущими производителями оборудования. [8] но его использование в индустрии программного обеспечения все еще томится. [ нужна цитата ] Это можно объяснить большей потребностью в отрасли аппаратного обеспечения, где ошибки имеют большее коммерческое значение. [ нужна цитата ] Из-за потенциальных тонких взаимодействий между компонентами становится все труднее реализовать реалистичный набор возможностей путем моделирования. Важные аспекты проектирования аппаратного обеспечения поддаются автоматизированным методам проверки, что упрощает внедрение формальной проверки и делает ее более продуктивной. [9]
По состоянию на 2011 год [update], несколько операционных систем были официально проверены: Secure Embedded L4 от NICTA Микроядро , коммерчески продаваемое под названием seL4 ; OK Labs [10] Операционная система реального времени ORIENTAIS на базе OSEK/VDX от Восточно-Китайского педагогического университета ; [ нужна цитата ] компании Green Hills Software операционная система Integrity ; [ нужна цитата ] и SYSGO от PikeOS . [11] [12] В 2016 году команда под руководством Чжун Шао из Йельского университета разработала официально проверенное ядро операционной системы под названием CertiKOS. [13] [14]
С 2017 года формальная проверка применяется к проектированию больших компьютерных сетей с помощью математической модели сети. [15] и как часть новой категории сетевых технологий — сети на основе намерений. [16] Поставщики сетевого программного обеспечения, предлагающие формальные решения для проверки, включают Cisco [17] Передовые сети [18] [19] и системы Veriflow. [20]
Язык программирования SPARK предоставляет набор инструментов, который позволяет разрабатывать программное обеспечение с формальной проверкой и используется в нескольких системах с высокой степенью интеграции . [ нужна цитата ]
Компилятор C CompCert — это формально проверенный компилятор C, реализующий большую часть ISO C. [21] [22]
См. также [ править ]
- Автоматизированное доказательство теорем
- Проверка модели
- Список инструментов проверки модели
- Формальная проверка эквивалентности
- Проверка доказательств
- Язык спецификации свойств
- Статический анализ кода
- Темпоральная логика в проверке конечных состояний
- Пост-кремниевая проверка
- Интеллектуальная проверка
- Проверка времени выполнения
Ссылки [ править ]
- ^ Сангхави, Алок (21 мая 2010 г.). «Что такое формальная проверка?». EE Times Asia .
- ^ Санджит А. Сешиа; Наташа Шарыгина; Ставрос Трипакис (2018). «Глава 3: Моделирование для проверки». В Кларке, Эдмунд М.; Хензингер, Томас А.; Фейт, Хельмут; Блум, Родерик (ред.). Справочник по проверке моделей . Спрингер. стр. 75–105. дои : 10.1007/978-3-319-10575-8 . ISBN 978-3-319-10574-1 .
- ^ Введение в формальную проверку , Калифорнийский университет Беркли, дата обращения 6 ноября 2013 г.
- ^ Коэн, Бен; Венкатараманан, Шринивасан; Кумари, Аджита; Пайпер, Лиза (2015). Справочник по утверждениям SystemVerilog (4-е изд.). Независимая издательская платформа CreateSpace. ISBN 978-1518681448 .
- ^ Ле Гу, Клэр; Нгуен, ТханьВу; Форрест, Стефани; Веймер, Уэстли (январь 2012 г.). «GenProg: универсальный метод автоматического восстановления программного обеспечения» . Транзакции IEEE по разработке программного обеспечения . 38 (1): 54–72. дои : 10.1109/TSE.2011.104 . S2CID 4111307 .
- ^ Харрисон, Дж. (2003). «Формальная проверка в Intel». 18-й ежегодный симпозиум IEEE по логике в информатике, 2003 г. Материалы . стр. 45–54. дои : 10.1109/LICS.2003.1210044 . ISBN 978-0-7695-1884-8 . S2CID 44585546 .
- ^ Формальная проверка конструкции аппаратного обеспечения реального времени . Portal.acm.org (27 июня 1983 г.). Проверено 30 апреля 2011 г.
- ^ «Формальная проверка: важный инструмент для современного проектирования СБИС, Эрик Селигман, Том Шуберт и М. В. Ачута Киранкумар» . 2015.
- ^ «Формальная проверка в промышленности» (PDF) . Проверено 20 сентября 2012 г.
- ^ «Абстрактная формальная спецификация API seL4/ARMv6» (PDF) . Архивировано из оригинала (PDF) 21 мая 2015 года . Проверено 19 мая 2015 г.
- ^ Кристоф Бауманн, Бернхард Беккерт, Хольгер Блазум и Торстен Бормер Ингредиенты правильности операционной системы? Уроки, извлеченные при формальной проверке PikeOS. Архивировано 19 июля 2011 г. на Wayback Machine .
- ^ "Все правильно" Джека Ганссла
- ^ Харрис, Робин. «Неуязвимая ОС? CertiKOS позволяет создавать безопасные ядра системы» . ЗДНет . Проверено 10 июня 2019 г.
- ^ «CertiKOS: Йельский университет разрабатывает первую в мире операционную систему, устойчивую к хакерам» . Интернэшнл Бизнес Таймс, Великобритания . 15 ноября 2016 г. Проверено 10 июня 2019 г.
- ^ Скрокстон, Алекс. «Для Cisco создание сетей на основе намерений предвещает будущие технологические потребности» . Компьютерный еженедельник . Проверено 12 февраля 2018 г.
- ^ Лернер, Эндрю. «Сеть, основанная на намерениях» . Гартнер . Проверено 12 февраля 2018 г.
- ^ Керравала, Зевс. «Cisco переносит сети, основанные на намерениях, в центры обработки данных» . СетьМир. Архивировано из оригинала 11 декабря 2023 года . Проверено 12 февраля 2018 г.
- ^ «Передовые сети: ускорение и снижение рисков сетевых операций» . Успех в понимании. 16 января 2018 года . Проверено 12 февраля 2018 г.
- ^ «Освоение сетей, основанных на намерениях» (PDF) . Сетевой Мир . Проверено 12 февраля 2018 г.
- ^ «Верифлоу Системс» . Блумберг . Проверено 12 февраля 2018 г.
- ^ «CompCert — компилятор CompCert C» . www.compcert.org . Проверено 22 февраля 2023 г.
- ^ Барьер, Орель; Блейзи, Сандрин ; Пишарди, Дэвид (9 января 2023 г.). «Формально проверенная генерация собственного кода в эффективной JIT-компиляторе: превращение серверной части CompCert в формально проверенный JIT-компилятор» . Труды ACM по языкам программирования . 7 (ПОПЛ): 249–277. arXiv : 2212.03129 . дои : 10.1145/3571202 . ISSN 2475-1421 . S2CID 253736486 .