Аналитический обзор

Введение

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

В настоящее время для поиска ошибок и уязвимостей (или доказательства их отсутствия) используются следующие подходы: 

Будучи примененными по отдельности (не образуя единой технологической цепочки), эти подходы не обеспечивают должного уровня надежности и безопасности, что обусловлено следующими причинами:

Рассмотрим каждый из подходов более подробно. 

Статический и динамический анализ применяется для обнаружения типовых ошибок и уязвимостей в программном обеспечении: в первом случае анализируется исходный код, в другом – процесс исполнения программы. Разработки в области статического и динамического анализа программ ведутся во всех развитых странах. Лидирующие позиции занимают США. Несколько промышленных инструментов разработаны в лабораториях Израиля и Европы. К наиболее известным компаниям относятся:

В России этой темой занимаются:

Тестирование позволяет выявить широкий класс ошибок в программном обеспечении путем его исполнения на ограниченном наборе сценариев. Существует большое число инструментов автоматизации тестирования, в том числе на основе моделей (формальных спецификаций), однако большинство из них ориентированы на пользовательские приложения и не учитывают специфику тестирования систем ответственного назначения: 

Среди компаний, разрабатывающих инструменты тестирования, можно выделить следующие (первые две из них специализируются на системах ответственного назначения):

Формальные методы – это целое направление в компьютерных науках и программной инженерии, которое исследует способы строго описания, моделирования и верификации программных систем опираясь на математический аппарат решают задачи повышения надежности и безопасности (защищенности) программного обеспечения. Актуальность формальной верификации программ подчеркивается, например, в отчетах Института Стандартов и Технологий (англ. National Institute of Standards and Technology) [1, 2]⁠.  Применение на практике формальных методов также требуется некоторыми международными стандартами. Например, один из ключевых стандартов в области разработки авионики DO-178, первая версия которого была разработана в конце прошлого столетия, в своей последней версии получил ряд уточняющих дополнений, посвященных исключительно применению различных методов повышения качества бортового программного обеспечения таких, как DO-333 и DO-331. В медицинской отрасли стандарты ISO 13485, ISO 14971, IEC 60601-1 требуют тщательной верификации программ для гарантий надежности и безопасности программного обеспечения. 

Формальные методы верификации применяются для доказательства корректности (надежности или безопасности) программ, то есть отсутствия в них ошибок. Суть подхода состоит в следующем:

Основными направлениями формальной верификации являются дедуктивная верификация и верификация моделей программ. Различия между ними состоят в виде проверяемых условий и используемых техниках проверки: если дедуктивная верификация нацелена на проверку функциональности в целом, то верификация моделей программ – на проверки отдельных свойств (нарушений условий безопасности). Существует несколько инструментов формальной верификации (большинство из них разработаны в академической среде и распространяются по свободным лицензиям):

Помимо "чистых" подходов к верификации, пытающихся доказать корректность модели или программы в общем случае, на практике используются "синтетические" формальные методы, которые объединяют в себе элементы формальных подходов, например, формальных моделей как способа спецификации требований к целевой системе, и техник тестирования, которые проверяют корректность целевой системы на ограниченном числе тестовых примеров. Такой подход называется тестированием на основе моделей (Model Based Testing – MBT). Он хорошо себя зарекомендовал при тестировании критичных по безопасности систем управления, например, в авионике и в задачах "тестирования соответствия", которые нужно решать, например, при проверке того, что реализация некоторого программного интерфейса или протокола отвечает требованиям соответствующего стандарта. В настоящее время инструменты класса MBT не имеют возможности для интеграции с инструментами формальной верификации, это обусловлено различием в нотациях для описания моделей/спецификаций интерфейсов и отсутствием унифицированных интерфейсов.

К числу наиболее известных технологий тестирования программных систем общего вида на основе формальных моделей можно отнести:

Разработки в области формальных методов ведутся в небольшом числе научных центров мира, наиболее известными из которых являются:

В России по инициативе ФСТЭК России внедряется процесс разработки надежного и защищенного ПО на основе современных технологий. Процесс поддерживается цепочкой инструментов, разработанных отечественными компаниями. Цепочка покрывает значительное число перечисленных подходов, нацеленных на получение доверенного ПО. Однако, если оценивать уровень технической зрелости инструментов и методик их применения в имеющейся цепочке (так же как и зарубежных аналогах) имеется по крайней мере два слабых звена. По сравнению с инструментами статического и статико-динамического анализа кода, которые уже имеют промышленный уровень зрелости, техники и инструменты дедуктивной верификации пока не достигли промышленного уровня зрелости – они используются, в основном, в университетских лабораториях и не используются практическими инженерами-программистами – это первое слабое звено. Второе слабое звено – это техники и инструменты разработки многоуровневых, многоаспектных моделей, представленных спецификациями моделей поведения программных систем, спецификациями собственно программных систем или отдельных программных моделей. 

«Многоуровневость» можно рассматривать как некоторый особый способ представления моделей не в виде монолитного кода, а в виде специальных модулей, каждый из которых описывает систему в целом, но на разных уровнях абстракции или с использованием различных уровней детализации. Необходимость разработки таких моделей и многоуровневых спецификаций предписывается рядом стандартов (например, ГОСТ Р ИСО/МЭК 15408-2012, ГОСТ Р 56939-2016 и КТ-178C), в частности, речь идет формальных моделях политик безопасности. Необходимость разработки и поддержки многоуровневых спецификаций обусловлена рядом причин. В ряде отраслей, например, в авионике или атомной энергетике, многоуровневость уже давно обусловлена требованиями наличия иерархически организованной документации (дизайн и требования высокого уровня, детальный дизайн и низкоуровневые требования, реализация на языке программирования) – опыт показывает, что такое скрупулезное документирования всех фаз проекта существенно повышает надежность ПО. В сообществе специалистов по формальным методам известно, что верификация формальных моделей становится проще, если модель представляет собой последовательность слоев, где каждый следующий является инкрементальным уточнением предыдущего. 

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

Рисунок 1. Многоуровневая модель ПО

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

Для того, чтобы не проверять весь набор требований на каждом уровне достаточно доказать выполнение некоторых требований для одного уровня, а для нижележащего доказать выполнение отношения уточнения. Определение самого отношения и способа доказательства могут в значительной степени отличаться в зависимости от устройства моделей и используемого формального метода. Чем больше отличий в наборе объектов и отношений на разных уровнях моделей, тем сложнее выполнять доказательство того, что модель одного уровня является уточнением вышележащего слоя модели. 

Еще один аргумент в пользу многоуровневости основывается на опыте организации совместной работы представителей разных специальностей, например программистов и специалистов по информационной безопасности. Первые в своих рассуждениях опираются на понятные им сущности типа файл, оперативная память, прерывание и т.д., в то время как другие (не владея в деталях знанием о структуре реализации программной системы) опираются на привычные им понятия «информационный поток», «право доступа», «роль» и другие. Опыт показывает, то для лучшего понимания друг друга специалисты готовы использовать модели – они упрощают общение и взаимопонимание. Однако такие модели не всегда легко свести одну к другой. Конкретным сложным случаем такого сведения является сопоставление высокоуровневой модели политики безопасности (политики управления доступом) в операционной системе и модели системных вызовов операционной системы. Более детально эта проблема описана в монографии П.Н. Девянин и др. Одно из решений этой проблемы запатентовано авторским коллективом ИСП РАН [3]. 

Инструменты верификации на основе многоуровневых спецификаций должны поддерживать различные техники верификации, начиная от дедуктивной верификации, заканчивая тестированием программного кода на соответствие  соответствующим формальным моделям (или отдельных уровней таких моделей). 

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

Опыт применения дедуктивной верификации к реальным системам. За исключением авионики и медицинского программного обеспечения существуют примеры программ, при разработке или верификации которых использовались методы формальной верификации. Например, формально верифицированные компилятор [4]⁠, микроядро операционной системы SeL4 [5], система организации конференций [6], формально верифицированная реализация языка ML [7]⁠, средство доказательства теорем [8], формализация логики высшего порядка [9]⁠, формально верифицированная файловая система FSCQ [10], система построения распределенных систем [11]⁠. Но список подобных программ ограничивается несколькими десятками проектов с размером верифицируемых систем порядка 20-30 тысяч строк кода (попытки верификации более крупных систем оказались неудачными).

Инструменты верификации моделей программ применимы к более сложным системам (порядка 50 тысяч строк кода), но не покрывают всех задач формальной верификации. Разработка программного обеспечения ответственного назначения находится под контролем сертифицирующих органов, требующих применения комплекса мер, закрепленных в международных стандартах (ISO/IEC 15408, DO-178С и других). К числу таких мер относятся, в частности, статический анализ кода и проверка стандартов кодирования (MISRA C/C++, Netrino C и т.п.); для этого имеются соответствующие инструменты. Между тем, для некоторых задач, связанных с моделированием и верификацией, инструментальная поддержка отсутствует. Например, стандарт ГОСТ Р ИСО/МЭК 15408-3-2013 «Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий» требует, чтобы при разработке наиболее критичного программного обеспечения (ПО) решались следующие задачи: 

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

Основная трудность связана с тем, что для работы с разными представлениями программного обеспечения используются разные нотации и инструменты, например: 

Возникает многоаспектная проблема интеграции различных средств моделирования и верификации для построения технологической цепочки, обеспечивающей сертификацию программного обеспечения в соответствии с требованиями современных стандартов. Данная проблема включает в себя следующие подпроблемы:

Данный аналитический обзор современной научно-технической, нормативной, методической литературы рассматривает те работы, которые нацелены на решение данных подпроблем.

Специализированные методы для спецификации многоуровневых формальных моделей

В данном разделе обзора рассматриваются специализированные методы и инструменты разработки и верификации многоуровневых формальных моделей программных систем с повышенными требованиями в отношении их надежности и безопасности. Для решения данной задачи на практике применяются различные специализированные формальные методы, среди которых можно выделить наиболее зрелые: Alloy, ASMs, B, Event-B, TLA+, VDM, Z. Отдельные уровни модели или некоторые требования к программной реализации также верифицируются средствами доказательства теорем (theorem provers) и проверкой моделей (model checking). В данном разделе использование инструментов аналитической верификации, основанных на универсальных средствах доказательства теорем таких, как Isabell/HOL и Coq, не рассматривается. Этим инструментам будет посвящен отдельный раздел, так как процесс построения моделей и верификации программ при помощи инструментов спецификации многоуровневых моделей существенно отличается от перечисленных выше специализированных формальных методов и требует значительно больше усилий, хотя и является более масштабируемым.

Формальные методы Alloy, ASMs, B, Event-B, TLA+, VDM, Z предназначены для построения и верификации многоуровневых моделей, поэтому инструментальные средства для них нацелены на обеспечение удобства и снижения трудоемкости этой задачи и успешно с ней справляются. В то же время из-за использования разных формализмов возможности у инструментов отличаются, в том числе и с точки зрения тех аспектов, которые рассматриваются в данной работе, а именно:

Согласно обзору, рассматривающему выбор формального метода, для использования на практике, приведенные формальные методы предоставляют существенно разные возможности для решения поставленной задачи [12]. В работе рассматривается степень выразительности средств моделирования, зрелость инструментов и возможность получения помощи и поддержки пользователей при их использовании, удобство работы и применимость инструментария на различных этапах разработки программного обеспечения. Хотя каждый метод оценивается авторами прежде всего на основе доступной литературы, а не на основе опыта применения, данное сравнение методов позволяет наглядно представить ограничения и возможности рассмотренных формальных методов.

Alloy

Формальный метод Alloy опирается на реляционную алгебру и логику предикатов первого порядка. Инструмент Alloy Analyzer представляет собой SAT решатель, который строит контрпримеры в виде графов. Данный формальный метод использовался для моделирования различных систем в то числе и систем контроля доступом, что подтверждает его применимость для задания требований абстрактной модели верхнего уровня. В то же время в нотации Alloy трудно представлять функции и рекурсивные операции, а также темпоральные свойства, так как явное понятие времени в рамках формального метода отсутствует.

Нотация Alloy достаточно сложна для понимания специалистами, не являющимися экспертами в области верификации. Это затрудняет ее применение в индустрии и, как следствие, развитие инструментов. Нам неизвестно о примерах применения данного формального метода для построения и верификации многоуровневых формальных моделей в индустриальном контексте.

К достоинствам доступного пользователям Alloy инструментария можно отнести возможность генерации Java-кода и интеграцию со средствами тестирования.

В то же время производительность инструмента верификации существенно зависит от размера и сложности модели, и при превышении определенного порога доказать корректность модели может быть достаточно сложно из-за переборного характера алгоритма верификации [13, 14]. Из-за данного ограничения Alloy трудно применять для моделирования и верификации в индустриальном контексте. Эксперименты показали, что инструмент Alloy Analyzer перестает работать стабильно, когда размер модели превышает полторы тысячи строк.

ASMs

Метод ASMs (Abstract State Machines) основан на расширенных конечных автоматах и построении их композиции. Данный метод успешно применялся для моделирования и верификации ПО для медицинских устройств, систем контроля доступом, файловых систем. 

Пример применения формальный метода ASMs для верификации медицинского оборудования представлен в работе [15]. В работе применяется подход, основанный на разработке формальной многоуровневой модели, ее уточнении и генерации тестов. Формальная модель задана при помощи композиции абстрактных конечных автоматов ASMs, для работы с которыми у авторов имеется набор инструментов: ASMRefProver для сопоставления моделей после уточнения, AsmetaS, AsmetaMA, AsmetaV для симуляции, статического анализа и моделирования сценариев соответственно и AsmetaSMV для верификации темпоральных свойств и свойств корректности (LTL, CTL) методом проверки моделей. Тестирование выполняется при помощи обхода в глубину модели и генерации тестов с использованием инструментов ATGT и CoMA.

Реализация программы была выполнена на языке Java и имела размер 2,6 тысячи строк кода. Модель была связана с исходным кодом при помощи фреймворка CoMA и аннотаций исходного кода реализации, добавленных к реализации вручную.

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

Другой пример моделирования и верификации с использованием ASMs представлен в [16]. Метод верификации подробно описан в данной работе и опирается на формат задания абстрактных конечных автоматов, полученных из обычных автоматов путем сохранения в состояниях произвольных данных.

Метод предполагает уточнение моделей и доказательство корректности уточнений автоматически или вручную. Для проверки согласованности моделей применяются подходы симуляции, проверки описанных вручную сценариев или сценариев, полученных путем генерации случайных входных данных, а также верификации модели методом проверки моделей при помощи инструмента nuSMV. Реализация системы должна быть разработана на языке программирования Java. Модель связывается с реализацией за счет аннотирования исходного кода при помощи AspectJ. Метод предлагает также схожие возможности, что и ProB, но опирается на подход проверки моделей, а не на аналитическую верификацию корректности моделей и выполненных уточнений.

В качестве примера в данной работе описан пример пошаговой верификации системы управления приземления ground control system.

Примеры демонстрируют, что данный формальный метод предлагает достаточно мощный механизм для выполнения доказательства отношений уточнения, в том числе по схеме n к m. При уточнении удается показать не только изменение структуры данных в моделях (data refinement), но и изменение в поведении (procedural refinement). Метод успешно позволяет моделировать параллельные системы. В то же время при помощи расширенных автоматов представляется трудным формулировать глобальные требования и требования живости. По этой причине метод не удобен для задания абстрактных моделей верхнего уровня, но предоставляет много средств для определения детальной спецификации.

В работе [17] детально обсуждается вопрос моделирования и верификации многоуровневой модели на примере банкомата (ATM). Авторы рассматриваются способ уточнения и построения разных уровней многоуровневой модели таким образом, чтобы они были понятны соответствующим специалистам, были корректны и удовлетворяли отношениям уточнения. Авторы детально описывают процесс моделирования, но не предлагают в рамках работы какого-либо универсального метода.

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

В инструментарии нет средств для генерации кода, но заявлена поддержка генерации тестов при помощи Asmeta. Для верификации исходного кода необходимо вручную добавить аннотации к исходному коду на языке Java, то есть переход от модели к реализации выполняется неформально.

Microsoft Research потратило много усилий для разработки инструмента MBT на основе ASMs (см. инструмент AsmL Test Tool – M. Barnett, W. Grieskamp, Yu. Gurevich, W. Schulte, Nikolai Tillmann, Margus Veanes. Scenario-oriented Modeling in AsmL and its Instrumentation for Testing.- Proc. Int’l Conf. Software Eng.(ICSE/SCESM).- 2003/5/3). Вместе с тем, через 2 года экспериментов от нотации AsmL пришлось отказаться, так как она оказалась неудобной для программистов-практиков.

B

Формальный метод B основан на теории множеств и логике предикатов первого порядка. Основным инструментом для работы с B-моделями является Atelier B, который в отличие от других рассматриваемых формальных методов, является коммерческим. 

Использование формального метода B для разработки многоуровневой формальной модели операционной системы fmC/OS представлено в работе [18]. Процесс разработки был разбит на две части: предварительно была разработана абстрактная модель верхнего уровня, включающая в себя модели 8 подсистем, а затем и модель нижнего уровня, представляющая собой уточнение абстрактной модели. Далее на основе детальной модели был автоматически сгенерирован исполняемый код операционной системы. В работе утверждается, что каждый уровень модели (абстрактный и детальный) был полезен и позволил обнаружить и исправить ряд ошибок. Авторы отметили эффективность встроенных инструментов автоматического доказательства в среде интерактивной разработки и доказательства моделей Atelier B. Инструменты позволили автоматически доказать около 70% сгенерированных условий верификации. В работе делается вывод о том, что формальный метод B может успешно использоваться при разработке операционных систем для улучшения их качества и безопасности.

Формальный метод B был также использован для моделирования механизма контроля доступом в ядре ОС Linux, который включает в себя описание аппаратной изоляции (ARM TrustZone) [19]. Разработанная формальная модель является многоуровневой и состоит из четырех абстрактных машин, которые описывают процессы операционной системы, ресурсы, и политику доступа. Четвертая машина включает в себя три предыдущие для получения доступа к определенным переменным и операциям. Она была частично верифицирована с использованием инструментов автоматического доказательства платформы Atelier B и инструмента проверки моделей ProB.

Примеры показывают, что метод применим и для задания абстрактной модели верхнего уровня и для детальной спецификации, а также для доказательства отношения уточнения между ними. Однако метод предлагает не очень наглядные средства для композиции моделей при помощи конструкций INCLUDES, USES, SEES, в то время как каждый модуль модели описывается в отдельном файле. Отношение уточнения может быть доказано только 1 к 1, то есть одну абстрактную машину может уточнять только одна абстрактная машина. В нотации B нет явного способа описывать темпоральные свойства и время. 

