stringtranslate.com

Формальная проверка

В контексте аппаратных и программных систем формальная верификация — это действие по доказательству или опровержению правильности системы относительно определенной формальной спецификации или свойства с использованием формальных методов математики . [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 , продаваемое на коммерческой основе как seL4 компанией OK Labs; [10] операционная система реального времени на базе OSEK/VDX ORIENTAIS от Восточно-Китайского педагогического университета ; [ нужна ссылка ] операционная система 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 предоставляет набор инструментов, который позволяет разрабатывать программное обеспечение с формальной проверкой и используется в нескольких системах с высокой степенью интеграции . [ необходима ссылка ]

Компилятор CompCert C — это формально проверенный компилятор C, реализующий большую часть ISO C. [21] [22]

Смотрите также

Поищите информацию о проверяемости в Викисловаре, бесплатном словаре.

Ссылки

  1. ^ Сангхави, Алок (21 мая 2010 г.). «Что такое формальная проверка?». EE Times Asia .
  2. ^ Санджит А. Сешиа; Наташа Шарыгина; Ставрос Трипакис (2018). «Глава 3: Моделирование для проверки». В Кларке, Эдмунд М.; Хензингер, Томас А.; Вайт, Хельмут; Блум, Родерик (ред.). Справочник по проверке моделей. Springer. стр. 75–105. doi :10.1007/978-3-319-10575-8. ISBN 978-3-319-10574-1.
  3. ↑ Введение в формальную проверку, Калифорнийский университет в Беркли, получено 6 ноября 2013 г.
  4. ^ Коэн, Бен; Венкатараманан, Шринивасан; Кумари, Аджита; Пайпер, Лиза (2015). SystemVerilog Assertions Handbook (4-е изд.). CreateSpace Independent Publishing Platform. ISBN 978-1518681448.
  5. ^ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley (январь 2012 г.). «GenProg: универсальный метод автоматического восстановления программного обеспечения». IEEE Transactions on Software Engineering . 38 (1): 54–72. doi :10.1109/TSE.2011.104. S2CID  4111307.
  6. ^ Харрисон, Дж. (2003). «Формальная верификация в Intel». 18-й ежегодный симпозиум IEEE по логике в компьютерных науках, 2003. Труды . С. 45–54. doi :10.1109/LICS.2003.1210044. ISBN 978-0-7695-1884-8. S2CID  44585546.
  7. ^ Формальная проверка конструкции оборудования реального времени. Portal.acm.org (27 июня 1983 г.). Получено 30 апреля 2011 г.
  8. ^ «Формальная верификация: необходимый инструмент для современного проектирования СБИС» Эрика Селигмана, Тома Шуберта и М. В. Ачуты Киранкумара. 2015.
  9. ^ "Формальная проверка в промышленности" (PDF) . Получено 20 сентября 2012 г.
  10. ^ "Abstract Formal Specification of the seL4/ARMv6 API" (PDF) . Архивировано из оригинала (PDF) 21 мая 2015 г. . Получено 19 мая 2015 г. .
  11. ^ Кристоф Бауманн, Бернхард Беккерт, Хольгер Блазум и Торстен Бормер Составляющие корректности операционной системы? Уроки, извлеченные из формальной проверки PikeOS Архивировано 19 июля 2011 г. на Wayback Machine
  12. ^ «Getting it Right» Джека Гансле
  13. ^ Харрис, Робин. «Невзламываемая ОС? CertiKOS позволяет создавать безопасные системные ядра». ZDNet . Получено 10 июня 2019 г. .
  14. ^ "CertiKOS: Йельский университет разрабатывает первую в мире операционную систему, устойчивую к хакерам". International Business Times UK . 15 ноября 2016 г. Получено 10 июня 2019 г.
  15. ^ Скрокстон, Алекс. «Для Cisco сети на основе намерений предвещают будущие технологические требования». Computer Weekly . Получено 12 февраля 2018 г.
  16. ^ Лернер, Эндрю. «Сетевое взаимодействие на основе намерений». Gartner . Получено 12 февраля 2018 г.
  17. ^ Керравала, Зевс. «Cisco приносит сети на основе намерений в центр обработки данных». NetworkWorld. Архивировано из оригинала 11 декабря 2023 г. Получено 12 февраля 2018 г.
  18. ^ "Forward Networks: Accelerating and De-risking Network Operations". Insights Success. 16 января 2018 г. Получено 12 февраля 2018 г.
  19. ^ "Getting Grounded in Intent=based Networking" (PDF) . NetworkWorld . Получено 12 февраля 2018 г. .
  20. ^ "Veriflow Systems". Bloomberg . Получено 12 февраля 2018 г.
  21. ^ "CompCert - Компилятор CompCert C". compcert.org . Получено 22 февраля 2023 г. .
  22. ^ Barrière, Aurèle; Blazy, Sandrine ; Pichardie, David (9 января 2023 г.). «Формально проверенная генерация собственного кода в эффективном JIT: превращение бэкэнда CompCert в формально проверенный JIT-компилятор». Труды ACM по языкам программирования . 7 (POPL): 249–277. arXiv : 2212.03129 . doi : 10.1145/3571202 . ISSN  2475-1421. S2CID  253736486.