Этап 2

В ходе выполнения проекта по Соглашению о предоставлении субсидии от 27.06.2014 №14.604.21.0051 с Минобрнауки России в рамках федеральной целевой программы «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2014-2020 годы» на этапе №2 в период с 01.01.2015 по 30.06.2015 выполнялись следующие работы:

  1. Разработка метода генерации моделей памяти компонентов операционных систем с возможностью интерпретации участков памяти как объектов разных типов.
  2. Разработка алгоритмов генерации моделей памяти компонентов операционных систем с возможностью интерпретации участков памяти как объектов разных типов.
  3. Разработка метода генерации моделей памяти разделяемой между несколькими потоками управления.
  4. Разработка алгоритмов генерации моделей памяти разделяемой между несколькими потоками управления.
  5. Участие в мероприятиях, направленных на освещение и популяризацию промежуточных и окончательных результатов ПНИ.
  6. Разработка веб-сайта для популяризацию результатов ПНИ.
  7. Идентификация и описание распространённых дисциплин синхронизации при работе с разделяемыми данными в компонентах операционных систем в обеспечение разработки метода генерации условий верификации для программ, работающих с разделяемыми данными.
  8. Подготовка и подача заявок на регистрацию результатов интеллектуальной деятельности.

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

Преимущества предложенных методов относительно других подходов, таких как предложенный в диссертации М.Яника "Automatic Modular Static Safety Checking for C Programs", проявляется при использовании современных SMT-решателей, основанных на алгоритме Дэвиса-Патнема-Логемана-Лавленда (DPLL), эффективная работа которых жизненно необходима для возможности применять методы дедуктивной верификации на практике. В SMT-решателях обычно каждая поддерживаемая логическая теория реализуется отдельно и связь между теориями устанавливается за счет обмена дизъюнкциями предикатов, среди которых только равенства интерпретируются всеми участвующими теориями. Из этого следует, что, чаще всего, логические предикаты и функции, требующие применения одновременно сразу нескольких теорий, в частности, преобразование целого в битовый вектор конечной длины или обратно, либо вовсе не поддерживаются современными решателями, либо их поддержка крайне ограничена и неэффективна. В такой ситуации все взаимосвязи между используемыми низкоуровневой и высокоуровневой моделями памяти оказывается необходимым выражать в виде сложно определяемых пользовательских предикатов, либо в виде неинтерпретируемых предикатов с соответствующими наборами
аксиом. При этом вся работа по формулированию спецификаций этих предикатов и возможному ручному доказательству получаемых в результате УВ (в силу сложности предикатов) ложится на инженера-верификатора. Кроме этого, в присутствии большого количества синонимичных указателей низкоуровневые регионы могут включать в себя довольно значительные области памяти, приводя к тому, что существенная часть данных программы может быть переведена в формулы с использованием теории битовых векторов конечной длины (причем из-за возможной переинтерпретации памяти векторы будут иметь значительную длину, например, при объединении переинтерпретируемого массива структур в один битовый вектор). Это, в свою очередь, может значительно осложнять проверку выполнимости таких формул. Другой неудачный, но весьма распространенный случай - это адресная арифметика со смещением, закодированным в виде битового вектора, когда добавление такого смещения к указателю в одном месте приводит к необходимости кодирования всех добавляемых к этому указателю (и его синонимам) смещений в виде битовых векторов. В предложенных методах моделирования памяти этих недостатков удалось избежать. 

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

Комиссия Минобрнауки России признала обязательства по Соглашению на отчетном этапе исполненными надлежащим образом.