Для моделей на B имеется возможность верификации при помощи аксиоматической системы доказательств в Atelier B или метода проверки моделей в ProB. Это делает метод пригодным и для автоматизации поиска ошибок как в случае небольших моделей, так и для выполнения доказательства корректности крупных систем.

Метод предполагает генерацию последовательного исходного кода на основе модели в программы на языках C, C++, Java и Ada. Разработкой и внедрением формального метода B занимаются компании ClearSy4, Systerel5 и SCCH; данный формальный метод применяется в различных индустриальных проектах начиная с 80-ых годов до настоящего времени.

Event-B

Формальный метод Event-B был разработан на основе B, но в значительной степени от него отличается. Event-B предназначен в первую очередь для моделирования крупных распределенных и событийно-ориентированных систем. Спецификации в данной нотации описывают модели программ в виде автоматных моделей, с состояниями, выраженными с помощью переменных, правилами переходов между состояниями (событиями), и требованиями к состояниям (инвариантами). К недостаткам нотации можно отнести отсутствие явного способа задания параллельных процессов, времени и последовательности выполнения и темпоральных требований.

Event-B является одним из наиболее широко распространенных формальных методов, применяемых на практике для разработки и верификации многоуровневых формальных моделей. Применение формального метода в индустрии выполняется как коммерческими компаниями ClearSy и SCCH, а также различными академическими исследователями и независимыми разработчиками..

В работе [20] рассказывается об опыте использования формального метода Event-B для моделирования системы управления доступом, существенной частью которой является описание механизмов аутентификации и авторизации. Система была формализована в виде общей упрощенной многоуровневой модели с использованием техники пошагового уточнения. Модель полностью верифицирована с использованием платформы Rodin и плагина Atelier B Provers. Модель не является большой, однако демонстрирует применимость формального метода B для моделирования низкоуровневых компонентов ядра Linux.

При помощи Event-B были предложены способы демонстрации явных зависимостей между требованиями к информационной безопасности (security) и надежностью моделируемых критичных по безопасности (safety) систем [21]. Основное требование большинства критичных по безопасности систем заключается в поддержании значений некоторого параметра в рамках предварительно заданных границ. Значения данного параметра считываются при помощи сенсора, а повлиять на них можно с помощью специального актуатора. Вся логика взаимодействий с сенсором и актуатором реализуется в контроллере, который соединен с ними в общую сеть. Сеть, в свою очередь, может быть подвержена информационным атакам и данные, передаваемые через нее, могут быть искажены. 

Как правило, на первом этапе разработки модели на Event-B разрабатывается абстрактная модель верхнего уровня, в которой отражены не все требуемые свойства. Затем данная модель итеративным образом уточняется до тех пор, пока не будет разработана детальная модель нижнего уровня. Отношение уточнения доказывается только 1 к 1. Если в результате удается доказать, что абстрактная модель корректна (консистентна), а детальная модель ей не противоречит и является ее уточнением, то на основе детальной модели можно сгенерировать код, который будет корректен по построению.

Авторы в работе [21] демонстрируют два подхода по моделированию подобных систем, которые основаны на использовании формального метода Event-B. Первый подход заключается в разработке на начальном этапе небольшой по размерам и сложности модели системы, описывающей контроллер. Такая модель содержит границы значений параметров, при соблюдении которых выполняются требования надежности. Данные границы значений должны быть достаточно велики, чтобы учесть то множество деталей, которые еще не определены в модели. Затем выполняется разработка следующего уровня модели, уточняющая допустимые границы значений параметров и уточняющая особенности реализации. Трудоемкость верификации каждого уровня разработанной таким образом многоуровневой модели по порядку величины не отличается. Однако может потребоваться дополнительно валидировать предположения о программной системе и ее допустимых границах значений, заданных на разных уровнях абстракции. 

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

В главе 5 работы [22] авторы рассматривают процесс доказательство того, что детальная спецификация (функциональная спецификация) уточняет абстрактную модель, моделирующей политику безопасности операционной системы. В данной главе рассматривается именно та сложность доказательства отношения уточнения, которая возникает из-за разнородности моделей.

Техникам доказательства соответствия между формальными спецификациями некоторой программной системы, которые отличаются друг от друга степенью детализации, посвящено достаточно много исследований. Техника пошагового уточнения [23] является одной из наиболее известных и широко используемых, в том или ином виде она поддерживается большинством формальных методов, включая Event-B. В рамках этого подхода рекомендуется вести разработку поэтапно, начиная с базового уровня спецификации, содержащей максимально простую и компактную модель системы, и затем постепенно добавлять новые детали в последующих уровнях, например, путем ввода новых операций или уточнения структур данных. В ходе каждого этапа проводится две группы доказательств корректности. Первая группа нацелена на доказательство корректности каждого уровня спецификации отдельно, самого по себе. Вторая группа доказательств должна подтвердить, что каждый новый уточненный уровень полон и не входит в противоречие с предыдущим, более абстрактным уровнем, то есть все свойства системы (и вся функциональность), описанные на более абстрактном уровне, сохранены и на более детальном уровне. Общая идеология данного подхода сводится к тому, что, если на каждом этапе разработки объем «приращения» функциональности небольшой и поддается формальной верификации, и, кроме того, доказано соответствие между уровнями спецификации, то можно гарантировать, что система в целом корректна и в ней выполнены все требования, которые были сформулированы по ходу проектирования.

Схема доказательства приведена на рисунке 2. Таким образом, для доказательства соответствия между двумя спецификациями некоторой системы — между абстрактной спецификацией М1 и детальной спецификацией М2 — достаточно показать, что между ними существует такое отношение уточнения R, что для каждого перехода между состояниями из спецификации М2, который ведет из некоторого состояния s в состояние s’, существует соответствующий переход в абстрактной спецификации М1 из абстрактного состояния σ в состояние σ’. При этом переход называется соответствующим, если выполняется соотношения R(s)= σ и R(s’)= σ’. 

Рисунок 2. Схема выполнения доказательства уточнения

В общем случае доказывать требование соответствия для двух разных спецификаций одной системы достаточно трудно. По этой причине в методологиях и технологиях, которые развивали данный подход, вводились достаточно жесткие ограничения на то, как описываются новые уровни уточнения, т. е. правила детализации проектирования системы жестко ограничивались, чтобы предоставить возможность формальной проверки сохранения соответствия между более абстрактными и более детальными слоями проекта. Например, в методологии RAISE [24] нельзя было переопределять структуры данных, т. е. для каждого типа данных требовалось дать сразу полное и окончательное его описание, что для сложных и тем более развивающихся систем является очень неприятным ограничением. В Event-B нельзя изменять значения переменных, определенных ранее (на предыдущих уровнях уточнения). Хотя благодаря этому ограничению можно быть уверенным, что определенные и доказанные на прошлых уровнях инварианты будут выполняться и на всех последующих, оно существенно усложняет процесс планирования уровней уточнения при разработке спецификации.

В предложенном доказательстве соответствия (см. [22]) между моделью политики безопасности и формальной функциональной спецификацией, показано существование отношения уточнения R между их состояниями и операциями, причем на уровне формальной функциональной спецификации за переход между состояниями отвечают системные вызовы, а на уровне модели политики безопасности — де-юре требования-ограничения контроля доступа. Однако оказалось, что построение соответствия является весьма непростой задачей. Если набор структур данных и пространство состояний формальной функциональной спецификации и можно рассматривать как расширение структур данных и пространства состояния абстрактной модели, то операции формальной функциональной спецификации — системные вызовы — не удается прямо отобразить на правила модели политики безопасности.

В работе на примере показывается, как можно решить данную проблему и построить соответствие в таком случае.

В соответствии с предлагаемым методом узлы графов системных вызовов, которые соответствуют правилам политики безопасности, будут представлены в детальной спецификации как уточнения описывающих эти правила Event-B-событий. Оставшиеся вспомогательные узлы (такие как разбор параметров некоторого системного вызова) будут представлены как вспомогательные события, изменяющие исключительно дополненное состояние детальной спецификации, которое затем будет связано инвариантами с состоянием Event-B абстрактной спецификации. Используя средства языка Event-B, данные события затем будут объединены в виде цепочек, где цепочка является одним из возможных путей в представляющем системный вызов графе.

Если таким образом разбить переходы на частные случаи и сформулировать спецификацию поведения реализации системного вызова с разными параметрами, то, благодаря использованию уточнения, данная спецификация будет корректна по построению и полностью соответствовать правилам политики безопасности. Что в свою очередь будет означать, что при любом сочетании параметров и состояний системы выполнение системного вызова сохранит все установленные в политике контроля доступа требования и свойства. После этого останется только доказать выполнимость инвариантов, которые связывают дополненное состояние и состояние абстрактной спецификации. В результате формализации подобным образом всех системных вызовов будет получена формальная функциональная спецификация с доказанными свойствами непротиворечивости и полноты.

Перечисленные ранее примеры демонстрируют возможности разработки и верификации многоуровневых моделей, но доказательство соответствия программной реализации таким моделям рассмотрено не было. Одним из способов получения реализации, которая сразу по построению соответствует модели, является генерация исходного кода программной реализации на основе модели. В Event-B отсутствует явная структура потока управления – последовательность выполнения событий задается неявно в их предусловиях. Из-за этого сложно выявить и применить правила трансформации Event-B моделей в последовательный код. 

Для того чтобы определять порядок наступления событий в модели был предложен специальный язык планирования (scheduled language) [25]. Язык планирования, а так же ассоциированные с ним правила уточнения, позволяют разработчику выводить структуру программы пошаговым образом на основе серии уточняющих друг друга Event-B моделей. Данный язык позволяет вводить циклы и делать недетерминированный выбор на абстрактном уровне, а также использовать общеизвестные операторы ветвления if и циклов while на конкретном уровне. 

В статье также представлены правила, которые должны помочь разработчику в уточнении абстрактного уровня вплоть до детального. Предложенный подход был апробирован на алгоритме разметки графов, модель которого была разработана на Event-B и языке планирования.

В другой работе авторы предлагают дальнейшее развитие языка планирования для разработки моделей на Event-B с конкретной явной структурой потока управления [26]⁠. Данное расширение получило название SEB Event-B (scheduled Event-B). Хотя SEB Event-B уменьшает сложность задачи генерации последовательного кода, все еще остается некоторый разрыв между моделью и исполняемым кодом. В работе описывается метод трансляции SEB моделей в язык программирования Dafny, который состоит из набора правил трансляции компонентов модели в конструкции Dafny. Также в работе предлагается подход генерации проверочных утверждений (assertions), которые позволяют проверить корректность сгенерированного кода в инструменте статической верификации. Данные утверждения необходимы, в частности, для проверки корректности порядка сгенерированных присваиваний новых значений в локальные и глобальные переменные. Присваивания в 

Event-B задаются в блоке действий событий, и считается, что все действия выполняются одновременно и атомарно, а значит синтаксический порядок между ними не важен. Поэтому на практике требуется доказать, что сгенерированная последовательность присваиваний будет изменять состояние точно так же, как и соответствующая ей последовательность действий атомарного события. 

Предложенные в работе подходы успешно объединяют возможности верификации, предоставляемые Dafny, с абстракцией и уточнением Event-B.

В работе [26, 27]⁠ представляется инструмент SEB-CG для генерации последовательного исполняемого кода из моделей на SEB Event-B. Инструмент позволяет описывать алгоритмическую структуру моделируемых программ с помощью уточнения. Инструмент позволяет генерировать код на языках Си и Java, и при этом является расширяемым для возможности поддержки других языков. В будущем планируется расширить инструмент для генерации программных контрактов (проверочных условий, пред- и постусловий), которые затем могут быть проверены статически или дедуктивно.

Для тестирования на основе моделей для Rodin существует плагин MBT. Существует ряд работ по тестированию на основе моделей например [28] или тестированию самих моделей в [29]. В то же время о примерах реального индустриального применения данных методов на практике нам неизвестно.

При верификации Event-B моделей имеется возможность использования инструмента проверки моделей ProB, инструмента Atelier B и внешних средств автоматизированного доказательства теорем Isabelle/HOL и SMT решателей для Rodin. За счет последних процесс верификации достаточно хорошо масштабируется и позволяет доказывать как корректность сложных случаев, так и автоматизировать доказательство простых.

TLA+

Формальный метод TLA+ является развитием языка действий темпоральной логики (Temporal Logic Actions – TLA). Нотация была разработана Лесли Лампортом в Compaq для спецификации параллельных систем. Метод хорошо подходит для задания параллельных, конкурирующих и распределенных систем; в нотации присутствуют удобные средства для декомпозиции модели и доказательства выполнения отношения уточнения для таких моделей, а также понятие времени для доказательства темпоральных свойств и обеспечения характеристик производительности. 

Для разработки моделей на TLA+ предлагается использовать интегрированную среду разработки TLA+ toolbox, которая также сочетает в себе инструмент верификации на основе проверки моделей и интерактивных доказательств. Формальные модели на TLA+ могут быть транслированы на B и наоборот.

Метод TLA+ используется в работах корпораций Microsoft, Compaq, Intel и Amazon. Один из недавних примеров использования TLA+ в индустрии представлен в работе [30]. Автор описывает опыт использования формального метода TLA+ компанией Amazon для описания и верификации высокоуровневых спецификаций архитектур сложных распределенных систем. Спецификации, о которых идет речь, обычно небольшие по размеру: от 100 до 1000 строк кода. Однако даже в таком виде они позволили обнаружить и исправить ряд серьезных ошибок, которые иначе не были бы найдены другими используемыми методами верификации. Отдельно отмечается наличие дополнительного языка PlusCal, который имеет Си-подобный синтаксис и может быть автоматически транслирован в TLA+. Данный язык предназначен в качестве прямой замены псевдокода и более прост в изучении и использовании для обычных инженеров и разработчиков, чем традиционные языки формальных методов.

Данный формальный метод был использован для описания правил фильтрации сетевого трафика, проходящего через межсетевой экран (firewall), и верификации их корректности с помощью инструмента проверки моделей TLC [31]. Данные правила рассматриваются в контексте обеспечения надежности программно определяемых сетей (software-defined networking, SDN). Для верификации SDN обычно используется язык Murphy или платформа VeriSDN, но работа демонстрирует, что TLA+ является хорошей альтернативой этим устоявшимся подходам.

Нам неизвестно об использовании TLA+ для генерации тестов, но существует пример работы по верификации реализации, разработанной на языке программирования Си [32]⁠. Предложенный подход заключается в подготовке и верификации абстрактной модели, разработанной вручную также с использованием формального метода TLA+ и автоматической генерации детальной модели на TLA+ с помощью инструмента C2TLA+. Затем требуется продемонстрировать, что детальная модель является уточнением абстрактной. Наличие подобного отношения уточнения означает, что детальная модель и исходный код корректно реализуют абстрактную модель и, следовательно, удовлетворяют всем заданным и доказанным в ней свойствам. 

Доказательство корректности и согласованности модели верхнего уровня требует меньше трудозатрат, чем аналогичная работа для детальной модели. Для того чтобы дополнительно снизить трудозатраты использования предложенного метода, в рассматриваемой работе определяется операционная семантика TLA+ моделей в виде систем переходов между состояниями (state transitions systems, STS) и, используя понятие систем переходов, определено понятие уточнения между моделями TLA+.

Хотя TLA+ используется в индустрии и позволяет разрабатывать многоуровневые модели,  данный формальный метод используется для моделирования и верификации относительно небольших моделей. Область применения ограничена прежде всего из-за проблем с масштабируемостью инструментов верификации.

VDM

Формальный метод VDM является одним из старейших формальных методов, разработанных в конце 70-ых в IBM. Существует три диалекта нотации языка: VDM-SL, позволяющий задавать абстрактные типы данных с пре- и постусловиями функций, работающих с потоком данных или потоком управления; VDM++ расширяет VDM-SL возможностями задания объектно-ориентированных и параллельных моделей; VICE который добавляет к VDM++ средства для описания приложений реального времени и распределенных систем. 

Доказательство отношения уточнения в VDM опирается на операции олицетворения и декомпозиции. VDM применяется для моделирования и спецификации систем и последующей генерации кода. На практике существует ряд коммерческих генераторов кода в VDM Tools, разрабатываемой CSK Systems, и открытых генераторов Java-кода в Overture. Данные инструменты также предоставляют средства для тестирования и оценки покрытия согласно [33].

На практике данный метод применялся для моделирования и верификации прежде всего систем реального времени и управления. Так в работе [34] формальный метод VDM-SL был выбран для моделирования системы управления трафиком аэропорта благодаря выразительной мощности и наличию инструментов моделирования, тестирования, визуализации и симуляции. Инструмент VDM Tools позволил разработать и автоматически верифицировать методом проверки моделей консистентность и полноту требований в рамках абстрактной модели, а также сгенерировать после серии уточнений исполняемый программный код и протестировать детальную модель. 

Из-за сложности нотации данный формальный метод применяется достаточно редко, если сравнивать с другими упомянутыми формальными методами. Использование проверки моделей для верификации также сужает область применимости метода из-за недостаточной масштабируемости.

Z

Формальный метод Z представляет собой язык на основе теории множеств Цермело-Френкеля и логики предикатов, разработанный исследовательской группой Жана-Раймонда Абриаля в университете Оксфорда в 80-ых годах прошлого столетия. Формальный метод не предназначен для разработки многоуровневых моделей и средства для доказательства отношения уточнения ограничены, хотя и присутствуют. Метод не предоставляет средств для моделирования параллельности и явного недетерминизма. Также в нотации нет средств для явного задания глобальных требований корректности и живости и отношений времени выполнения. 

При помощи VCC и Z была верифицирована реализация планировщика на языке Си операционной системы FreeRTOS [35]. Для верификации использовался подход с уточнением моделей и двумя уровнями детальности модели. В результате авторам удалось найти несколько ошибок, подтвержденных разработчиками.

Схема доказательства корректности заключалась в разработке абстрактной модели M1 и детальной модели M2. Реализация была разработана на языке Си и обозначалась как P. Реализация программы с моделью библиотек списков вместо их реальной реализации обозначалась как P1. Верификация системы заключалась в попарном доказательстве отношений уточнения между M1 и M2, M2 и P1 и P1 и P соответственно. В последнем случае различие состояло только в использовании модели списков вместо их реальной реализации.

