В контексте аппаратных и программных систем , формальная верификация является актом доказать или опровергнуть правильность намеченных алгоритмов , лежащих в основе системы по отношению к определенной формальной спецификации или свойствам, используя формальные методы по математике . [1]
Формальная проверка может быть полезна для подтверждения правильности таких систем, как: криптографические протоколы , комбинационные схемы , цифровые схемы с внутренней памятью и программное обеспечение, выраженное в виде исходного кода.
Проверка этих систем выполняется путем предоставления формального доказательства на абстрактной математической модели системы, соответствие между математической моделью и природой системы иначе известно при построении. Примеры математических объектов, часто используемых для моделирования систем: конечные автоматы , системы помеченных переходов , сети Петри , системы сложения векторов , временные автоматы , гибридные автоматы , алгебра процессов , формальная семантика языков программирования, такая как операционная семантика , денотационная семантика , аксиоматическая семантика. и логика Хора . [2]
Подходы
Один из подходов и форм - это проверка модели , которая состоит из систематически исчерпывающего исследования математической модели (это возможно для конечных моделей , но также и для некоторых бесконечных моделей, где бесконечные множества состояний могут быть эффективно представлены в конечном итоге с помощью абстракции или использования преимуществ симметрия). Обычно это состоит из исследования всех состояний и переходов в модели с использованием умных и зависящих от предметной области методов абстракции для рассмотрения целых групп состояний за одну операцию и сокращения времени вычислений. Методы реализации включают перечисление пространства состояний , символическое перечисление пространства состояний, абстрактную интерпретацию , символьное моделирование , уточнение абстракции. [ необходима цитата ] Свойства, которые необходимо проверить, часто описываются в темпоральной логике , такой как линейная темпоральная логика (LTL), язык спецификации свойств (PSL), утверждения SystemVerilog (SVA), [3] или логика вычислительного дерева (CTL). Большим преимуществом проверки модели является то, что она часто полностью автоматическая; его основной недостаток в том, что он, как правило, не масштабируется до больших систем; символические модели обычно ограничены несколькими сотнями битов состояния, в то время как явное перечисление состояний требует, чтобы исследуемое пространство состояний было относительно небольшим.
Другой подход - дедуктивная проверка. Он состоит из генерации на основе системы и ее спецификаций (и, возможно, других аннотаций) набора математических доказательств , истинность которых подразумевает соответствие системы ее спецификации, и выполнения этих обязательств с использованием либо помощников доказательства (интерактивных средств доказательства теорем) ( такие как HOL , ACL2 , Isabelle , Coq или PVS ), автоматические средства доказательства теорем , включая, в частности, решатели выполнимости по модулю теорий (SMT). Недостаток этого подхода состоит в том, что он обычно требует от пользователя детального понимания того, почему система работает правильно, и передачи этой информации системе проверки либо в форме последовательности теорем, которые необходимо доказать, либо в форме спецификаций ( инварианты, предусловия, постусловия) компонентов системы (например, функций или процедур) и, возможно, подкомпонентов (таких как циклы или структуры данных).
Программное обеспечение
Формальная проверка программного обеспечения включает доказательство того, что программа удовлетворяет формальной спецификации своего поведения. Подразделы формальной проверки включают дедуктивную проверку (см. Выше), абстрактную интерпретацию , автоматическое доказательство теорем , системы типов и упрощенные формальные методы . Перспективным подходом к верификации на основе типов является программирование с зависимой типизацией , в котором типы функций включают (по крайней мере, часть) спецификации этих функций, а проверка типов кода устанавливает его соответствие этим спецификациям. Полнофункциональные языки с зависимой типизацией поддерживают дедуктивную проверку как особый случай.
Другой дополнительный подход - создание программ , при котором эффективный код создается из функциональных спецификаций с помощью ряда шагов по сохранению правильности. Примером такого подхода является формализм Берда – Меертенса , и этот подход можно рассматривать как еще одну форму построения правильности .
Эти методы могут быть надежными , что означает, что проверенные свойства могут быть логически выведены из семантики, или ненадежными , что означает отсутствие такой гарантии. Звуковая техника дает результат только тогда, когда она исследует все пространство возможностей. Примером ненадежного метода является метод, который ищет только подмножество возможностей, например, только целые числа до определенного числа, и дает "достаточно хороший" результат. Методы также могут быть разрешимыми , что означает, что их алгоритмические реализации гарантированно завершатся с ответом, или неразрешимыми, что означает, что они могут никогда не завершиться. Поскольку они ограничены, необоснованные методы часто более разрешимы, чем разумные.
Верификация и валидация
Верификация - это один из аспектов проверки соответствия продукта своему назначению. Валидация - дополнительный аспект. Часто весь процесс проверки называют V&V .
- Проверка : «Пытаемся ли мы сделать то, что нужно?», Т. Е. Соответствует ли продукт реальным потребностям пользователя?
- Проверка : «Сделали ли мы то, что пытались сделать?», Т. Е. Соответствует ли продукт спецификациям?
Процесс проверки состоит из статических / структурных и динамических / поведенческих аспектов. Например, для программного продукта можно проверить исходный код (статический) и запустить его с конкретными тестовыми примерами (динамический). Валидация обычно может проводиться только динамически, т. Е. Продукт тестируется путем его типичного и нетипичного использования («Удовлетворительно ли он соответствует всем сценариям использования ?»).
Автоматизированный программный ремонт
Восстановление программы выполняется по отношению к оракулу , охватывая желаемую функциональность программы, которая используется для проверки сгенерированного исправления. Простым примером является набор тестов - пары ввода / вывода определяют функциональность программы. Различные методы используются, прежде всего с помощью выполнимости по модулю теории (SMT) решателей, [4] и генетическое программирование , [5] с использованием эволюционного вычисления для генерации и оценки возможных кандидатов для исправления. Первый метод является детерминированным, а второй - рандомизированным.
Восстановление программ сочетает в себе методы формальной проверки и синтеза программ . Методы локализации неисправностей при формальной проверке используются для вычисления точек программы, которые могут быть возможными местоположениями ошибок, на которые могут быть нацелены модули синтеза. Системы исправления часто сосредотачиваются на небольшом заранее определенном классе ошибок, чтобы уменьшить пространство для поиска. Промышленное использование ограничено из-за вычислительной стоимости существующих методов.
Промышленное использование
Рост сложности проектов увеличивает важность формальных методов проверки в индустрии оборудования . [6] [7] В настоящее время формальная верификация используется большинством или всеми ведущими производителями оборудования [8], но ее использование в индустрии программного обеспечения все еще не используется. [ необходима цитата ] Это может быть связано с большей потребностью в индустрии оборудования, где ошибки имеют большее коммерческое значение. [ необходима цитата ] Из-за потенциальных тонких взаимодействий между компонентами становится все труднее реализовать реалистичный набор возможностей с помощью моделирования. Важные аспекты проектирования оборудования поддаются автоматизированным методам проверки, что упрощает внедрение формальной проверки и делает ее более продуктивной. [9]
По состоянию на 2011 г.[Обновить], несколько операционных систем прошли формальную проверку: микроядро NICTA Secure Embedded L4 , коммерчески продаваемое OK Labs как seL4 ; [10] OSEK / VDX операционная система реального времени ORIENTAIS Восточно-Китайского педагогического университета ; [ необходима цитата ] Операционная система Integrity Green Hills Software ; [ Править ] и SYSGO «s PikeOS . [11] [12]
В 2016 году профессора Йельского и Колумбийского университета Чжун Шао и Ронгхуэй Гу разработали формальный протокол проверки для блокчейна под названием CertiKOS. [13] Программа является первым примером формальной верификации в мире блокчейнов и примером формальной верификации, явно используемой в качестве программы безопасности. [14]
С 2017 года формальная проверка применялась к проектированию больших компьютерных сетей [15] через математическую модель сети [16] и как часть новой категории сетевых технологий, сетей на основе намерений. [17] Поставщики сетевого программного обеспечения, предлагающие формальные решения для проверки, включают Cisco [18] Forward Networks [19] [20] и Veriflow Systems. [21]
Компилятор CompCert С является формально проверить компилятор реализует большинство ISO C.
Смотрите также
- Автоматическое доказательство теорем
- Проверка модели
- Список инструментов проверки модели
- Формальная проверка эквивалентности
- Проверка пруфа
- Язык спецификации свойств
- Избранная библиография для формальной проверки
- Статический анализ кода
- Временная логика в проверке с конечным числом состояний
- Пост-силиконовая проверка
- Интеллектуальная проверка
- Проверка во время выполнения
Рекомендации
- ^ Sanghavi, Alok (21 мая 2010). «Что такое формальная проверка?». EE Times Asia .
- ↑ Introduction to Formal Verification , Калифорнийский университет Беркли, по состоянию на 6 ноября 2013 г.
- ^ Коэн, Бен; Венкатараманан, Шринивасан; Кумари, Аджита; Пайпер, Лиза (2015). Справочник утверждений SystemVerilog (4-е изд.). Независимая издательская платформа CreateSpace. ISBN 978-1518681448.
- ^ Фавио ДеМарко; Цзифэн Сюань; Даниэль Ле Берр; Мартин Монперрус (2014). Автоматическое исправление ошибок при возникновении условий и пропущенных предварительных условий с помощью SMT . Труды 6-го Международного семинара по ограничениям в тестировании, проверке и анализе программного обеспечения (CSTVA 2014) . С. 30–39. arXiv : 1404.3186 . DOI : 10.1145 / 2593735.2593740 . ISBN 9781450328470. S2CID 506586 .
- ^ Ле Гуэ, Клэр; Нгуен, ТханьВу; Форрест, Стефани; Веймер, Уэстли (январь 2012 г.). «GenProg: общий метод автоматического восстановления программного обеспечения» . IEEE Transactions по разработке программного обеспечения . 38 (1): 54–72. DOI : 10.1109 / TSE.2011.104 . S2CID 4111307 .
- ^ Харрисон, Дж. (2003). «Формальная проверка в Intel». 18-й ежегодный симпозиум IEEE по логике в компьютерных науках, 2003. Труды . С. 45–54. DOI : 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
- ^ "Все правильно" Джек Гэнссл
- ^ Харрис, Робин. «Невзламываемая ОС? CertiKOS позволяет создавать защищенные системные ядра» . ZDNet . Проверено 10 июня 2019 года .
- ^ «CertiKOS: Йельский университет разрабатывает первую в мире операционную систему, устойчивую к хакерам» . International Business Times UK . 15 ноября 2016 . Проверено 10 июня 2019 года .
- ^ Хеллер, Брэндон. «В поисках истины в сети: от тестирования до проверки» . Форвардные сети . Проверено 12 февраля 2018 года .
- ^ Скрокстон, Алекс. «Для Cisco создание сетей на основе намерений знаменует будущие потребности в технологиях» . Computer Weekly . Проверено 12 февраля 2018 года .
- ^ Лернер, Эндрю. «Сеть на основе намерений» . Gartner . Проверено 12 февраля 2018 года .
- ^ Керравала, Зевс. «Cisco привносит сети на основе намерений в центры обработки данных» . NetworkWorld . Проверено 12 февраля 2018 года .
- ^ «Прямые сети: ускорение и снижение рисков сетевых операций» . Insights Success . Проверено 12 февраля 2018 года .
- ^ «Основываясь на намерениях = сети на основе» (PDF) . NetworkWorld . Проверено 12 февраля 2018 года .
- ^ "Veriflow Systems" . Блумберг . Проверено 12 февраля 2018 года .