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

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

Докладчик: Хорошилов Алексей Владимирович

Должность: в.н.с.

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

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

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

Новизну задач и обусловленную ими новизну предлагаемых методов в данном проекте нужно рассматривать в трех аспектах:
Первый аспект «новизны» - это перечисленные выше особенности компонентов операционных систем, которые в полной мере не поддерживаются известными методами и инструментами дедуктивной верификации, доступными отечественным исследователям и разработчикам.
Второй аспект - это применение уже известных в академических исследованиях приемов для верификации реальных крупных и сложных программ – реальные программы как минимум на 2 порядка превосходят типичные примеры верификации, которые рассматриваются в статьях и учебных курсах;
В-третьих, речь идет о новых для промышленного программирования подходах. В случае дедуктивной верификации проверка корректности программы отказывается от метода проб и ошибок, типичного для программистов и тестировщиков-практиков, и превращается в "математическое" доказательство. Для того, чтобы методы и инструменты могли использоваться в промышленной практике, нужно существенно адаптировать их к условиям целевого применения, то есть к процессам разработки ядра ОС Linux.

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

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

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

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