Авторы использовали автоматические средства доказательства, в основе которых лежит решатель Z3, что в значительной степени упрощает доказательство корректности. В то же время все модели были разработаны целиком вручную, как и описания связей между уровнями модели, использовавшейся для моделирования реализации. Интересным является шаг с отдельным сопоставлением модели M2 и P1 без использования реальной реализации списков, которая бы значительно усложнила процесс верификации.

Для разработки Z-моделей предлагается использовать инструмент Community Z Tools (CZT), основанный на среде разработки Eclipse. Для верификации используются инструменты проверки моделей ProB и интерактивного доказательства теорем на основе логики высшего порядка ProofPower, разрабатываемого британской коммерческой компанией Lemma 1 Ltd. В работах [36, 37] исследователи подчеркивают высокую сложность моделей на Z и необходимость их сопровождения дополнительными текстуальными описаниями, чтобы сделать их понятными пользователям, не знакомым с данным методом. Из-за последнего обстоятельства данный формальный метод нечасто используется на практике, хотя инструменты верификации имеют неплохую масштабируемость. 

Выводы

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

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

Event-B не всегда справляется с верификацией сложных моделей нижнего уровня и не предоставляет средств для демонстрации соответствия исходного кода модели. В то же время развитие Event-B в направлении генерации кода продолжается. 

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

Методы проверки моделей

Впервые методы верификации моделей возникли в 80-х годах прошлого столетия благодаря работам таких ученых, как Эдмунд Кларк, Аллен Эмерсон и Джозеф Сифакис. Впоследствии перечисленные ученые получили премию Тьюринга за свой вклад в развитие формальных методов верификации. 

Задача проверки моделей формулируется как проверка соответствия модели M с начальным состоянием s некоторому свойству корректности p: M,s ⊧ p. Изначально модель формулировалась при помощи структур Крипке, а требование в виде формулы темпоральной логики LTL. Схема работ по проверке моделей представлена на рисунке 3.

Рисунок 3. Схема работ по проверке моделей 

Согласно одному из авторов самого метода проверки моделей Эдмунду Кларку, появление таких технологий, как предикатная абстракция, редукция числа состояний существенно помогло развитию методов проверки моделей [38]. Сегодня развитие данных методов все еще продолжается в направлении комбинации проверки моделей и статического анализа, проверки моделей и методов интерактивного доказательства теорем, проверки вероятностных и гибридных моделей, интерпретации контрпримеров, покрытия и др. Данные результаты как расширяют область применения методов проверки моделей на системы, для проверки которых требуется учитывать различные новые свойства (темпоральные свойства, вероятностное поведение, свойства, обусловленные вещественной арифметикой), так и повышают масштабируемость методов для проверки крупных моделей и программ.

Согласно Патрику Годфруа методы проверки моделей могут дополнять друг друга в комбинации с системным тестированием, так как данные методы нацелены на обход пространства состояний модели или реализации программы [39]. Автор утверждает, что как в тестировании конечной целью является проверка выполнения программы при всех возможных входных данных и возможном поведении окружения, так и при проверке моделей задачей является проверка корректности программы при всех возможных состояниях, достижимых из начального состояния. Хотя целью проверки моделей является формальное доказательство корректности, на практике доказательство всегда является условным и выполненном при определенных предположениях, что и приближает тестирование к методам проверки моделей. В частности результатом этого развития обоих направлений является появление динамической формы проверки моделей программ, которая опирается на систематическое тестирование, и применима к индустриальным параллельным программам. Схема применения методов приведена ниже на рисунке 4.

Рисунок 4 Метод комбинирования тестирования и проверки моделей

За почти тридцатилетнюю историю развития методов проверки моделей было опубликовано множество научных работ и их обзоров. В работе Анила Карна и других представлен достаточно широкий обзор применения методов проверки моделей в программной инженерии [40]⁠. Авторы не только рассмотрели работы в области проверки моделей с точки зрения их применения и влияния на современные технологии, но и попытались обобщить направления развития данных методов.

Авторы перечисляют следующие виды программ, для верификации которых применялись инструменты проверки моделей: драйверы устройств в операционных системах, распределенные параллельные программы, приложения с пользовательским графическим интерфейсом, мультиагентные системы, сервисно ориентированных системы, программное обеспечение встраиваемых систем, аспектно-ориентированные программы, мобильные приложения, веб-приложения, системы управления базами данных, бортовое программное обеспечение авиакосмической отрасли. Кроме того, существуют примеры применения упомянутого метода в области биологии, верификации бинарного кода и обнаружения вредоносного программного обеспечения. 

Авторы отмечают, что до 2005 года целью верификации были преимущественно модели, например, модели программ, протоколов, графических моделей таких, как, UML. В последнее время усилия исследователей сосредоточены на верификации исходного кода программ. Еще одной областью применения является использование проверки моделей для тестирования или вместо тестирования тех сценариев, которые сложно воспроизвести на практике.

Верификация моделей

Хотя последние исследования в области проверки моделей нацелены на верификацию программ, применение инструментов проверки моделей для верификации именно моделей продолжается. Например в работе [41] описывается подход к формализации системы и верификации ее свойств при помощи инструмента CADP. Подход предполагает спецификацию как структуры системы, так и требований к ней в виде формальной нотации IF. В работе изначально предполагается, что требования формализованы и записаны при помощи данного языка, оперирующего с темпоральными конечными автоматами (temporal state machines), взаимодействующих при помощи пересылки сигналов. 

Авторы предлагают транслировать автоматически требования из языка IF в язык MCL (model checking language), представляющего собой расширение μ-исчисления. Сама верифицируемая система при этом задается при помощи системы переходов (Labelled Transition System - LTS). 

Верификация выполняется с использованием фреймворка CADP, который позволяет формулировать цели тестирования (test objectives) и автоматически их проверять методом проверки моделей. При этом поддерживается проверка как свойств живости, так и свойств корректности.

Другой пример применения проверки моделей для интегральной модульной авионики (IMA) предложен в работе [42]. Авторы предложили вместо традиционного при сертификации и разработке подхода к оценке рисков и верификации при помощи моделей цепочек событий использовать системно теоретический анализ процессов, предложенный ранее и уже применявшийся к верификации ИМА, но в меньшем масштабе.

Авторы предложили алгоритм анализа дизайна системы и описание ее модели и требований в виде LTL формул. Для верификации предлагается использовать инструмент проверки моделей NuSMV.

Авторы не приводят примеров индустриального применения и демонстрируют свою идею на небольшом примере.

На практике авторы применили свой подход к верификации требований для одной из систем класса управления железнодорожным транспортом European Train Control System (ETCS). Модель системы состояла из 662 состояний и 3615 переходов между ними. Авторы продемонстрировали автоматизацию процесса верификации для получения формально верифицированной модели системы, состоящей из параллельных процессов. 

Авторы не рассматривали детально процесс формализации требований, а также проблему разделения иерархии требований на уровни.

Так как демонстрация метода выполнялась на сравнительно небольшой модели, масштабируемость подхода остается неизвестной.

Другим недавним примером применения проверки моделей при доказательстве корректности моделей является проект Dione [43, 44]. В данной работе рассматривается подход для верификации моделей, заданных при помощи IOA (Input Output Automata) автоматов. Авторы отмечают, что среди существующих решений сложность верификации таких моделей была слишком высока, так как опиралась на средства интерактивного доказательства теорем таких, как Isabelle/HOL, Coq и другие. Целью авторов было автоматизировать процесс верификации, и снизить трудоемкость верификации.

Авторы предложили фреймворк и одноименный язык Dione. Язык опирается на синтаксис языка Python, но предназначен для задания параллельной композиции IOA автоматов. Затем был предложен подход к автоматической трансляции автоматов, заданных на языке DIONE, в язык Dafny. Кроме трансляции фреймворк добавляет леммы, которые используются Dafny для проверки корректности модели методом ограничиваемой верификации моделей и k-индукции. Авторам удалось отчасти автоматизировать процесс доказательства и снизить трудоемкость верификации за счет как использования более простого высокоуровневого языка задания моделей, так и за счет автоматизации доказательства корректности для случая, когда требуется работать с теориями первого порядка. 

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

Верификация программ

Некоторые программы могут уже являться моделями реальных систем. Пример верификации таких программ приводится в работе [45]⁠. В данной работе авторы описали и оценили метод автоматической проверки соответствия фотоэлектрической системы ее спецификации с использованием методов верификации моделей программ. Внимание было уделено методу проверки проектов фотоэлектрической системы, модель которой представляла собой программу на языке Си. Обычно модели таких систем проверяются при помощи средств симуляции, многие из которых являются коммерческими продуктами.

Для верификации использовались три современных инструмента ESBMC, CBMC и CPAchecker; и один специализированный инструмент симуляции HOMER Pro.

Практические результаты, полученные с помощью инструментов верификации и симуляции, сравнивались с информацией, полученной из мест, где были развернуты реальные фотоэлектрические системы. Хотя предложенный метод проверки при помощи инструментов верификации моделей программ занимает больше времени, чем методы симуляции, он способен представить детали, которые приводят к сбоям в фотоэлектрической системе. Данные сбои не удалось воспроизвести в представленной коммерческой системе симуляции. В частности предложенный метод был успешным в обнаружении ошибок. Все результаты были доказаны (sound), потому что владельцы фотоэлектрической системы и система мониторинга подтвердили возможные недостатки, которые система могла бы представлять в полевых условиях. 

Что касается сравнения инструментов верификации, то ESBMC с решателем Z3, показал лучшую производительность (примерно в четыре раза быстрее, чем CBMC), использовал меньше оперативной памяти (менее 2 ГБ по сравнению с 9,2 ГБ CBMC и 19,2 ГБ у CPAchecker).

В качестве примера формальной верификации приложений в области автомобильной промышленности служит работа Хитао Жанга и других [46]⁠. В данной работе авторы предлагают подход к проверке OSEK/VDX приложений методом проверки моделей.

Операционная система для OSEK/VDX приложений представляет собой операционную систему с детерминированным планировщиком, который управляет выполнением некоторого заданного заранее при помощи конфигурации набором приложений. Операционная система имеет также модуль для обслуживания прерываний и организации синхронизации и разделяемого доступа к ресурсам для приложений. Операционная система и приложения разрабатываются на языке Си. Операционная система и приложения широко используются в автомобильной промышленности и используются такими компаниями, как Toyota, Volkswagen, BMW и др. 

Ранее уже предлагались подходы к верификации OSEK/VDX приложений методом верификации моделей EPG. Авторы предложили автоматически транслировать операционную систему с приложениями на языке Си в препроцессированную программу при помощи CIL и затем транслировать ее на язык Promela. После чего открывается возможность использования инструмента верификации моделей Spin. Таким образом, операционная система и приложения верифицируются вместе на соответствие темпоральным свойствам живости корректности, а также проверяются условия верификации, сформулированные при помощи assert. 

В качестве результатов авторы сравнили предложенный и EPG подходы при применении к некоторому набору приложений. Авторы утверждают, что EPG подход масштабируется лучше, но в случае наличия циклов в приложениях по производительности выигрывает подход с использованием Spin.

Кармен Далран и другие предложили использовать подход комбинирования тестирования и ограничиваемой проверки моделей для сертификации программного обеспечения [36]⁠. Авторы предлагают использовать для проверки функциональных свойств реализации инструменты автоматической верификации программ. Для этого предлагается использовать на практике интерактивную среду разработки программного обеспечения для встраиваемых систем embeddr. Данная среда позволяет использовать такие инструменты автоматической верификации программ как CBMC или CPAchecker. Авторы предлагают использовать CBMC для доказательства свойств корректности, выраженных при помощи расширения языка Си операторами assert и assume. В тех случаях, когда не удается выполнить автоматическое доказательство, авторы предлагают явно записывать предположения, ограничивающие пространства состояний, то есть предположения об окружении. Данные предположения предлагается проверять при помощи тестов, генерируемых автоматически. Аналогичный подход можно применять, если не удается проверить корректность программы для определенных диапазонов значений, которые могут быть в реальности, но при которых не удается выполнить автоматическое доказательство корректности.

Выводы

Методы верификации моделей активно применяются в рамках различных работ по верификации и тестированию. В то же время сам подход проверки моделей подразумевает верификацию определенной модели, то есть в контексте спецификации многоуровневой модели данный подход позволяет анализировать только выбранный уровень. Главным достоинством инструментов проверки модели является полностью автоматическая работа, но она же является и главной проблемой масштабируемости – устранить проблему взрыва числа состояний при верификации крупной модели на практике представляется крайне трудным.

Дедуктивная верификация реализации

В данном разделе рассматриваются методы и инструменты дедуктивной верификации программ, которые предназначены для задания и проверки программных контрактов. Данные методы позволяют формализовать требования к программе, но не позволяют смоделировать систему отдельно от ее исходного кода. Инструменты дедуктивной верификации, например, SPARK или Frama-C, достаточно широко применяются на практике, так как имеют высокую степень автоматизации доказательств и низкий порог входа.

Frama-C

Frama-C – это фреймворк для статического анализа кода на языке программирования Си. Фреймворк имеет модульную архитектуру и позволяет подключать различные виды статического анализа, реализованные в плагинах. Плагины могут использовать результат работы друг друга. Язык спецификаций ACSL является для фреймворка стандартным. Он позволяет аннотировать исходный код специального вида комментариями для задания программных контрактов. В аннотациях описываются контракты функций, аксиоматизация           теорий, предикаты и другие логические конструкции. Среди наиболее используемых плагинов Frama-C можно выделить: плагин для анализа значений (value analysis, и его более новую версию enhanced value analysis EVA), плагин для генерации аннотаций об ошибках времени выполнения (RTE), плагин для слайсинга исходного кода, плагины для дедуктивной верификации исходного кода WP и Jessie.

В работе Феррара и др. рассматриваются вопросы изучения исходного кода с целью составления модели функционирования программной системы и разработки формальных спецификаций [47]⁠. Авторы выделяют ряд анализаторов, встроенных в инструмент Frama-C, которые способны облегчить выполнение этой задачи. Так, рассматриваются инструменты для предварительного статического анализа кода, слайсинга для выделения зависимых частей кода, трансляции спецификаций в проверки времени исполнения для быстрого подтверждения или опровержения гипотез о поведении кода и др. 

Авторы выделяют ряд предварительных шагов, которые совершаются при анализе любой программной системы перед построением её модели и разработкой спецификаций для неё. Сначала изучается способ сборки проекта: это необходимо для интеграции анализаторов в систему. Такие анализаторы как Frama-C не могут быть запущены непосредственно на исходных файлах проекта без предварительной подготовки и требуют глубокой интеграции в систему сборки проекта. Для анализа инструменту требуется информация обо всех частях исходного кода, заголовочные файлы используемых библиотек, конфигурация системы сборки и аппаратной архитектуры, для которой выполняется сборка проекта. На последнем шаге выполняется настройка точности анализатора и задаются параметры его запуска. 

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

В другой работе рассматривается подход к верификации индустриального кода с инструментарием Frama-C [48]. На основе своего опыта по верификации двух индустриальных проектов авиационного программного обеспечения, авторы формулируют подход к верификации нового проекта. Цель верификации состояла в доказательстве отсутствия ошибок времени выполнения. 

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

Работа с каждым слоем функций состоит из четырех шагов: 1) определение функций, которые вызывают данные и функций-заглушек, вызываемых анализируемыми; 2) запуск статического анализа (value analysis) на всех анализируемых функциях; 3) анализ всех предупреждений, полученных на прошлом шаге 4) итеративное исправление всех предупреждений (добавления спецификаций в случае ложного срабатывания, исправления ошибки в ином).

Применение языка ACSL рассматривалось с точки зрения описания требований нижнего уровня (Low-Level Requirements, LLR) авиационного стандарта DO-178C [49]. Эти требования определяют непосредственно вид исходного кода системы. В проектах, в которых участвовал автор исследования, такие LLR требования изначально записывались на английском языке как аннотации к функциям и декларациям. С требованиями нижнего уровня ассоциировано несколько так называемых DO-178C целей (objectives), которые должны выполняться для прохождения сертификации. LLR должны быть сформулированы таким образом, чтобы их выполнимость можно было проверить (verifiability). Последнее обычно показывается через ревью кода. 

На основе проведенной работы, автором делаются выводы о том, что язык ACSL хорошо подходит для выражения требований нижнего уровня (LLR) стандарта DO-178C. Более того, формализация требования через ACSL сама по себе позволяет добиться выполнения перечисленных выше целей стандарта. Однако автором также отмечается, что на момент написания текста работы (2015 год) инструментарий Frama-C реализует язык ACSL не в полной мере, что усложняет работу инженера по формальной верификации.

В работе [50]⁠ исследовалось применение абстрактной интерпретации и дедуктивной верификации для анализа программного обеспечения бразильского спутникового ракетоносителя (VLS-3). В обоих случаях использовался фреймворк для статического анализа Frama-C с плагином анализа значений (value analysis) в первом случае и дедуктивной верификации Jessie во втором случае.

Абстрактная интерпретация использовалась в двух сценариях анализа. В первом результаты анализа Frama-C для всех возможных входных значений сравнивались с конкретными значениями, полученными при симуляции на конкретных тестовых запусках, как они вкладываются в интервалы выходных значений. Во втором случае результаты конкретных тестовых запусков сравнивались со значениями, полученными с помощью абстрактной интерпретации на этих же конкретных входных значениях. В результате такого вида анализа были выявлены незначительные недостатки в коде, такие как его мертвые участки и неточности в документации. 

В ходе дедуктивной верификации функции аннотировались спецификациями на языке ACSL. Источником для функциональных требований была документация. В ходе анализа были выявлены несколько дефектов: недопустимое значение для аргумента функции, лишнее условие в функции, неявное приведение значения в инициализации float переменной. 

В ходе анализов не было выявлено ошибок, влияющих на надежность (safety) функционирования системы. Авторами отмечается, что в их случае рассмотренные виды анализа эффективно комбинируются с тестированием и дополняют друг друга в выявлении дефектов на всем диапазоне допустимых входных значений.

Парсер сертификатов X.509 также был верифицирован формально [51]. Целью авторов была разработка парсера криптографических сертификатов на языке Си с гарантиями отсутствия ошибок времени выполнения в реализации. Для этого авторами был проанализирован формат сертификатов и 200 миллионов существующих сертификатов. 

Авторы ввели верхние границы на размеры полей в формате, ограничились поддержкой только широко используемых расширений формата, отбросили поддержку некоторых устаревших форматов отдельных полей. Это позволило существенно упростить реализацию парсера и ввести ограничения на стиль разработки: использования языка С99 без массивов переменной длины (VLA) и ограниченным использованием указателей на функции, отказом от динамического выделения памяти, запретом на использование рекурсии в функциях, отказом от использования вспомогательных библиотек и других внешних зависимостей, использованием минимальных типов для неотрицательных целых чисел, ограничением на цикломатическую сложность функций и др. 

