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

14.616.21.0015

Аннотация скачать
Постер скачать
Общие сведения
Номер
14.616.21.0015
Тематическое направление
Информационно-телекоммуникационные системы
Исполнитель проекта
Федеральное государственное бюджетное учреждение науки Институт системного программирования Российской академии наук
Название доклада
Разработка методов и инструментов для масштабируемой статической верификации системного программного обеспечения.
Докладчик
Петренко Александр Константинович
Тезисы доклада
Цели и задачи исследования
Основной целью данного проекта является исследование и разработка комплекса научно-технических решений, позволяющих распространить
область применения новейших методов статической верификации на реальное системное программное обеспечение, в первую очередь, на
операционные системы.
Данный проект направлен на решение следующих проблем:
- ограничения современных аппаратных средств и программных средств статической верификации, не позволяющие верифицировать
программные системы достаточно большого размера;
- отсутствие готовых решений и опыта решения крупных верификационных задач с использованием возможностей кластерных и облачных
технологий;
- неэффективный анализ операций с числами с плавающей точкой, операций с динамической памятью и операций с общими данными в
многопоточных программных системах.
Актуальность и новизна исследования
В программных системах встречается множество ошибок, которые связаны с нарушениями предметно-ориентированных правил, накладывающих ограничения на взаимодействия между различными компонентами системы, например, между драйвером и ядром. Было проведено исследование исправленных ошибок в драйверах ОС Linux за год разработки (с 2010 по 2011), которое показало, что более половины ошибок связаны с нарушением правил взаимодействия с интерфейсами ядра. То есть для выявления таких ошибок требуются проверки, учитывающие особенности предметной области, в данном случае требования к межмодульным взаимодействиям в ОС Linux. В настоящее время методы статической верификации не достаточно развиты, чтобы обеспечить верификацию системного ПО. Источниками сложности являются размер программ и их сложность. Современные методы статической верификации справляются лишь со сравнительно небольшими по размеру программами. Размеры же современного системного ПО измеряются миллионами строк кода.
Вторая причина сложности верификации системного ПО связана с целым рядом отличий системного ПО от пользовательских приложений. Примерами такого отличия является активное использование арифметики указателей, операций с битовой точностью. Имеющиеся в настоящее время инструменты верификации без соответствующей модернизации не могут верифицировать программы с такими конструкциями. Тем самым можно констатировать, что системное ПО требует специальную поддержку в инструментах статической верификации.
Принципиальным элементом новизны данного исследования является привлечение новейших инструментов и математических, формальных методов верификации программ реального размера и чрезвычайно высокой сложности.
Описание исследования

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

Наиболее перспективный метод статической верификации, который позволяет выделить подзадачи из общей задачи верификации, был предложен в рамках развития метода адаптивного статического анализа (англ. Configurable Program Analysis - CPA). Данный метод развивается, в основном, благодаря усилиям Иностранного партнера проекта, группы сотрудников Университета Пассау (Германия) под руководством профессора Дирка Бейера (Dirk Beyer). Метод адаптивного статического анализа позволяет развивать новые техники верификации независимо, комбинируя их между собой. Способ комбинации методов не произвольный. Он дает положительный эффект только в случае учета совместимости методов, учета взаимной зависимости результатов различных видов анализа. Для эффективной комбинации также требуется соответствующая инфраструктура.

Результаты исследования

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

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

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