Регистрация / Вход
Прислать материал

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

Докладчик: Петренко Александр Константинович

Должность: Заведующий отделом

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

Основные планируемые результаты проекта:
Запланированы следующие основные результаты работ:
- Должен быть выполнен аналитический обзор современной научно-технической, нормативной, методической литературы, затрагивающей научно-техническую проблему, исследуемую в рамках научных исследований, в том числе обзор научных информационных источников: статьи в ведущих зарубежных и (или) российских научных журналах, монографии и (или) патенты - не менее 15 научно-информационных источников за период 2009 – 2013 гг.
- Должны быть выполнены патентные исследования в соответствии с ГОСТ 15.011-96.
- Должны быть проведены исследования методов масштабируемой статической верификации программ, а также определены направления их развития для верификации системного программного обеспечения.
- Должен быть разработан метод масштабируемой статической верификации системного программного обеспечения.
- Должен быть разработан метод параллельной статической верификации системного программного обеспечения, позволяющий проверять одновременно несколько правил корректности.
- Должен быть разработан метод фильтрации трасс ошибок, позволяющий выявлять несколько ошибок в программном обеспечении и проверять несколько правил корректности за один запуск инструмента статической верификации.
- Должен быть разработан метод оценки покрытия исходного кода при статической верификации.
- Должен быть разработан метод статической верификации многопоточного программного обеспечения.
- Должен быть разработан экспериментальный образец системы масштабируемой статической верификации системного программного обеспечения.
- Должны быть разработаны программа и методики экспериментальных исследований экспериментального образца системы масштабируемой статической верификации системного программного обеспечения.
- Должны быть проведены экспериментальные исследования экспериментального образца системы масштабируемой статической верификации системного программного обеспечения в соответствии с разработанными программой и методиками экспериментальных исследований.
- Должны быть проведены обобщение и оценка полученных результатов научных исследований.
- Должны быть разработаны предложения и рекомендации по вовлечению полученных результатов прикладных научных исследований в хозяйственный оборот.
- Должен быть разработан проект технического задания на проведение ОКР по теме «Разработка инструментов для масштабируемой статической верификации промышленного системного программного обеспечения».

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

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

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

Верификация отдельного программного модуля распадается на решение многих, так называемых, верификационных задач. Каждая из задач направлена на проверку тех или иных семантических правил языка программирования или правил взаимодействия модуля с другими модулями, системой поддержки времени исполнения или с ядром операционной системы (предметно-ориентированных правил). С одной стороны, то что проверку разных правил можно выполнять независимо друг от друга, позволяет распараллеливать верификацию. Однако таких верификационных задач становится так много, что управление параллельной верификацией может оказаться слишком сложным, а уровень накладных расходов слишком высоким. Еще один способ повышения скорости верификации — использовать для каждой из программ и даже каждого из фрагментов программ (например, для циклов, для линейных участков и так далее) различные методы верификации. Это является одной из основных идей адаптивного (конфигурируемого) анализа — метода, который развивает группа профессора Д.Бейера. Заранее узнать, какой метод верификации следует выбрать для той или иной программы можно только путем запуска того или иного вида анализа. При этом на такой процесс «проб и ошибок» уходит и время, и другие ресурсы. Выходом из этой ситуации может быть эффективное решение вопроса о переиспользовании данных (от англ. re-use), которые получены во время анализа программы одним методом, другими методами. Аналогично, можно переиспользовать данные анализа одного правила для анализа другого правила или даже сразу для анализа группы правил.

Идея эффективного переиспользования результатов первых фаз верификации в ходе последующих фаз верификации была проверена на экспериментах. Группа из Университета Пассау экспериментировала с переиспользованием данных анализа, полученных при помощи разных алгоритмов верификации (классический CEGAR, Explicit verification и др.). ИСП РАН провел эксперименты с одновременной проверкой нескольких спецификаций правил при верификации одного модуля. И те и другие эксперименты показали, что это перспективное направление исследований.

Эксперименты показали существенное увеличение скорости анализа, в среднем в 4 раза. В отдельных случаях удалось повысить скорость анализа до 210 раз. Кроме того, становятся разрешимыми задачи, которые не были разрешимы без переиспользования результатов анализа (см. Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, and Philipp Wendler. Precision Reuse for Efficient Regression Verification. In B. Meyer, L. Baresi, and M. Mezini, editors, Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2013), pages 389-399, 2013).

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

В настоящее время существуют различные реализации инструментов статической верификации в облачных сервисах, в том числе доступные как веб-сервисы:
- Набор инструментов от компании Майкрософт: http://rise4fun.com
- Aprove: http://aprove.informatik.rwth-aachen.de/index_llvm.asp
- Divine: http://divine.fi.muni.cz/try.cgi
- Interproc: http://pop-art.inrialpes.fr/interproc/interprocweb.cgi

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

Наиболее полно конструкции языков программирования на данный момент поддерживают инструменты статической верификации, основанные на методах ограничиваемой проверки моделей (Bounded Model Checking, BMC). Например, в инструменте верификации CBMC(D.Kröning, M.Tautschnig. CBMC – Си bounded model checker. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 8413, 2014.), совместной разработки университетов Карнеги Меллон (США), Оксфорд (Англия) и Королевы Марии (Англия), есть поддержка операций с битовой точностью, динамического выделения памяти, операций с указателями, а также с числами с плавающей точкой.

Метод BMC имеет принципиальное теоретическое ограничение — доказательство выполнения спецификации строится только для заданной пользователем глубины разворачивания циклов, то есть для программ, где реальное число итераций может превысить хотя бы 10, этот метод не применим. Кроме того, известно, что данные методы в применении к сравнительно большим программам гораздо хуже масштабируются по сравнению с методами адаптивного статического анализа, так как не умеют абстрагироваться от большого количества несущественных деталей, не влияющих на нарушение спецификации. Так, например, на международных соревнованиях по верификации в категории состоящей из драйверов устройств CBMC работал в 200 раз дольше победителя, инструмента BLAST, разрабатываемого в ИСП РАН.

Назначение и область применения, эффекты от внедрения результатов проекта:
В практической плоскости областью применения полученных результатов являются все виды программного обеспечения, написанного на языке Си, в первую очередь, системного программного обеспечения. В настоящее время заинтересованность в использовании планируемых результатов проекта проявили несколько российских и зарубежных компаний, занимающихся разработкой, адаптацией и сертификацией специализированных версий ОС Linux. Основная бизнес-модель, на которую нацелен ИСП РАН в плане коммерциализации полученных результатов, это предоставление сервисов по развитию/адаптации/внедрению инструментов верификации по требованиям крупных компаний и развертывание веб-сервиса для удаленной верификации отдельных компонентов пользователей на основе платной подписки.

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

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

Выполнен поиск и предварительный анализ патентов по теме исследования.

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

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