Для того чтобы получить гарантии отсутствия ошибок времени выполнения в реализации, авторами был проведен формальный анализ разработанного кода. Для этого использовался инструмент Frama-C и язык спецификаций ACSL. На исходном коде сначала запускался плагин RTE для генерации условий ошибок, далее проводился статический анализ плагином EVA (value analysis) для их проверки. В тех случаях, когда статического анализа было недостаточно, использовался плагин дедуктивной верификации WP и код дополнительно аннотировался спецификациями ACSL. Реализация парсера потребовала 8000 строк исходного кода с комментариями и 1100 строк спецификаций на языке ACSL.

Авторы работы [52]⁠ описывают опыт формальной верификации отдельных свойств подсистемы страничной организации памяти гипервизора Anaxagorus. Для этого применялся инструмент Frama-C с плагином дедуктивной верификации WP. 

Высокоуровневые требования (модельные) к подсистеме управления формулировались непосредственно на зыке ACSL в виде предикатов, выполнимость которых доказывалась в предусловиях и постусловиях к функциям. Так как исходный код гипервизора является многопоточным, все анализируемые функции были разделены на атомарные функции нижнего уровня и функции верхнего уровня, в которых многопоточность симулировалась особым образом при анализе. Последнее было необходимо, так как Frama-C не имеет инструментальной поддержки работы с многопоточным кодом. 

Функции нижнего уровня анализировались обычным образом: к ним разрабатывались спецификации на ACSL и доказывалось соответствие функций их контрактам, соблюдение глобальных инвариантов. В функциях верхнего уровня выделялись последовательные “атомарные” шаги, каждая функция разбивалась на последовательность таких шагов. Эти шаги затем оформлялись как отдельные подфункции с отслеживанием последовательности переходов между ними. 

Для симуляции многопоточности добавлялась функция с бесконечным циклом с вызовами этих подфункций внутри.

В результате было верифицированно 15 функций нижнего уровня (около 500 строк исходного кода вместе с аннотациями ACSL). Авторами не приводится количество верифицированных функций верхнего уровня. 

Для одной функции верхнего уровня set_entry (10 строк кода на языке Си), которая рассматривается в работе, приводятся данные: 80 строк потребовала ее многопоточная модель и 530 строк составили ACSL спецификаций к ней. Отдельные сложные утверждения выносились в леммы на ACSL и доказывались с помощью средства интерактивного доказательства теорем Coq. Формальная верификация была проведена в предположении корректной работы буфера ассоциативной трансляции (TLB).

В статьях [53–55] описываются разные этапы по формальной верификации ядра операционной системы Contiki для интернета вещей с помощью инструментария Frama-C. В статье [53] с помощью плагина дедуктивной верификации WP доказывается корректность работы подсистемы выделения и освобождения памяти в ядре операционной системы. 

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

В следующей работе [53, 54] анализируется исходный код криптографических функций AES-CCM. В работе доказывается отсутствие ошибок времени выполнения в их реализации. Для были использованы плагины генерации аннотаций о такого рода ошибках RTE и для верификации WP. Для проверки корректности описанных предусловий к рассматриваемым функциям и проверки работы программного интерфейса авторами также были добавлены тесты. В результате было доказано отсутствие ошибок времени выполнения в подсистеме AES-CCM ядра операционной системы Contiki.

В работе [55] формальным образом верифицируются библиотечные функции работы со списками ядра Contiki. Функции манипуляции динамическими структурами данных, такими как списки и деревья, традиционно представляют сложность для формальной верификации из-за работы с указателями. На уровне спецификаций, авторы представляли список как массив и доказывали свойства на нем. Для отображения списков на массив исследуемые функции дополнялись “теневым” кодом в спецификациях: включались дополнительные аргументы в функции, дописывался код для работы с ними, добавлялись необходимые для доказательства новые функции на языке Си в спецификации. 

В целом  для формального анализа 176 строк кода на языке  Си, было написано 1400 строк спецификаций ACSL. Дополнительно 24 леммы потребовали ручного доказательства в среде интерактивного доказательства теорем Coq. В ходе анализа в функции внесения элемента в список list_insert была выявлена проблема, которая потенциально могла приводить к нарушению целостности списка. Проблема была признана разработчиками Contiki и исправлена впоследствии. По результатам формального анализа был разработан тестовый пакет с 30 тестами для исследуемых функций.

Другие инструменты дедуктивной верификации программ

Рассмотрим примеры индустриального применения инструментов дедуктивной верификации помимо Frama-C. Например, инструмент mCRL2 использовался для обнаружения взаимных блокировок или других вариантов незапланированного поведения системы управления дорожным трафиком в туннеле.

Авторы воспользовались нотацией mCRL2 для формализации неформальной автоматной спецификации, описывающей поведение системы. Размер модели составил 700 строк кода. Модель была проверена на соответствие нескольким десяткам свойств корректности, сформулированных совместно с разработчиками системы.

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

Авторы не выявили проблем в финальной реализации системы, что они объяснили детальным тестированием и проектированием системы. Однако авторам удалось найти достаточно сложный дефект в ранней версии спецификации, потратив на это около 7 дней.

Язык Eiffel сочетает в себе функции языков программирования и языков спецификации (формализации) требований. Кроме управляющих конструкций язык позволяет записывать программные контракты, инварианты и аннотации для функций. В работе [56]⁠ описан подход к верификации программ на языке Eiffel, в основе которого лежит полуавтоматический интерактивный подход, требующий от пользователя не так много усилий как другие средства интерактивного доказательства, но все же требует в ряде случаев дополнительного аннотирования исходного кода. 

Предложенный авторами подход основан на переводе аннотированной программы на языке Eiffel сначала в абстрактное синтаксическое дерево, а затем в программу на языке Boogie, для которой генерируются условия верификации, решаемые при помощи запросов к SMT решателю.

Особенностью предлагаемого языка является работа с объектно-ориентированным кодом, с которым, например, не могут работать такие средства, как Why3, или ограничено поддерживают SPARK. В то же время детального сравнения трудоемкости и возможностей подходов на примерах не приводится.

Методы дедуктивной верификации применяются и при разработке программного обеспечения авионики. Для этого был разработан язык SPARK, расширяющий язык Ada вспомогательными конструкциями для формулирования и доказательства программных контрактов. Инструмент GNATProve для доказательства корректности программ, разработанных при помощи SPARK 2014, основан на плагине WHY3.

Работа [57] описывает пример применения языка SPARK при разработке и верификации программного обеспечения для планера. Программное обеспечение, которое требовалось верифицировать, представляло собой две части: приложение, обеспечивающее запись данных с датчиков на SD-карту и управляющее планированием, и набор библиотек для поддержки HAL и RTS (Run-time system). Приложение представляло собой программу размером около 6,8 тыс. строк кода, с аннотациями в виде пред- и постусловий для функций с цикломатической сложностью кода 2.03. 

Для доказательства корректности было доказано 3214 условий верификации, составившие 88,1% от числа всех условий, которые было необходимо доказать.

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

Сочетание методов проверки моделей и дедуктивной верификации позволило получить новые способы генерации условий верификации [58]. Авторы данного исследования рассмотрели и сравнили два подхода, используемых для генерации условий верификации, VCGen, используемый для дедуктивной верификации, и NormNF, предложенный Кларком и другими при реализации инструмента CBMC. В результате сравнения авторы предлагают шесть гибридных методов на их основе и приводят сравнение методов, реализованных для этого в инструменте SNIPER, принимающего на вход программы во внутреннем представлении LLVM.

Метод VCGen опирается на построение сильных постусловий и генерации для assertion команд верификационных условий, учитывающих локальный контекст. Второй метод, напротив, основан на глобальном контексте и генерации единого верификационного условия для всей программы. Соответственно предложенные методы различаются по форме построения логической формулы, учета глобального и локального контекста, а также семантики утверждений assert. В зависимости от выбора того или иного поведения можно построить куб гибридных методов. А с учетом ряда возможных оптимизаций таких гибридных методов становится шесть.

В статье [59] авторами рассматривается вопрос применения формальных методов к верификации кода встраиваемых автомобильных систем. Стандарт ISO 26262, определяющий требования к функциональной безопасности дорожных транспортных средств, рекомендует применение формальных методов на высоких уровнях доверия. Авторы публикации рассматривают вопрос, насколько возможно применение формальных методов и что необходимо для того, чтобы использовать дедуктивную верификацию в разработке встраиваемого программного обеспечения в автомобильной компании SCANIA.

Для формальной верификации кода на языке программирования Си использовался инструмент VCC. Он относится к тому же классу инструментов дедуктивной верификации программ, что и Frama-C. К его отличительным свойствам можно отнести возможность работы с многопоточным кодом, но, как отмечается самими авторами, работа с числами с плавающей запятой поддерживается в нем с меньшей точностью, чем в Frama-C.

Авторами исследовался критичный с точки зрения надежности код вторичного рулевого управления, который используется в грузовиках SCANIA. Код состоял из 10 функций на языке программирования Си с суммарным объемом 1400 строк. Исходный код был последовательным и не имел циклов. В документации неформальным и полуформальным образом было сформулировано 27 требований к рассматриваемому коду. Но на практике только 10 из них были выбраны для верификации при помощи VCC. Требования были формализованы по аналогии с электронной цепью, когда входные значения связываются с выходными. В результате было разработано около 700 строк спецификаций. Несмотря на то, что в коде не было выявлено функциональных ошибок, в документации обнаружились неточности и два противоречивых требования. Авторы заключают, что применение методов формальной верификации в подобного рода проектах возможно и реалистично уже сейчас.

В своей следующей работе [60] авторы обобщают опыт работы по формальной верификации в SCANIA за 8 лет. За это время было завершено:

Один из проектов по дедуктивной верификации уже рассматривался ранее, два других состояли в верификации модуля вычисления потери крутящего момента и модуля непреднамеренной активации муфты планетарной передачи. Из-за недостаточной поддержки работы с плавающими числами в VCC верифицировать требование о том, что сумма отдельных потерь крутящего момента находится в границах определенных значений, не удалось.

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

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

Инструмент UPPAAL более сложен и требует преобразования модели в временной автомат (timed automata), но предлагает более быструю производительность. Инструмент LBTest производит тестовые воздействия на систему, которая рассматривается им как черный ящик,  и постепенно строит её модель внутри себя. Когда модель построена, она проверяется на соответствие формализованным в темпоральной логике требованям к системе. Если инструмент выявляет несоответствие требованиям в построенной модели, то он выводит контрпример и посылает его в виде теста в систему. В большинстве случаев выведенный контрпример оказывается ложным и тогда выполняется уточнение построенной модели. В ином случае, выявляется нарушение требований в анализируемой системе. 

При помощи данного инструмента анализировалась также двухконтурная система рулевого управления. Из 32 неформальных требований к ней 11 не могли быть сформулированы в пропозиционной линейной темпоральной логике, остальные были формализованы. Из 10 ошибок 2 не были обнаружены инструментов LBTest. Анализ длился 7 часов, покрытие по модели достигло 97%. Необходимо отметить, что данный вид тестирования может давать хорошие результаты лишь для моделей, количество возможных состояний в которых не является слишком большим. 

В последних трех проектах использовался инструмент, разработанный в самой компании SCANIA. В инструменте управления требованиями, они могут специфицироваться, уточняться, связываться друг с другом через разные уровни абстракции, формируя иерархическое разбиение требований от высокого уровня до уровня реализации для описания программного и аппаратного обеспечений. Для описаний используется простой логический язык.

Опыт, вынесенный авторами из этих работ, свидетельствует о том, что в большом количестве случаев требования плохо сформулированы даже на высоком уровне, что свидетельствует о плохом качестве неформальных требований к работе систем. Выявление недостатков в данном случае является критичным с точки зрения скорости анализа и предоставления обратной связи, даже с учетом некоторого количества ложноположительных срабатываний.

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

В своем докладе на конференции FCSD19 “Deductive verification of industrial automotive C code” один из авторов приведенных работ (Christian Lidström, KTH Royal Institute of Technology) отметил, что впоследствии они перешли от использования инструмента дедуктивной верификации VCC к инструменту Frama-C.

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

Работа исследователей из университета EPFL (Швейцария) рассматривает построение фреймворка для верификации реализаций сетевых функций для виртуальных сетей [61]⁠. Авторы поставили целью разработать фреймворк для разработчиков программного обеспечения для телекоммуникационного оборудования для построения виртуальных сетей (Software-defined networks). В своей работе авторы выделяют две ключевые проблемы в области верификации программного обеспечения программируемых сетевых устройств и предлагают пути их преодоления: сложности и трудоемкости верификации для инженеров, которые не являются экспертами в области верификации, и большой стек сложного для верификации встраиваемого программного обеспечения. Решение заключается в разработке специального стека программного обеспечения над аппаратным обеспечением, верифицированного формально и обеспечивающего простоту реализации и верификации новых сетевых функций (Network Function).

Стек программного обеспечения для реализации сетевых функций состоит из фреймворка для входящих и исходящих пакетов, драйвера сетевой карты, библиотеки сетевых функций, библиотеки абстрактных данных libVig и специальной операционной системы NFOS. Процесс верификации предполагает символьное выполнение при помощи инструмента KLEE всего стека фреймворка и реализованных сетевых функций для обнаружения возможных путей выполнения и их преобразования в последовательные программы на языке Си без циклов и ветвлений. Затем в полученные программы добавляются леммы и инварианты, относящиеся к библиотеке libVig, используемой при реализации сетевых функций. Затем выполняется автоматическое доказательство корректности при помощи Verifast. Схема работы изображена на рисунке 5:

Рисунок 5. Схема верификации сетевых функций

Авторы показали возможность масштабирования верификации, хотя использовалось достаточно высокопроизводительное оборудование. Доказательство корректности отдельной сетевой функции требовало несколько секунд и Гб оперативной памяти, а весь стек уже около получаса и почти 700 ГБ оперативной памяти. Размер спецификаций, который требуется написать для отдельной сетевой функции составляет не более 10% от размера реализации (авторы рассматривали исходный код размером менее 1 тысячи строк кода).

Предложенный авторами процесс верификации нацелен на снижение трудозатрат на верификацию, а именно устранение необходимости выполнения сложной подготовки к верификации, то есть разработки спецификаций и моделей, и участия человека в построении доказательств. Но пользователь все же должен разработать спецификацию на языке Python для того, чтобы связать реализацию сетевых функций со спецификацией сетевых протоколов, моделью библиотеки libVig и сформулировать непосредственно функциональные требования для верифицируемых функций. К недостаткам предложенного подхода можно отнести невозможность верификации таким образом существующего программного обеспечения и сложность борьбы с ситуациями, когда при верификации возникает проблема взрывного роста числа возможных путей. 

В работе [62] рассматривается формальная верификация исполняемого кода для микроконтроллера электрокардиостимулятора. Верификация выполнялась с учетом темпоральных свойств. Авторы сформулировали модель требований верхнего уровня как TTS (timed transition system) и аналогичную модель для реализации. Авторы использовали подход Well-Founded Equivalence Bisimulation (WEB) refinement для доказательства соответствия моделей друг другу⁠.

Хотя формальная верификация программного обеспечения для электрокардиостимулятора выполнялась ранее с использованием UPPAAL новизна данной работы связана с верификацией именно исполняемого кода и доказательства соответствия TTS моделей друг другу. В то же время, хотя авторы показали возможность построения многоуровневой модели и ее верификации на практике для данного случая, каких-либо инструментальных средств для переиспользования данного подхода предложено не было. Модели были разработаны вручную и также вручную выполнялись запросы к SMT решателю для доказательства условий верификации.

В работе Нельсона и других описывается верификация ядра операционной системы Hyperkernel [63]⁠. Авторы вдохновлялись работами по верификации операционных систем, выполненных с использованием средств интерактивного доказательства теорем, например, CertikOS и SeL4. Но задачей было выполнить формальную верификацию ядра операционной системы существенно меньшими усилиями, автоматизировав процесс доказательства корректности.

Авторы поставили задачу верификации ядра операционной системы Hyperkernel, построенной на базе xv6, схожей с Unix. Авторы разработали декларативную спецификацию для проверки требований высокого уровня на языке Python размером порядка 300 строк и автоматную спецификацию, также разработанную на языке Python, размером около 800 строк. Реализация операционной системы представляет собой 7 тысяч строк на языке Си.

Операционная система представляет собой ОС общего назначения, с разделением адресного пространства ядра и приложений и ограничениями на максимальное количество захваченных процессами ресурсов. ОС предназначена для систем с единственным процессором и ядром. Такие ограничения были сделаны для упрощения процесса верификации. Верификации подвергалась реализация ОС без слоя взаимодействия с аппаратурой и приложениями пользовательского пространства.

Авторы разработали декларативную спецификацию для функциональных требований верхнего уровня, автоматную реализацию, уточняющую спецификацию верхнего уровня и реализацию. Доказательство корректности выполнялось при помощи решателя Z3. При верификации были доказаны теоремы о том, что автоматная модель удовлетворяет декларативной спецификации, а реализация является уточнением автоматной модели (refinement). Для доказательства последней теоремы была разработана вспомогательная функция эквивалентности на языке Python, которая отображает все структуры данных ядра на переменные состояния автоматной модели. Для верификации был также разработан верификатор размером около трех тысяч строк кода на языках Python и C++.

Авторы показали возможность выполнения верификации согласно предложенному подходу. Хотя точные оценки трудоемкости не приводятся, но основные силы разработчиков были потрачены на реализацию и разработку моделей, а не на верификацию. Так решатель Z3 доказал необходимые условия верификации за 20 минут. В то же время подход не является универсальным, так как масштабируемость решателя ограничена и для того, чтобы не превысить возможности решателя, в архитектуре операционной системы были добавлены ограничения, сокращающие пространств состояний автоматной модели.

В работе [64] рассматривается вопрос формальной верификации ядра Linux с использованием автоматных моделей. По автомату генерируется код специального драйвера-монитора ядра. Последний динамически загружается в работающую систему и, отслеживая определенные события в ядре операционной системы, выполняет её проверку на соответствие модели. Таким образом выполняется динамическая верификация ядра.

Выбор авторов в пользу динамического метода обусловлен большим объемом кода ядра Linux, который постоянно обновляется, и ложными срабатываниями при использовании статических методов. Авторами приводится несколько моделей, на основе которых они реализовали динамические проверки в ядре описываемого подхода. Необходимо отметить, что модели являются достаточно простыми и представляют собой конечные автоматы с переходами, срабатывающими по наступлению определенных событий в ядре, а именно вызовам определенных функций. Таким образом, модели не имеют внутреннего глобального состояния. Во всех случаях сгенерированные драйверы для динамической проверки не содержат кода, который бы обращался к глобальным структурам данных ядра, отслеживается только вызов определенных функций. 

Авторами не упоминаются специальные требования к процессу сборки, хотя, вероятно, необходимо включить опции, позволяющие отслеживать наступление определенных событий в ядре. Конкретно в случае приводимых в статье примеров: опции отслеживания включения/отключения прерываний на процессоре и включения/отключения вытеснения потоков в ядре. 

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

Авторами было выявлено несколько дефектов в коде ядра Linux, производительность ядра при таком динамическом анализе страдает незначительно (при условии сравнения одной и той же конфигурации ядра Linux в работе с модулем динамической проверки и без него).

Интеграция инструментов дедуктивной верификации программ и тестирования

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

Статья [65] описывает работы по тестированию ранее рассмотренной работы [52] по формальной верификации гипервизора Anaxagorus. Авторам не удалось полностью доказать все рассматриваемые свойства в ходе дедуктивной верификации. Сложные для доказательства условия верификации требовали включения информации о работе аппаратного обеспечения и его модели. Эти свойства вместе с участками кода функций, где не удавалось провести доказательство, идентифицировали и выделяли в отдельные функции меньшего размера. Обозначенные свойства с языка формальных спецификаций ACSL вручную переписывались на язык Си, для функций разрабатывались тесты с критерием покрытия по всем путям с учетом некоторых ограничений на размеры входных значений. Это позволило проверить тестами те требования к исходному кода гипервизора, которые не поддавались формальному доказательству.

В статье [66] рассматривается вопрос интеграции формальной верификации и тестирования. Авторы используют инструмент Frama-C для анализа исходного кода на языке программирования Си. Предложенный подход состоит в том, чтобы транслировать формальные спецификации в Си код и генерировать тесты для проверки описываемых ими свойств. 

Подмножество языка ACSL может быть транслировано в код на языке программирования Си в виде проверок и ассертов. Это подмножество называется Executable ACSL (E-ACSL). Авторами был разработан плагин для Frama-C, названный StaDy, который осуществляет генерацию E-ACSL в Си и проставляет метки для покрытия тестами. Другой инструмент PathCrawler используется для генерации тестов с учетом транслированных предусловий и критериев покрытия. PathCrawler - это конколик (конкретно-символьный) генератор тестов для языка программирования Си. 

Разработанный авторами публикации подход интересен с точки зрения отладки спецификаций (предоставления тестов-контрпримеров) и покрытия тестами сложных для дедуктивной верификации свойств.

В продолжении своей работы над инструментом StaDy [67, 68] авторы более подробно раскрывают то, каким образом тестирование может быть совмещено с дедуктивной верификацией. Описывается ряд сценариев работы инструмента, которые могут помочь инженеру по формальной верификации отладить спецификации и покрыть тестами не поддающиеся доказательству свойства. Инженер, столкнувшись с тем, что не удается провести доказательство соответствия кода его спецификации, вынужден тратить большое количество времени на выяснение проблемы. Автоматическое доказательство может не выполняться из-за неполноты спецификации, ошибки в коде, некорректной спецификации или же из-за того что условие верификации слишком сложно для разрешения автоматическими решателями в заданных ограничениях на время и память. Помочь инженеру в такой ситуации может предлагаемый авторами подход автоматической генерации тестов, способный либо найти контрпример для разработанных спецификаций, либо повысить уверенность в их корректности, если подобрать такой не удается.

Авторы расширяют E-ACSL специальными конструкциями для генератора тестов, которые дают возможность вводить ограничения на порождаемые входные данные, например, их размер. Предложенный подход также помогает в выявлении неполных спецификаций, например, неполноты инвариантов цикла: когда постусловия не доказываются автоматически, а сгенерированные тесты полностью удовлетворяют контракту, то это помогает выявить ситуации нехватки возможностей автоматических решателей. 

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

Авторами статьи [69] был создан инструментарий LTest для автоматического тестирования программ на языке программирования Си. LTest является набором инструментов для автоматического построения тестов для Си программ с открытым исходным кодом.

Инструмент создан на основе Frama-C и использует результаты работы других плагинов. LTest достигает автоматизации за счет встроенных в инструмент возможностей оценки покрытия, генерации тестов, детектирования непокрытых тестовых объектов. Механизм меток используется для задания критериев покрытия. Метка представляет собой предикат, прикрепляемый к инструкциям программы. Метка считается покрытой тестом, если поток выполнения достигает её, и предикат метки выполняется. С помощью механизма меток авторы моделируют множество стандартных критериев покрытия, таких как DC, CC, MCC, IDC и др. 

Инструментарий LTest строится на четырёх плагинах к Frama-C: LAnnotate, LReplay, LUncov и LGenTest. LAnnotate встраивает метки в исходный код функций на основе заданных стандартных критериев покрытия. LUncov вычисляет недостижимые метки на основе результатов плагина анализа значений Frama-C. LReplay занимается запуском тестов и мониторингом покрытия. LGenTest используется для генерации тестов на основе меток в исходном коде. Он является модифицированной версией конколик тестового генератора PathCrawler.

В работе [70] авторы описывают опыт применения своего инструмента LTest для создания тестового пакета по индустриальному коду Mitsubishi Electric, так как тестирование в индустрии применяется более активно чем иные виды анализа кода и декларируется обязательным в ряде стандартов.

Авторами применялись уже ранее рассмотренные инструменты LTest/PatchCrawler для анализа порядка 80 тысяч строк кода (без заголовочных файлов), включающих 1300 функций и распределенных по более 150 файлам. Индустриальный партнер разработал свой инструмент Annotator для аннотирования кода метками согласно требуемым критериям покрытия, инструмент Stubber для создания заглушек при unit тестировании и Output Process для составления отчетов об анализе. 

Генерация тестов по коду заняла порядка 8 часов времени на обычном компьютере, в то время как разработка этого же тестового пакета программистами занимает оценочно 230 дней.

Выводы

Исходя из проделанного обзора работ по формальной верификации индустриального кода с помощью инструмента Frama-C, можно сделать выводы о его достаточной зрелости для такого вида работ. Однако, во многих публикациях отмечается ряд недостатков в существующем инструментарии и нехватка отдельных функциональных возможностей, которые могли бы существенным образом упростить и ускорить работы по формальной верификации. В частности, отмечаются проблемы масштабирования анализа: инструменты плохо работают с большими участками кода (более 10000 строк кода), из-за чего их приходится разбивать на более мелкие части, что является проблемой для уже устоявшегося исходного кода. В инструментарии присутствуют проблемы со стабильностью доказательств: при обновлении версии инструментов или их библиотек существующие артефакты формальной верификации требуют повторного доказательства. Не всегда то, что доказывалось в прошлой версии, будет доказано в новой автоматически. Существует и проблема отладки спецификаций: требуется большой опыт работы с инструментами и знание деталей их внутреннего устройства, чтобы выявить проблемы в процессе доказательств. В части выразительности языка ACSL отмечается, что на нем нельзя выражать темпоральные свойства, описывать гиперсвойства, делать подтипизацию контрактов для полноценной поддержки указателей на функции, выполнять отношения симуляции для работы с параллельными программами, описывать требования в логике высших порядков. Также отмечается слабая поддержка работы с множествами и отображениями.

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

Аналитическая верификация без автоматической генерации условий верификации

Наиболее выразительными формальными методами с точки зрения моделирования и универсальными с точки доказательства корректности являются основанные на логике высоких порядков системы аналитической верификации, например, Coq и Isabelle/HOL. Данные инструменты успешно справляются и со спецификацией и верификацией многоуровневых моделей, и с верификацией реализации на соответствие детальной спецификации. В то же время в отличие от специализированных инструментов спецификации моделей трудоемкость моделирования существенно выше, так как готового фреймворка и инструментов автоматизированного доказательства корректности под рукой у разработчика нет. От инструментов дедуктивной верификации программ данный класс инструментов отличает отсутствие уже поставляемого в рамках инструмента генератора условий верификации. Как следствие к недостаткам данных формальных методов относится высокая трудоемкость, так как построение моделей и доказательств выполняется преимущественно вручную.

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

Далее для краткости реализацией системы будем называть ее исходный код, а формальной моделью – описание программной системы, сформулированное на каком-либо формальном языке, семантика которого полностью определяется какой-либо исполнимой программной реализацией. Любое  утверждение о структуре или поведении программы на этом языке полагается истинным только при условии подтверждения его истинности соответствующей программной реализацией: алгоритмом типизации, ядром системы, реализующим вывод в соответствующей логической системе, SMT-решателем или каким-либо другим инструментом.

При таком подходе к определению реализации и модели программной системы, существующие подходы к верификации соответствия между ними можно разделить на три основных направления: погружение (embedding), экстракцию или кодогенерацию и аннотирование спецификациями. 

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

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

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

Затем реализация системы вместе с соответствующими ей аннотациями подается инструменту верификации, который может реализовывать различные алгоритмы преобразования программы и ее спецификации для получения набора утверждений на промежуточном формальном языке. Он может как совпадать с каким-либо существующим формальным языком, например, логическими формулами первого порядка в теориях в формате SMT-lib или набором языков, используемом Coq, PVS или Isabelle, так и являться новым специальным формальным языком, используемом только в данной конкретной системе верификации. 

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

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

Основное преимущество инструментов, основанных на погружении (embedding), это богатая выразительность используемых языков формальной спецификации, позволяющих выражать в рамках одной и той же системы верификации спецификации самых различных видов, использующие самые разные логические формализмы, например: 

Для всех логических формализмов системой верификации гарантируется одинаковая степень надежности соответствующих логических выводов, опирающаяся на использование базового логического формализма, реализованного в данной системе верификации (например, языка с зависимыми типами Gallina для Coq, основанного на интуиционистской теории типов или ядра Isabelle/Pure системы Isabelle/HOL, основанной на формализации классической логики высших порядков). 

Основной недостаток таких методов — слабость специализированной инструментальной поддержки для каждого отдельного конкретного логического формализма. Как следствие, доказательство утверждений в соответствующих формализмах происходит либо с использованием очень подробных формальных доказательств, разрабатываемых пользователем системы, либо с использованием специализированных решающих процедур, которые необходимо либо разрабатывать специально для каждого конкретного логического формализма с помощью средств соответствующей системы верификации. Для этого могут применяться, например, внутренний программный интерфейс системы Coq, реализованный на языке OCaml, язык доказательств Ltac для системы Coq и язык Isabelle/ML, представляющий собой диалект Standard ML для системы Isabelle или среды метапрограммирования для системы Lean. Другое возможное решение заключается в адаптации существующих внешних инструментов для использования — Hammer-подобные инструменты, позволяющие удобно и эффективно использовать SMT, суперпозиционные и некоторые другие решатели в системах Isabelle (SledgeHammer), HOL Light и HOL4 (HOLyHammer) и Coq (CoqHammer).

Слабость инструментальной поддержки в современных интерактивных средах верификации менее существенна при разработке высокоуровневых формальных спецификаций и становится более существенной для более детальных спецификаций, тем более для моделей реализаций программ, являющихся, как правило, существенно более детальными, чем даже формальные спецификации самого нижнего уровня. Соответственно основные направления развития данного класса инструментов — поддержка новых логических формализмов,  формализация семантики новых исходных языков программирования и разработка трансляторов в соответствующее встроенное представление языка внутри системы верификации (основанное на формальной семантике), а также разработка новых средств автоматизации доказательств, как общих, так и специализированных.

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

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

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

Главное преимущество инструментов верификации, основанных на аннотировании существующего исходного кода формальными спецификациями — высокая степень автоматизации доказательств корректности для значительного числа встречающихся на практике видов спецификаций и программ. Например, может быть полностью автоматизирована проверка спецификаций в некотором фрагменте сепарационной логики, или достигнута высокая степень автоматизации для доказательства классических контрактных спецификаций для фрагментов программ, работающих с одномерными массивами (в частности, строками). 

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

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

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

Как правило, глубокое встраивание предполагает практически полное сохранение структуры исходного кода реализации системы, в то время как неглубокое встраивание допускает существенное преобразование исходного кода для приближения его структуры к структуре, типичной для соответствующих конструкций целевого языка. Например, для императивных языков программирования, таких как Си, при глубоком встраивании для таких конструкций, как условный оператор, цикл, вызов функции и последовательность инструкций в целевом языке создаются специальные сущности (например, конструкторы некоторого алгебраического типа в таких системах, как Coq или Isabelle). Затем для этих сущностей в явном виде задается операционная, денотационная, либо аксиоматическая семантика, которая является единственным исходным определением погруженного языка. На нем в дальнейшем строятся все доказательства свойств погруженной программы. Такой подход существенно упрощает создание инструмента, автоматизирующего погружение программ, но часто также и усложняет процесс верификации, так как для погруженного языка в результате необходимо создавать отдельный достаточно большой набор базовых доказательств, формализующих свойства его основных конструкций. 

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

Глубокое погружение при выполнении аналитической верификации

Одним из наиболее известных направлений в верификации программ с использованием глубокого погружения является развитие и применение набора инструментов VST (Verified Software Toolchain), который основан на глубоком погружении Си-программ в среду интерактивной верификации Coq с использованием определений сущностей языка.  Определения основаны на семантике языка программирования Си, формализованной в рамках верифицированного компилятора CompCert, а также специально разработанной логики для доказательств утверждений о погруженных программах и специально разработанного инструментария (определений, доказательств и автоматизирующих тактик) для поддержки спецификации программ с использованием различных расширений сепарационной логики. 

В статье [71] представлен результат формальной верификации реализации криптографического алгоритма аутентификации HMAC (Hash-Based Message Authentication Ccode, код аутентификации сообщений, использующий хеш-функции, один из механизмов проверки целостности информации, позволяющий гарантировать то, что данные, передаваемые или хранящиеся в ненадёжной среде, не были изменены посторонними лицами) с использованием хеш-функции SHA-256 относительно соответствующей функциональной спецификации, неформально описанной в FIPS (Federal Information Processing Standard - Федеральный стандарт по обработке информации, cтандарт компьютерной безопасности правительства США, используемый для сертификации криптографических модулей), а также верификации соответствующей формализованной функциональной спецификации относительно ожидаемых криптографических свойств (в соответствии с формализацией понятия псевдослучайной функции в работах M. Bellare и др.).

Данная работа представляет собой пример непрерывного (безразрывного) доказательства (end-to-end proof), так как результатом доказательства является теорема о программе на языке ассемблера, полученной в результате компиляции реализации криптографического алгоритма, но сформулированная в общих криптографических терминах. Таким образом, доказательство объединяет доказательства  корректности реализации алгоритма, корректности компилятора CompCert и криптографической безопасности функциональной спецификации алгоритма без неформализованных разрывов между соответствующими формализациями. 

Все формализации и доказательства выполнены в среде интерактивного доказательства теорем Coq с использованием трех реализованных в этой среде систем верификации — Foundatinal Cryptography Framework [72]⁠ для верификации криптографических свойств функциональной спецификации алгоритма, VST для верификации соответствия реализации алгоритма на языке Си его функциональной спецификации и CompCert для замыкания непрерывного доказательства с помощью верифицированной компиляции Си кода в ассемблерный код. 

Общее соотношение размеров спецификаций с доказательствами к размеру кода реализации алгоритма в данной работе составило около 35 строчек спецификации или доказательства в Coq на каждую строку реализации алгоритма (всего приблизительно 14 тысяч строк Coq на 400 строк Си). 

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

Еще одним примером верификации реализации небольшой, но достаточно критичной программной системы с помощью глубокого погружения с использованием инструментария VST является работа [73]. В ней представлены результаты верификации реализации параллельной системы обмена сообщениями через буфер с возможностью параллельного чтения и эксклюзивной записи и доказанными свойствами функциональной корректности и защищенности от компрометации со стороны некорректно функционирующих клиентских процессов чтения или записи. 

Реализация системы обладает тремя основными свойствами: 

Соответствующие утверждения были сформулированы и верифицированы с использованием конкурентной сепарационной логики с модельным состоянием (concurrent separation logic with ghost state) в системе Coq с использованием инструментария VST, расширенного операцией атомарного обмена значений. Так как VST  основан на семантике Си из верифицированного компилятора CompCert, полученный результат также является примером непрерывной верификации. 

Общее соотношение объема спецификаций и доказательств к объему кода составило около 16 строк Coq на одну строку Си (2860 строк Coq на 180 строк реализации). Работа представляет пример верифицированной реализации протокола с разделяемой памятью на языке Си с использованием инструмента VST и предложенной в работе аксиоматизации операции атомарного обмена. 

Протокол изначально предназначен для использования во встроенных системах, таких как автономные транспортные средства, однако, может быть использован в любой ОС с защитой памяти и механизмом разделяемой памяти.

Для облегчения верификации Си-программ с помощью инструментария VST был разработан набор тактик VST-Floyd [74]⁠, который позволяет частично автоматизировать процесс доказательства свойств функциональной корректности погруженного кода Си-программ. 

Свойства были представлены в виде спецификаций, выраженных в логике Verifiable C, расширяемой  сепарационной логики высших порядков. Ее семантика верифицирована относительно семантики языка Си (промежуточного представления Clight), формализованной в рамках компилятора CompCert.

В статье приведены примеры использования разработанного набора тактик для верификации реальных Си-программ на соответствие функциональным спецификациям. Соотношение размера доказательств к размеру Си-кода составляет на этих примерах от 5 до 22, в среднем 14. Время, затрачиваемое на верификацию, оценивается как составляющее от 3 до 25 человеко-недель (в среднем 9) на Си-программу размером около 200 строк. Также на этих примерах оценивается опыт использования системы Coq, необходимый для достаточно эффективной работы с системой, который составляет от 0.3 до 7 лет (в среднем 4,5 года).

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

Для поддержки верификации реалистичных интерактивных программ, достаточно произвольно взаимодействующих с окружением, в работе была разработана корекурсивная структура данных общего назначения, названная деревом взаимодействий (interaction tree).  Построенная по аналогии со «свободными монадами», эта структура по сути является их коиндуктивным аналогом, представляющим программу в виде дерева неинтерпретированных событий, связанных между собой с помощью потенциально отложенных возобновлений (продолжений) (continuations). Такое представление дает возможность композируемого построения произвольных интерпретаторов таких деревьев взаимодействия, которые передают конкретную семантику ранее не интерпретированным событиям с помощью обработчиков (event handlers). Они определяют семантику событий как последовательностей действий внутри некоторых монад (свободная композиция достигается за счет того, что каждый обработчик может независимо определять свой монадный трансформер). 

Деревья взаимодействий представляют собой достаточно выразительный подход к формализации семантики программ, позволяющий представлять побочные эффекты, незавершающиеся вычисления, паралеллизм и взаимную рекурсию, допуская при этом верификацию  программ относительно спецификаций, выраженных в терминах слабой бисимуляции. В отличие от подходов, основанных на операционной семантике и требующих изменения структуры самой определяемой программы для ее трансляции в исполнимый код, интерпретация деревьев взаимодействий позволяет задавать различные семантики с помощью обработчиков отдельно от самой программы, не изменяя тем самым ее структуру. Это позволяет упростить доказательства, которые теперь могут проводиться напрямую с помощью структурной индукции. Она устанавливает отношение бисимуляции между исходной и транслированной программой.

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

Практическая применимости подхода, основанного на деревьях взаимодействий, продемонстрирована в работе [75]. В ней представлены результаты формальной верификации реализации сервера подкачки (swap server) на языке Си на соответствие высокоуровневой функциональной спецификации, заданной в виде простого линеаризованного дерева взаимодействия сервера с одним клиентом.

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

Представленное доказательство включает в себя два основных доказательства соответствия между разными уровнями спецификации системы: соответствие Си-программы низкоуровневому дереву взаимодействий, подробно моделирующему взаимодействие реализации сервера с несколькими произвольными клиентами в реальной сети, и соответствие низкоуровневого дерева взаимодействий линеаризованному дереву, которое выражается с помощью специального отношения слабой симуляции — отношения сетевого уточнения (network refinement relation).

Для погружения, спецификации и верификации Си-кода в работе используется инструментарий VST. Однако для достижения непрерывности верификации в случае реализации сервера недостаточно гарантий, предоставляемых  верифицированным компилятором CompCert, необходима также верификация спецификаций сетевых взаимодействий. С этой целю в качестве спецификаций, а также верифицированных реализаций примитивов сетевых взаимодействий были использованы соответствующие фрагменты формализации верифицированной операционной системы CertiKOS mC2. 

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

В рамках данной работы также было разработано расширение инструментария VST поддержкой утверждений о состоянии окружения (the external assertions), которое не требовалось ранее при верификации замкнутых, то есть не взаимодействующих с окружением интерактивно, программ и библиотек. 

Помимо верификации в работе также было использовано случайное тестирование с помощью инструмента QuickChick (работающего в рамках среды Coq) для предварительной проверки разрабатываемых спецификаций.

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

Схожий прямолинейный подход был использован в нескольких работах по формальной верификации реализаций целых операционных систем, таких как CertiKOS mC2 и uC/OS-II. Основное достижение этих работ — разработка полностью формализованного (обеспечивающего непрерывную верификацию) набора инструментов для спецификации, композирования, верифицированной компиляции и сборки сертифицированных  параллельных уровней абстракции. 

Набор инструментов под названием CCAL описан в статье [76] и состоит из трех основных частей: композиционной семантической модели параллелизма, основанной на идеях игровой семантики вычислений.

В ней процессы вычисления выступают игроками, участвующими в формировании общего журнала игры с помощью добавления в него некоторых событий в соответствии с полностью характеризующими  процессы-участники стратегиями — детерминированным частичным функциям из текущего состояния журнала в следующий ход текущего игрока (то есть добавляемый им в конец журнала список событий). Формализации этой модели в виде теорий и тактик, реализованных в системе Coq, наборе композирующих теорем для объединения параллельных уровней абстракции, в том числе выполняющихся в разных потоках и на разных процессорах, и верифицированного компилятора CompCertX (модификации CompCert), поддерживающего потокобезопасную компиляцию и сборку реализаций компонентов ОС.

Таким образом, разработанный набор инструментов поддерживает непрерывную верификацию многоуровневых параллельных частей (уровней) и модулей ОС, реализованных как на языке Си, так и на языке ассемблера. Инструментарий CCAL был успешно использован для разработки непрерывно верифицированного параллельного ядра ОС, основанного на кооперативной многозадачности и использующего мелкозернистые блокировки (fine-grained locking). 

Общий объем спецификаций и доказательств, составляющих инструментарий CCAL, составил около 52000 строк на Coq, соотношение объемов спецификаций и доказательств к объему кода различных компонентов ядра ОС составило от 18 до 70 раз (всего 28000 строк спецификаций и доказательств на 900 строк Си-кода, то есть в среднем около 30 раз).

Различные результаты, полученные в ходе верификации ядра mC2 в рамках проекта, проводимого группой FLINT в Йельском университете, представлены в статьях [77–79]. В статье [76]⁠ представлен основной результат — полностью формально верифицированное относительно сформулированных на высоком уровне абстракции свойств функциональной корректности ядро ОС общего назначения, использующее мелкомасштабные блокировки. 

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

Всё ядро состоит из более чем 25 модулей (из которых 16 модулей самого ядра и 9 драйверов), формализованных на 5 и более уровнях абстракции. Реализация ОС написана с использованием языков Си и ассемблера с использованием их формализаций в рамках верифицированного компилятора CompCert. Общий объем Си-кода ядра составил 6500 строк, спецификация оборудования укладывается в 943 строк формализации в системе Coq, а спецификация программного интерфейса ОС — в 450. Промежуточные спецификации и доказательства составляют вместе около 100 тыс. строк на Coq, но по крайней мере треть из них является избыточной, являясь либо результатом автоматизированной генерации, либо копирования с небольшими изменениями.

В целом работа показала возможность и реальность создания сертифицированных параллельных ядер ОС (в отличие от ранее существующих сертифицированных ядер без параллелизма, таких как SeL4).

В статье [78]⁠ представлено расширение верифицированной ОС CertiKOS, основанной на кооперативной многозадачности, и соответствующего инструментария для поддержки верификации драйверов устройств, поддерживающих такие нелокальные эффекты как прерывания.

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

Разработанные модели и методы верификации были реализованы в системе Coq, и с их помощью существующее верифицированной ядро CeriKOS было расширено двумя видами верифицированных драйверов устройств — драйверами устройств, подключаемых по последовательному порту, спецификация которых основана на соответствующей модели, и драйверами двух программируемых контроллеров прерываний: IOAPIC (I/O Advanced Programmable Interrupt Controller) и LAPIC (Local Advanced Programmable Interrupt Controller).

В целом использованный в данной статье подход основан на общей концепции сертифицированных уровней, использованной при верификации CertiKOS. Сертифицированный уровень состоит из тройки (L1, M, L2) и формального доказательства, показывающего, что реализация уровня M, использующая интерфейс со спецификацией L1 (являющийся основанием уровня, underlay)  является контекстуальным уточнением интерфейса самого уровня — L2 (его оболочки, overlay). L2 также называется глубокой спецификацией (deep specification) уровня и соответствующего ему модуля реализации M, так как эта спецификация полностью охватывает все наблюдаемые извне свойства модуля M, которые в дальнейшем используются для доказательства свойств других модулей системы. 

Основная проблема, решаемая авторами данной работы, заключалась в том, что основная часть (сердцевина, core) ядра CertiKOS доказана для параллелизма с кооперативной многозадачностью. Она предоставляет процессам-участникам существенно более сильные гарантии изоляции, чем параллелизм с вытесняющей многозадачностью, и таким образом, существующие доказательства корректности реализации ядра не могут быть непосредственно использованы для доказательства корректности расширенной системы, содержащей код драйверов, поддерживающий асинхронные аппаратные прерывания. В исходной системе CertiKOS взаимодействие с устройствами может осуществляться только с помощью синхронных операций чтения/записи и таким образом, асинхронное изменение состояния устройства является ненаблюдаемым с точки зрения ОС, а взаимодействие с этим состоянием может быть формализовано в рамках кооперативной многозадачности. 

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

В парадигме CertiKOS драйвер как расширенное устройство,  представляет собой сертифицированный уровень с основанием — моделью прерываний  конкретной архитектуры, и оболочкой — абстрактной моделью прерываний, используемой при верификации других частей и драйверов CertiKOS. 

В целом в рамках данной работы к коду, спецификациям и доказательствам CertiKOS было добавлено около 20 тыс. строк кода, на что потребовалось 7 человеко-месяцев разработки. В ходе проекта было найдено две ошибки в существующих реализациях драйверов, одна из которых приводила к потере данных в буфере драйвера консоли.

В статье [79, 80] представлен новый метод формальной верификации свойств изоляции потоков данных для многоуровневых программных систем, реализация которых включает код как на языке Си, так и на языке ассемблера. Метод основан на использовании общего понятия функции наблюдения (observation function), введение которого позволяет определить концепты спецификации политики безопасности, неразличимости состояний и различных отношений между трассами выполнения (гиперсвойств) в рамках унифицированной парадигмы.

Авторы статьи показывают, как использовать различные функции наблюдения на различных уровнях абстракции и как объединять соответствующие доказательства свойств безопасности с помощью отношений симуляции, доказуемо сохраняющих неразличимость состояний в соответствии с функциями наблюдения. С помощью предложенного метода, реализованного в виде расширения инструментария CertiKOS, было проведено непрерывное доказательство свойств безопасности нетривиального ядра ОС, содержащего как код на языке Си, так и ассемблерный код (доказательство свойств было проведено в предположении отсутствия межпроцессного взаимодействия (IPC)). 

Общий объем доказательств изоляции данных пользовательских процессов в отсутствии IPC для всех примитивов (системных вызовов), поддерживающихся CertiKOS составил около 6 тыс. Строк на Coq, их которых около 2 тыс. — общая часть, формализующая основные понятия и теоремы используемого метода.

Статья [80] подробно рассматривает процесс верификации реализации одного из примитивов синхронизации, используемых в CertiKOS — спин-блокировки Меллора-Крамми и Скотта (MCS-блокировка, MCS-lock). Реализация этой блокировки — совсем небольшая, но весьма сложная как с точки зрения спецификации, так и с точки зрения реализации. Блокировка обеспечивает процессы-участники дополнительными гарантиями очередной упорядоченности ожидающих процессов и масштабируемости в смысле накладных расходов на использование блокировки такого типа при синхронизации процессов, выполняющихся на большом количестве процессорных ядер. 

В статье описывается применение метода сертифицированных уровней абстракции для верификации контекстуального уточнения высокоуровневых спецификаций функций захвата и освобождения блокировки их реализацией с использованием языков Си и ассемблера. Для верификации MCS-блокировки используется 6 уровней абстракции — базовый уровень машинной архитектуры и процессорных команд (включая модельные команды, которые оперируют с модельным состоянием и не имеют физической реализации), уровень примитивных операций с памятью, уровень моделирования интерливинга и межпроцессорного взаимодействия, уровень функциональных спецификаций, привязанных к коду реализации, уровень абстракции структур данных и модельного состояния и уровень целевой функциональной спецификации свойств атомарности и живучести. 

Общий объем спецификации и доказательств примерно в 30 раз превысил объем исходного кода реализации в этой работе (8800 строк на 287 строк реализации). В результате был получен набор формально специфицированных функций блокировки, полностью готовых к интеграции с остальными частями CertiKOS.

Итоговые результаты проекта по верификации ядра CertiKOS с различными расширениями представлены в статье [77]⁠. Статья объединяет и представляет результаты описанных работ DDE field и [80].

Статьи [77, 80, 81] представляют метод формализации спецификаций императивных функций высокого порядка, то есть функций, использующих реализации других функций, передаваемых в качестве параметров или элементов состояния (например, в виде функциональных указателей), и реализованных на императивных языках. 

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

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

В то же время исследование не содержит существенных по объему примеров использования предложенного в ней метода.

В работе [82]⁠ представлены результаты проекта по формальной верификации коммерческого микроядра встроенной ОС реального времени μC/OS-II, с вытесняющей многозадачностью и поддержкой многоуровневых прерываний. Корректность ядра была формализована и доказана в виде отношения контекстуального уточнения между низкоуровневой реализацией системы на языке Си и высокоуровневой спецификацией с использованием доменно-специфичного языка, основанного на параллельной сепарационной логике (Concurrent Sepataion Logic, CSL). Как семантика использованного фрагмента языка Си, так и семантика конструкций языка спецификации, а также все остальные использованные в работе формализмы были разработаны в системе Сoq и хотя и являются достаточно общими и допускают повторное использование, не основаны ни на каком существующем инструментарии для верификации Си-программ и не привязаны к семантике какого-либо конкретного компилятора. Таким образом, работа представляет собой пример не полностью непрерывной верификации с помощью глубокого погружения. 

Основное новшество работы — формализация в виде контекстуального уточнения и верификация реализации интерфейса ОС реального времени с вытесняющей многозадачностью. Помимо контекстуального уточнения, включающего в себя все базовые свойства безопасности (изоляцию процессов, отсутствие неопределенного поведения и т.д.), для подсистемы управления процессам было также доказано свойство отсутствия обратных вытеснений (priority-inversion-freedom), то есть ситуаций, когда процесс с высоким приоритетом неявно вытесняется в результате некоторых действий процессов с более низким приоритетом. 

В рамках проекта была формализована семантика подмножества языка Си, расширенного специально подобранными примитивами, соответствующими последовательностям ассемблерных инструкций, необходимых для реализации планировщика процессов, обработчиков прерываний и примитивов синхронизации. Спецификации семантики системных вызовов были формализованы на высоком уровне с использованием трасс абстрактных событий, содержащих действия планировщика процессов, обработчиков прерываний и проверочные утверждения в параллельной сепарационной логике, расширенной предикатами соответствия представлений (representation predicates), формализующих абстракцию данных в памяти, а также состоянием флагов прерываний. Доказательство производилось с использованием отношения симуляции, формализующего отношение уточнения между трассами выполнения, а также правил вывода, формализующих низкоуровневую семантику выбранного подмножества Си (и ассемблера). 

Для ускорения доказательства были разработаны специфичные тактики (на языке Ltac системы Сoq), которые позволили сократить отношение объема кода доказательств в исходному коду системы до 26:1.  Общий объем формализации составил около 200 тыс. строк формализации в системе Coq, из которых 76 тыс. приходится на базовый логический инструментарий (семантика языка Си, машинной архитектуры, логик, используемых для спецификации,  а также тактики), около 100 тыс. на микроядро и 34 тыс. на модули, такие как реализация примитивов межпроцессного взаимодействия (IPC) и примитивов синхронизации пользовательских процессов.

В статье [83]⁠ представлен инструментарий PEDANTIC для верификации Си-подобных программ с помощью глубокого погружения в систему Coq, спецификаций на основе сепарационной логики и специально разработанных тактик для доказательства соответствия кода спецификациям с помощью символьного выполнения. В состав инструментария входит формализация фрагмента сепарационной логики с помощью глубокого погружения в язык Gallina (основной язык программирования системы Coq), набор специально разработанных сепарационных предикатов для выражения отношения взаимной адресации (по указателю) между структурами данных в памяти, набор тактик для объединения и упрощения предикатов, описывающих состояние памяти программы в ходе ее символьного исполнения, а также интерфейс для расширения инструментария новыми сепарационными предикатами. 

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

В работе [83, 84]⁠ разработан инструментарий для доказательства корректности параллельных императивных программ, основанный на методе Owicki-Gries (OG) для параллельных программ над общей памятью. Метод OG предусматривает аннотацию каждого атомарного действия каждого параллельного процесса одним предикатом предусловия, который должен являться инвариантом относительно каждого потенциально возможного (при выполнении соответствующих предусловий) атомарного действия любого другого процесса. 

Инструментарий объединяет ранее созданную формализацию метода OG в системе Isabelle/HOL в рамках библиотеки Hoare-Parallel с существующей обобщенной формализацией семантики императивных языков программирования в библиотеке SIMPL. В рамках работы синтаксис и семантика SIMPL были расширены примитивами, формализующими параллельную композицию и синхронизацию.

Также была разработана и верифицирована система правил вывода (программная логика) для конструкций расширенного языка, включающая поддержку сложно формализуемых возможностей, таких как экстренное завершение. Разработанная система правил поддерживает вызовы функций, однако их семантика, в отличие от классической логики Хоара, — встраивающая, при которой вместо функции при верификации подставляется ее аннотированная по методу OG реализация. Для поддержки рекурсивных функций, однако, вызов функции также сопровождается сохранением и восстановлением текущего состояния локальных переменных. Также правила вывода предусматривают возможность задания нескольких различных аннотаций по методу OG для одной и той же функции, одна из которых может быть явно выбрана в точке вызова. 

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

Таким образом, был получен новый инструментарий COMPLX для верификации параллельного низкоуровневого императивного кода по методу OG, наследующий возможности библиотеки SIMPL, такие как обработка исключений, вызовы функций и экстренное завершение.

В статье [85] представлены промежуточные результаты разработки современного безопасного загрузчика Syracuse Assured Boot Loader Ex-ecutive (SABLE). Безопасный загрузчик реализует вычисление контрольных хеш-сумм исполняемого кода, сверку этих сумм с заранее предоставляемой базой доверенных значений, а также предоставляет загруженному позднее (доверенному) программному обеспечению, а также удаленным пользователям, возможность убеждаться в целостности системы на основе ее журнала сохраненных контрольных сумм и специального регистра конфигурации. Также безопасный загрузчик должен следовать специальным протоколам взаимодействия с оборудованием и аппаратным безопасным загрузчиком общего назначения.

Представленный в работе безопасный загрузчик реализован на языке Си и для его верификации был применен подход, ранее использованный при формализации и верификации ОС SeL4. Си-код транслируется в глубоко погруженное в систему Isabelle/HOL представление С-SIMPL, формализующее операционную семантику языка Си. Затем с помощью инструмента AutoCorres для глубоко погруженных представлений кода Си-функций генерируются соответствующие неглубоко погруженные представления в виде обычных тотальных функций HOL в специальной монаде, моделирующей состояние кучи и возможность экстренного завершения. 

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

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

Так как безопасный загрузчик, разрабатываемый в рамках данной работы, в своей функциональности существенно опирается на примитивы, предоставляемые конкретной аппаратурой, авторы предложили производить его верификацию, начиная с корня дерева вызовов функций, так как большая часть неглубоко расположенных вызовов имеет семантику, достаточно независимую от конкретной аппаратуры. Реализации функций, семантика которых существенно зависит от работы аппаратуры, на представленном в статье этапе работы не верифицируются, а их спецификации используются как доверенные. В дальнейшем предполагается минимально необходимое расширение спецификации семантики языка SIMPL с целью формализации семантики взаимодействия с аппаратурой. Только после этого станет возможным доказательство абстрактных свойств безопасности всей загруженной системы на уровне реализации загрузчика.

Тем не менее, авторы статьи утверждают на основании предыдущего опыта верификации реализации ОС SeL4, что большая часть реальных ошибок обнаруживается на этапе доказательства соответствия поведения автоматически построенных инструментом AutoCorres моделей реализации Си-функций их абстрактным моделям. В частности, при верификации SeL4, в ходе доказательства соответствия между абстрактными моделями и реализацией было обнаружено 150 ошибок в модели и 144 в реализации, в то время как при доказательстве абстрактных свойств безопасности не было обнаружено никаких новых ошибок. Таким образом, в данной работе авторы представляют промежуточные результаты доказательства соответствия, в ходе которых пока не было обнаружено новых ошибок.

Статья [86] от той же группы разработчиков описывает процесс верификации модуля выделения памяти (heap allocator) для безопасного загрузчика SABLE. При верификации был использован подход, аналогичный общему подходу к верификации SeL4 и самого загрузчика SABLE. Однако в отличии от большей части кода загрузчика, для верификации потребовались доказательства утверждений о низкоуровневом, нетипизированном представлении кучи. Соответствующие утверждения трудно непосредственно переиспользовать для кода, работающего с типизированным представлением кучи.

Чтобы избежать необходимости проводить доказательство строго типизированного кода на нетипизированной куче, в язык аннотаций инструмента C-Parser, генерирующего представление С-SIMPL, и в инструмент AutoCorres была добавлена поддержка модельной операции «перетипирования» участка памяти. Она обрабатывается вместе с остальными инструкциями в исходном Си-коде программы и имеет свою спецификацию и правило вывода в логике Хоара, семантика которого соответствует доказуемо корректному преобразованию модели нетипизированного участка памяти в типизированный с явным указанием типа и размера. Таким образом, после каждой операции выделения памяти модельное типизированное состояние памяти восстанавливается (вычисляется) и дальнейшее доказательство может проводиться на типизированном уровне. 

В рамках данной работы, однако, была доказана лишь достаточно слабая спецификация функций выделения и освобождения памяти, которая оставляет за рамками рассмотрения статически выделенную память, а также  свойства непересечения вновь выделенных объектов с ранее выделенными объектами того же типа. Тем не менее, в результате верификации в модуле выделения памяти были найдены 2 критические ошибки.

В работе [87]⁠ представлен инструментарий CSimpl (от Concurrent-SIMPL, в отличие от C-SIMPL, в котором буква «C» соответствует языку Си), который, как и COMPLX, является расширением инструмента SIMPL для верификации параллельных программ. Однако, в отличие от COMPLX, основанного на чистом методе OG, СSimpl основан на методе Rely-Guarantee (RG), в котором для доказательства корректности параллельной системы каждому процессу требуется спецификация всего из четырех предикатов — предусловия-инварианта (pre), постусловия (post), ограничения на действия системы (rely) и ограничения на действия процесса (guarantee). 

В отличие от чистого метода ОG, в RG не требуется непосредственная аннотация каждого атомарного действия своим предусловием; эти предусловия выводятся автоматически по индуктивным правилам вывода в соответствии с семантикой языка программирования из одного общего предусловия-инварианта, который должен согласно этим правилам вывода преобразовываться в предусловие любого действия соответствующего потока. Кроме этого RG поддерживает композиционную верификацию процессов и композиционное правило вывода для вызовов функций, так как инвариантность  всех внутренних предусловий вызываемой функции гарантируется инвариантностью ее  предусловия-инварианта и семантической структурой самой функции. Эти особенности существенно улучшают масштабируемость метода верификации и позволяют применять его к коду программ среднего размера, в том числе, к фрагментам реализаций коммерческих программных систем. 

Представленный в данной статье инструмент CSimpl включает формализацию правил вывода, поддерживающих расширение языка Simpl  конструкцией Await, соответствующей синхронизации по значению общих переменных. Параллельная композиция допускается только на уровне целых процессов и не может быть вложена в другие конструкции языка. Правила вывода для расширенного языка CSimpl верифицированы относительно общего определения валидности в подходе RG, опирающегося на определение параллельного вычисления. 

В отличие от формализации общего метода RG в рамках библиотеки HoareParallel, которая также опирается на определение параллельного вычисления и является достаточно компактной (общий объем формализации метода RG — 2300 строк на Isabelle), формализация представленного в данной статье инструментария (RG с правилами вывода для языка CSimpl) включает более 13000 строк формализации в Isabelle/HOL. 

Данная работа содержит экспериментальное применение разработанного инструментария, хотя разработанный инструментарий не включает генератор условий верификации для автоматизированного применения формализованных правил вывода. В апробации демонстрируется верификация абстрактной модели сервиса пересылки сообщений, предоставляемого микроядром XtratuM. В рамках эксперимента доказана корректность операций добавления и удаления сообщений из очередей соответствующих процессов, а также отсутствие переполнений этих очередей. Общий объем потребовавшихся для этого формализаций и доказательств составил около 3500 строк в Isabelle/HOL. 

Так как инструментарий расширяет язык SIMPL, его генератор условий верификации может применяться для доказательства некоторых фрагментов спецификации на языке CSimpl с последовательной семантикой. Кроме этого, существующий инструментарий C-SIMPL, формализующий семантику конструкций языка Си в рамках инструмента SIMPL, может быть интегрирован с расширенным инструментом для верификации параллельных Си-программ.

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

Статья [88]⁠ тех же авторов представляет существенное расширение предыдущей работы не только для верификации реалистичных Си-программ, но и реактивных систем с несколькими наборами обработчиков событий. Основная проблема, решаемая в данной статье — сложность формализации параллельных реактивных систем, обладающих двумя уровнями недетерминизма: недетерминизмом возникновения в системе асинхронных событий и запуска процессов их обработки и недетерминизмом интерливинга между работающими процессами, обрабатывающими текущие события. 

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

Опираясь на такой подход, авторы статьи разработали каркас PiCore для конкретных формализаций метода RG, который позволяет конструировать инструментарий для верификации реактивных параллельных систем на основе существующих формализаций метода RG для конкретных языков программирования. Каркас включает в себя определение параллельной семантики взаимодействия обработчиков событий, систему правил вывода для комбинирования доказательств по методу RG для отдельных событий, специальную теорему для доказательства сохранения инвариантов данных для всей системы в целом, а также явно сформулированный интерфейс для подключения формализаций конкретных языков программирования, реализованный в виде локали в системе Isabelle/HOL. Интерфейс каркаса состоит из 9 сущностей, таких как отношение переходов по окружению, отношение переходов между атомарными действиями программы, множество возможных вычислений, правило вывода контракта по методу RG и другие, а также из 10 условий консистентности, которым должны удовлетворять заданные сущности. 

Соответствующие определения сущностей и доказательства условий консистентности были проведены авторами статьи для двух языков формализаций языков программирования — CSimpl, ранее разработанного расширения семантики языка SIMPL и инструмента C-SIMPL для поддержки верификации  по методу RG, и IMP — минимального модельного языка программирования, для которого была определена параллельная семантика по методу RG.

Формализация параллельной семантики IMP была апробирована на примере низкоуровневой точной модели параллельно работающих функций выделения и освобождения памяти в ОС реального времени Zephyr. Объем исходного кода реализаций всех функций на языке Си составил около 400 строк, совокупный объем  спецификаций и доказательств — около 17600 строк, в 40 раз больше исходного кода реализации. В процессе верификации было обнаружено 3 ошибки в коде реализации управления памятью, 2 из которых являются критическими и были исправлены разработчиками в последних релизах ОС Zephyr. 

Таким образом, в статье представлен инструментарий для верификации реактивных параллельных систем с помощью взаимодействия схем событий и подхода RG, который применим к точным низкоуровневым моделям модулей реальных ОС, но на практике, возможно, не непосредственно к исходному коду этих модулей, так как для верификации не использовалось инстанцирование каркаса PiCore языком CSimpl для более точного моделирования семантики языка Си.

В статье [89] более подробно описан процесс верификации подсистемы распределения динамической памяти ОС реального времени Zephyr. Подсистема использует выделение памяти по методу близнецов, в котором память рекурсивно разбивается на пары блоков с экспоненциально убывающей длиной, которые затем могут вновь объединяться парами при освобождении двух рядом расположенных блоков. Блоки одинакового размера представляют из себя уровень, для которого хранится список свободных блоков. Блоки могут не только быть занятыми или свободными, но так же находиться в процессе разбиения или слияния в момент вызова функции выделения памяти, так как во время разбиения и слияния блоков разрешены переключения контекста и операции с не занятыми в процессе разбиения или слияния блоками памяти. Таким образом, процесс, выполняющий в данный момент функцию выделения или освобождения памяти, может быть прерван как процессом, также выполняющим в данный момент функцию выделения или освобождения памяти, так и процессом, вновь вызвавшим такую функцию и, следовательно, множество процессов, участвующих в интерливинге, не детерминировано и меняется в ходе работы системы.  

В рамках каркаса PiCore такой недетерминизм моделируется как двухуровневый интерливинг, когда каждый отдельный процесс представляется как последовательная композиция  недетерминированно вызываемых событий (таких как выполнение выделения памяти, выполнение освобождения памяти, выполнение пользовательского кода), а система в целом представляет собой интерливинг таких последовательных композиций. При этом каркас предоставляет верифицированные правила вывода для корректного построения последовательных и параллельных композиций по методу RG. 

В рамках работы по верификации распределения памяти в ОС Zephyr участки кода, где в реализации обработчиков событий в Си-коде используются блокировки  прерываний, моделировались как атомарные операции. В остальном модели реализаций точно следуют исходному Си-коду и допускают возможность переключения контекста там, где это должно быть возможно с точки зрения семантики соответствующих операций. Тем не менее, модель кода делает существенные упрощения, используя высокоуровневое представление структур данных в виде записей Isabelle/HOL и игнорируя, например, условия корректности работы с памятью ядра в самой реализации обработчиков и семантику арифметики с ограниченными целыми.

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

Неглубокое погружение при выполнении аналитической верификации

Следует отметить, что ранее рассмотренные работы [85] и [86]⁠ по сути используют в большей степени неглубокое, чем глубокое погружение, так как несмотря на то, что исходно Си-программа погружается в теорию Isabelle/HOL глубоко в виде конструкции синтаксического дерева в представлении C-SIMPL, целевые доказательства проводятся не на глубоко погруженной модели, а на монадическом представлении, генерируемом инструментом AutoCorres, который очень близок к неглубокому погружению исходной программы.

AutoCorres был разработан в рамках проекта по верификации SeL4 с целью облегчения доказательства соответствия кода функций реализации ОС соответствующим им высокоуровневым моделям. Он автоматически генерирует монадические представления погруженных функций, а также доказательства их семантического соответствия исходным моделям в представлении C-SIMPL. Тем не менее, представление AutoCorres имеет некоторую избыточную глубину по сравнению с наиболее типичным для Isabelle/HOL подходом к монадическому заданию определений функций; в частности, для представления циклов используются специально разработанные комбинаторы вместо входящих в состав самого Isabelle/HOL пакетов, обычно используемых для задания определений функций. 

Это несколько осложняет доказательство сложных функций, так как препятствует эффективной декомпозиции доказательства, сводя обработку всех специальных комбинаторов к одному вызову генератора условий верификации (тактики wp, генерирующей условия верификации с помощью вычисления слабейших предусловий). Всё дальнейшее доказательство после вызова тактики представляется в виде набора подцелей в рамках одной леммы, в результате чего смешиваются большое число совершенно разных условий верификации, относящихся к различным участкам исходного кода, среди которых есть как существенно сложные, так и тривиальные. Кроме этого, в силу использования генератором условий верификации wp-правил в логике Хоара, такой подход осложняет формулировку утверждений о связях между различными состояниями выполнения участка программы. Как утверждения, так и доказательства, относящиеся к функциям, определяемым непосредственно (неглубоко) в рамках самого Isabelle/HOL, обычно не требуют использования специальных логик. Именно такие функции используются в подходах, основанных на неглубоком погружении, а также экстракции и кодогенерации (например, в рамках инструментария Imperative-HOL/SepRef). 

Подходы, основанные на неглубоком погружении, наиболее очевидным образом реализуются для языков программирования, имеющих семантику, изначально близкую к денотационной, таким как Haskell, а также существенные фрагменты языков Scala или Rust.

Выводы

Представленные работы демонстрируют, что для формальной верификации крупных программных систем наиболее эффективными оказываются подходы дедуктивной верификации с использованием нотации ACSL и инструментария Frama-С и аналитической верификации с неполным погружением на основе Isabelle/HOL. Нотация ACSL представляет собой язык, удобный для записи и верификации программных контрактов в частности для программ на языке Си. А инструменты Isabelle/HOL предоставляют больше возможностей по автоматизации и снижению трудоемкости, чем Coq.

Интеграция инструментов верификации и тестирования

Задача интеграции различных инструментов верификации, включая инструменты тестирования, при верификации сложных программных систем обсуждалась подробно в работе [90]. Ниже приведены выводы, полученные в рамках данной работы.

Размеры и сложность современного программного обеспечения (ПО) обычно не позволяют провести верификацию достаточно высокого качества. Это связано как с большим количеством разнородных функций и компонентов, входящих в типичную программную систему, так и с практическими ограничениями самих применяемых технологий верификации. Подобные ограничения в первую очередь касаются формальных методов верификации, дающих самые надежные гарантии корректности верифицированных систем. Причины таких ограничений разнообразны – это могут быть низкая выразительность или, наоборот, чрезмерная усложненность формального аппарата, лежащего в основе метода, ограниченность конкретных инструментов, а также, что является на практике важнейшим фактором, сложность, высокая стоимость и длительность выполнения самих формальных методов верификации. Интеграция различных формальных методов верификации является перспективным подходом к решению проблемы преодоления таких ограничений. На практике бывает важно совместить результаты верификации различных компонентов сложной системы, проведенные разными командами с помощью различных техник. Другая часто встречающаяся задача - найти приемлемую комбинацию методов и технологий верификации, которые позволяют проверить всю систему в целом и, одновременно, сфокусировать усилия на отдельных, наиболее критических компонентах и функциях, используя в их верификации наиболее строгие, но и более сложные и дорогостоящие методы. В данной работе рассматривается вторая задача применительно к ядру операционной системы как к системе с повышенными требованиями по показателям надежности и корректности. 

При решении задач интеграции методов верификации просматривается как минимум два аспекта. Первый – это повторное использование (reuse) артефактов верификации и возможностей инструментов разных технологий, которые применялись к одним и тем компонентам проверяемой системы. Второй – это стыковка процессов верификации взаимодействующих компонентов, каждый из которых в отдельности верифицировался при помощи разных методов и инструментов, и увязывание получаемых при этом артефактов. Проблемы интеграции методов верификации и, в частности, формальных методов рассматриваются исследовательским сообществом достаточно давно - международная конференция по интеграции формальных методов проводится уже с 1999 года [91]. Пожалуй, наибольшим продвижением в этом направлении можно назвать широкое использование инструментов поиска решений систем логических утверждений, так называемых решателей (solvers), таких как Z3, CVC4 и др., в рамках различных технологий верификации. Они успешно применяются как компоненты многих инструментов динамической верификации (например, SpecExpolrer, Pex, SAGE), инструментов верификации программ с извлечением их моделей (software model checking, например, BLAST, Static Driver Verifier, CPAchecker), а также инструментов дедуктивной верификации (например, Frama-C, Rodin). Авторы тоже обращались к теме интеграции методов верификации в нескольких работах, например в [92] и [93]. В данной статье рассматривается еще одно направление интеграции, которому ранее не уделялось должного внимания. Анализируя публикации на тему интеграции формальных методов, авторы приходят к выводу, что наиболее активно разрабатывается тема интеграции подходов, построенных на различных формализмах моделирования поведения. Задача собственно стыковки самих методов рассматривается на примерах частных приложений. Авторы считают, что есть еще одно измерение интеграции, на которое следует обратить внимание, – это комплексная верификация некоторого важного класса систем, обладающих специфическими особенностями архитектуры и имеющих некоторую общую область характеристик функциональности, определяющую их назначение и являющуюся по существу объектом анализа в ходе верификации. В рассматриваемой статье в качестве такого класса систем рассматриваются операционные системы, в более узком смысле – ядра операционных систем. 

В данном исследовании авторы опираются на опыт, полученный в многочисленных проектах по верификации программного и аппаратного обеспечения за последние 20 лет работы в отделе Технологий программирования ИСП РАН. Коротко перечислим эти проекты. Начнем с тех, которые базировались на использовании одного вида формальных методов, а затем перейдем к проектам, где проводились эксперименты с синтезом различных подходов.

Первые проекты полностью опирались на тестирование на основе формальных моделей (model based testing, MBT). В них были использованы следующие формализмы для представления моделей [94]:

В этих проектах было проведено промышленное тестирование нескольких операционных систем, включая ОС Linux и отечественные операционные системы реального времени, оптимизирующего компилятора компании Intel, некоторых компонентов информационной инфраструктуры компании крупного телекоммуникационного оператора, моделей отечественных микропроцессоров. В рамках данных проектов решался следующий типовой набор задач, связанных с построением соответствующих компонентов верифицирующей (в данном случае тестовой) системы:

Следующая группа проектов использовала технику проверки программных моделей (software model checking). Верифицируемой системой в данном случае являлись компоненты ядра ОС Linux, в первую очередь, драйвера устройств [95, 96]. В рамках этих проектов типовой состав работ был таков:

Еще одна группа проектов связана с использованием дедуктивной верификации [95]. Проверяемой системой в данном случае является система защиты информации (СЗИ) ОС AstraLinux. В рамках этой группы проектов проводилась верификация модели требований к СЗИ, в качестве такой модели была использована мандатная сущностно-ролевая модель доступа и потоков данных (МРОСЛ ДП), а затем нужно было провести верификацию кода модуля безопасности ядра ОС Linux (Linux Security Module, LSM). В рамках этих проектов решались следующие задачи.

Заметим, что здесь работы с моделью и модулем LSM рассматриваются совместно, так как между этими объектами верификации много концептуально близкого – они описывают механизмы обеспечения контроля доступа к информации. Однако модель и модуль реализованы на разных языках (Event-B и C) и верифицируются разными инструментами (Rodin и Frama-C/Jessie/Why3). Кроме того, в части интерфейсов модель и модуль не совпадают.

Помимо различия в используемых языках и инструментах, задачи верификации модели СЗИ и модуля LSM существенно отличаются друг от друга тем, что модель представляет на соответствующем уровне абстракции целевую систему в целом, а LSM лишь часть ядра ОС, ответственную за выполнение проверок при обращениях к ней других компонентов ядра. Это означает необходимость, помимо решения других задач, описать формально предположения о поведении окружении модуля (т.е., ядра и всех приложений в целом, по отношению к вызовам операций модуля), без таких предположений невозможно верифицировать сам модуль. Отметим, что корректность таких предположений тоже надо проверять, то есть верифицировать. 

В выделенных списках работ в каждой из трех рассмотренных групп можно отметить работы, нацеленные на решение одних и тех же задач, хотя пока, в силу технических различий между инструментами верификации, их приходится решать по-разному. Авторы разместили схожие задачи в приведенной ниже таблице. Всего получилось пять групп. 

Группы задач Тестирование на основе моделей Проверка моделей Дедуктивная верификация
Определение программного контракта  Построение спецификаций программного контракта (тесно связано с построением тестовых оракулов)  Формализация правил взаимодействия компонентов программной системы Построение формальных спецификаций операций и типов данных в форме программных контрактов 
Построение модели окружения Построение модели тестового сценария Генерация модели окружения Формальное описание предположений о поведении окружения проверяемого модуля
Построения пути, демонстрирующего ошибку Выполнение обхода сценарного автомата, генерация тестовых данных для всех воздействий Генерация и решение верификационных задач Задача не ставилась
Увязка уровней абстракции Построение отображения реализационных событий и данных в модельные Задача не ставилась Задача не ставилась
Оценка полноты верификации

Определение метрик полноты тестирования и построение системы сбора и анализа достигнутого тестового покрытия

Сбор информации о проанализированных путях в графе потока управления системы Задача не ставилась

На основании сказанного можно выделить узлы, в которых различные методы и реализующие их инструменты имеют возможные точки сопряжения. Примерами таких точек могут быть следующие артефакты: 

Выводы

Представленные работы демонстрируют, что задача разработки и верификации формальных многоуровневых моделей и верификации на соответствие им программных реализаций может быть успешно решена. Наиболее перспективными с точки зрения разработки и верификации многоуровневых моделей представляются формальные методы B и Event-B, с точки зрения удобства разработки и верификации программных контрактов – язык ACSL и инструментарий Frama-C, а наилучшим выбором для аналитической верификации сложных программ и доказательства их соответствия модели Isabelle/HOL. Наилучшей базой для интеграции методов тестирования и аналитической верификации является использование методов тестирования на основе формальных моделей или MBT. Этот же подход позволяет строить тесты на основе многоуровневых спецификаций. 

Готовых решений, которые позволяют верифицировать и тестировать системы на основе многоуровневых спецификаций в условиях промышленного производства программ пока нет, по этой причине, задачи поставленные в данном проекте, следует признать актуальными.

Литература

  1. Black PE, Badger L, Guttman B, Fong E (2016) Dramatically reducing software vulnerabilities: Report to the White House Office of Science and Technology Policy
  2. Black PE, Ribiero A (2016) SATE V Ockham Sound Analysis Criteria
  3. RU2682003C1 - СПОСОБ ВЕРИФИКАЦИИ ФОРМАЛЬНОЙ АВТОМАТНОЙ МОДЕЛИ ПОВЕДЕНИЯ ПРОГРАММНОЙ СИСТЕМЫ - Яндекс.Патенты. https://yandex.ru/patents/doc/RU2682003C1_20190314. Accessed 25 Dec 2019
  4. Leroy X (2009) Formal verification of a realistic compiler. Communications of the ACM 52:107
  5. Klein G, Norrish M, Sewell T, et al (2010) seL4: formal verification of an operating-system kernel. Communications of the ACM 53:107
  6. Kanav S, Lammich P, Popescu A (2014) A Conference Management System with Verified Document Confidentiality. Computer Aided Verification 167–183
  7. Kumar R, Myreen MO, Norrish M, Owens S (2014) CakeML: a verified implementation of ML. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’14 179–191
  8. Myreen MO, Davis J (2014) The Reflective Milawa Theorem Prover Is Sound. Interactive Theorem Proving 421–436
  9. Kumar R, Arthan R, Myreen MO, Owens S (2016) Self-Formalisation of Higher-Order Logic. Journal of Automated Reasoning 56:221–259
  10. Chen H, Ziegler D, Chajed T, et al (2015) Using Crash Hoare logic for certifying the FSCQ file system. Proceedings of the 25th Symposium on Operating Systems Principles - SOSP ’15
  11. Hawblitzel C, Howell J, Kapritsos M, et al (2015) IronFleet: proving practical distributed systems correct. Proceedings of the 25th Symposium on Operating Systems Principles - SOSP ’15 1–17
  12. Mashkoor A, Kossak F, Egyed A (2018) Evaluating the suitability of state-based formal methods for industrial deployment. Software: Practice and Experience 48:2350–2379
  13. Devyanin PN, Khoroshilov AV, Kuliamin VV, et al (2014) Formal Verification of OS Security Model with Alloy and Event-B. Lecture Notes in Computer Science 309–313
  14. Maoz S, Ringert JO, Rumpe B (2011) Semantically Configurable Consistency Analysis for Class and Object Diagrams. Model Driven Engineering Languages and Systems 153–167
  15. Arcaini P, Bonfanti S, Gargantini A, et al (2015) Formal validation and verification of a medical software critical component. 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)
  16. Arcaini P, Gargantini A, Riccobene E (2017) Rigorous development process of a safety-critical system: from ASM models to Java code. Int J Softw Tools Technol Trans 19:247–269
  17. Börger E, Zenzaro S (2015) Modeling for change via component-based decomposition and ASM refinement. Proceedings of the 7th International Conference on Subject-Oriented Business Process Management - S-BPM ONE ’15
  18. Danmin C, Yue S, Zhiguo C (2015) A Formal Specification in B of an Operating System. The Open Cybernetics & Systemics Journal 9:1125–1129
  19. Ren L, Chang R, Yin Q, Wang W (2017) Using the B Method to Formalize Access Control Mechanism with TrustZone Hardware Isolation (Short Paper). Information Security Practice and Experience 759–769
  20. Hussain S, Farid S, Alam M, et al (2018) Modeling of Access Control System in Event-B
  21. Troubitsyna E, Laibinis L, Pereverzeva I, et al (2016) Towards Security-Explicit Formal Modelling of Safety-Critical Systems. Lecture Notes in Computer Science 213–225
  22. Девянин ПН, Ефремов ДВ и др. Моделирование и верификация политик безопасности управления доступом в операционных системах. https://www.ispras.ru/publications/2018/security_policy_modeling_and_verification/. Accessed 27 Dec 2019
  23. Wirth N (1978) Program Development by Stepwise Refinement. Programming Methodology 321–334
  24. The RAISE development method. In: Google Books. https://books.google.com/books/about/The_RAISE_development_method.html?hl=ru&id=aqhQAAAAMAAJ. Accessed 27 Dec 2019
  25. Dalvandi M, Butler M, Rezazadeh A (2017) Derivation of algorithmic control structures in Event-B refinement. Science of Computer Programming 148:49–65
  26. Dalvandi M, Butler M, Rezazadeh A, Fathabadi AS (2018) Verifiable Code Generation from Scheduled Event-B Models. Lecture Notes in Computer Science 234–248
  27. Dalvandi MS, Butler M, Fathabadi AS (2019) SEB-CG: Code generation tool with algorithmic refinement support for Event-B. In: Practical Formal Verification for Software Dependability: co-located with the Formal Methods 2019 (FM’19) (07/10/19)
  28. Vu DH, Truong AH, Chiba Y, Aoki T (2017) Automated testing reactive systems from Event-B model. 2017 4th NAFOSTED Conference on Information and Computer Science
  29. Savary A, Frappier M, Leuschel M, Lanet J-L (2015) Model-Based Robustness Testing in Event-B Using Mutation. Software Engineering and Formal Methods 132–147
  30. Newcombe C, Rath T, Zhang F, et al (2015) How Amazon web services uses formal methods. Communications of the ACM 58:66–73
  31. Kim Y-M, Kang M, Choi J-Y (2017) Formal Specification and Verification of Firewall using TLA +
  32. Methni A, Lemerre M, Ben Hedia B, et al (2015) Verifying and Constructing Abstract TLA Specifications: Application to the Verification of C programs. In: Tenth International Conference on Software Engineering Advances (ISCEA 2015)
  33. Pandey T, Srivastava S (2015) Comparative Analysis of Formal Specification Languages Z , VDM and B
  34. Zafar NA (2016) Formal specification and analysis of take-off procedure using VDM-SL. Complex Adaptive Systems Modeling 4
  35. Divakaran S, D’Souza D, Kushwah A, et al (2015) Refinement-Based Verification of the FreeRTOS Scheduler in VCC. Formal Methods and Software Engineering 170–186
  36. Bowen JP (2001) Z: A Formal Specification Notation. Software Specification Methods 3–19
  37. Knight JC, DeJong C, Gibble MS, Nakano LGM (1997) Why are Formal Methods Not Used More Widely
  38. Clarke EM The Birth of Model Checking. 25 Years of Model Checking 1–26
  39. Godefroid P (2016) Between Testing and Verification: Dynamic Software Model Checking
  40. Karna AK, Chen Y, Yu H, et al (2018) The role of model checking in software engineering. Front Comput Sci 12:642–668
  41. Boulifa RA, Ana C, Maag S (2019) Verifying complex software control systems from test objectives: application to the ETCS system. In: ICSOFT 2019: 14th International Conference on Software Technologies. Scitepress
  42. Wang H, Zhong D, Zhao T (2019) Avionics system failure analysis and verification based on model checking. Engineering Failure Analysis 105:373–385
  43. Hsieh C, Mitra S (2019) Dione: A Protocol Verification System Built with Dafny for I/O Automata. Lecture Notes in Computer Science 227–245
  44. Trindade A, Cordeiro L (2019) Automated formal verification of stand-alone solar photovoltaic systems. Solar Energy 193:684–691
  45. Zhang H, Li G, Cheng Z, Xue J (2018) Verifying OSEK/VDX automotive applications: A Spin-based model checking approach. Software Testing, Verification and Reliability 28:e1662
  46. Cârlan C, Ratiu D, Schätz B (2016) On Using Results of Code-Level Bounded Model Checking in Assurance Cases. Lecture Notes in Computer Science 30–42
  47. Maroneze A, Perrelle V, Kirchner F (2019) Advances in Usability of Formal Methods for Code Verification with Frama-C. Electronic Communications of the EASST 77.: https://doi.org/10.14279/tuj.eceasst.77.1108
  48. Duprat S, Lamiel VM, Kirchner F, et al (2016) Spreading Static Analysis with Frama-C in Industrial Contexts. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016)
  49. Dordowsky F (2015) An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Project. Electronic Proceedings in Theoretical Computer Science 187:28–41
  50. Silva RAB e., Rovedy Aparecida Busquim, Arai NN, et al (2016) Formal Verification With Frama-C: A Case Study in the Space Software Domain. IEEE Transactions on Reliability 65:1163–1179
  51. Ebalard A, Mouy P, Benadjila R (2019) Journey to a RTE-free X.509 parser. In: SSTIC. pp 1–30
  52. Blanchard A, Kosmatov N, Lemerre M, Loulergue F (2015) A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. Formal Methods for Industrial Critical Systems 15–30
  53. Mangano F, Duquennoy S, Kosmatov N (2017) Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study. Lecture Notes in Computer Science 114–120
  54. Peyrard A, Kosmatov N, Duquennoy S, Raza S (2018) Towards Formal Verification of Contiki: Analysis of the AES–CCM* Modules with Frama-C. In: RED-IOT 2018 - Workshop on Recent advances in secure management of data and resources in the IoT
  55. Blanchard A, Kosmatov N, Loulergue F (2018) Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. Lecture Notes in Computer Science 37–53
  56. Furia CA, Nordio M, Polikarpova N, Tschannen J (2017) AutoProof: auto-active functional verification of object-oriented programs. International Journal on Software Tools for Technology Transfer 19:697–716
  57. Becker M, Regnath E, Chakraborty S (2017) Development and Verification of a Flight Stack for a High-Altitude Glider in Ada/SPARK 2014. Lecture Notes in Computer Science 105–116
  58. Lourenco CB, Frade MJ, Nakajima S, Pinto JS (2018) A Generalized Approach to Verification Condition Generation. 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC)
  59. Gurov D, Lidström C, Nyberg M, Westman J (2017) Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report. Lecture Notes in Computer Science 3–18
  60. Nyberg M, Gurov D, Lidström C, et al (2018) Formal Verification in Automotive Industry: Enablers and Obstacles. Lecture Notes in Computer Science 139–158
  61. Zaostrovnykh A, Pirelli S, Iyer R, et al (2019) Verifying software network functions with no verification expertise. Proceedings of the 27th ACM Symposium on Operating Systems Principles - SOSP ’19
  62. Shuja S, Srinivasan SK, Jabeen S, Nawarathna D (2015) A Formal Verification Methodology for DDD Mode Pacemaker Control Programs. Journal of Electrical and Computer Engineering 2015:1–10
  63. Nelson L, Sigurbjarnarson H, Zhang K, et al (2017) Hyperkernel: Push-Button Verification of an OS Kernel. In: Proceedings of the 26th Symposium on Operating Systems Principles. ACM, pp 252–269
  64. Oliveira DB de, de Oliveira DB, Cucinotta T, de Oliveira RS (2019) Efficient Formal Verification for the Linux Kernel. Software Engineering and Formal Methods 315–332
  65. Kosmatov N, Lemerre M, Alec C (2014) A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing. Tests and Proofs 158–164
  66. Petiot G, Botella B, Julliand J, et al (2014) Instrumentation of Annotated C Programs for Test Generation. 2014 IEEE 14th International Working Conference on Source Code Analysis and Manipulation
  67. Petiot G, Kosmatov N, Giorgetti A, Julliand J (2014) How Test Generation Helps Software Specification and Deductive Verification in Frama-C. Tests and Proofs 204–211
  68. Petiot G, Kosmatov N, Botella B, et al (2018) How testing helps to diagnose proof failures. Form Asp Comput 30:629–657
  69. Bardin S, Chebaro O, Delahaye M, Kosmatov N (2014) An All-in-One Toolkit for Automated White-Box Testing. Tests and Proofs 53–60
  70. Bardin S, Kosmatov N, Marre B, et al (2018) Test Case Generation with PathCrawler/LTest: How to Automate an Industrial Testing Process. Lecture Notes in Computer Science 104–120
  71. Beringer L, Petcher A, Ye KQ, Appel AW (2015) Verified correctness and security of OpenSSL HMAC. In: Proceedings of the 24th USENIX Conference on Security Symposium. USENIX Association, pp 207–221
  72. Petcher A, Morrisett G (2015) The Foundational Cryptography Framework. Lecture Notes in Computer Science 53–72
  73. Mansky W, Appel AW, Nogin A (2017) A verified messaging system. Proceedings of the ACM on Programming Languages 1:1–28
  74. Cao Q, Beringer L, Gruetter S, et al (2018) VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. Journal of Automated Reasoning 61:367–422
  75. Xia L-Y, Zakowski Y, He P, et al (2019) Interaction trees: representing recursive and impure programs in Coq. Proceedings of the ACM on Programming Languages 4:1–32
  76. Gu R, Shao Z, Kim J, et al (2018) Certified concurrent abstraction layers. Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI 2018
  77. Gu R, Shao Z, Chen H, et al (2019) Building certified concurrent OS kernels. Communications of the ACM 62:89–99
  78. Chen H, Wu X (newman), Shao Z, et al (2016) Toward compositional verification of interruptible OS kernels and device drivers. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI 2016
  79. Costanzo D, Shao Z, Gu R (2016) End-to-end verification of information-flow security for C and assembly programs. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI 2016
  80. Kim J, Sjöberg V, Gu R, Shao Z (2017) Safety and Liveness of MCS Lock—Layer by Layer. Programming Languages and Systems 273–297
  81. Beringer L, Appel AW (2019) Abstraction and Subsumption in Modular Verification of C Programs. Lecture Notes in Computer Science 573–590
  82. Xu F, Fu M, Feng X, et al (2016) A Practical Verification Framework for Preemptive OS Kernels. Computer Aided Verification 59–79
  83. Roe K, Smith SF (2017) Using the coq theorem prover to verify complex data structure invariants. Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design - MEMOCODE ’17
  84. Amani S, Andronick J, Bortin M, et al (2017) Complx: a verification framework for concurrent imperative programs. Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2017
  85. Constable SD, Sutton R, Sahebolamri A, Chapin S (2018) Formal Verification of a Modern Boot Loader
  86. Sahebolamri A, Constable SD, Chapin SJ (2018) A Formally Verified Heap Allocator
  87. Sanán D, Zhao Y, Hou Z, et al (2017) CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. Tools and Algorithms for the Construction and Analysis of Systems 481–498
  88. Zhao Y, Sanán D, Zhang F, Liu Y (2019) A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. Lecture Notes in Computer Science 161–178
  89. Zhao Y, Sanán D (2019) Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS. Computer Aided Verification 515–533
  90. Петренко АК, Кулямин ВВ, Хорошилов АВ (2015) Об интеграции формальных методов в задачах верификации операционных систем
  91. Araki K, Galloway A, Taguchi K (2012) IFM’99: Proceedings of the 1st International Conference on Integrated Formal Methods, York, 28–29 June 1999. Springer Science & Business Media
  92. Петренко АК (2008) Унификация в автоматизации тестирования. Позиция UniTESK. Труды Института системного программирования РАН 14:
  93. Kuliamin VV (2009) Integration of verification methods for program systems. Programming and Computing Software 35:212–222
  94. Kuliamin V, Petrenko A (2014) Evolution of UniTESK Test Development Technology. Proceedings of ISP RAS 26:9–26
  95. Devyanin PN, Khoroshilov AV, Kuliamin VV, et al (2016) Using Refinement in Formal Development of OS Security Model. Lecture Notes in Computer Science 107–115
  96. Zakharov IS, Mandrykin MU, Mutilin VS, et al (2014) Configurable Toolset for Static Verification of Operating Systems Kernel Modules. Proceedings of ISP RAS 26:5–42