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

14.604.21.0051

Аннотация скачать
Общие сведения
Номер
14.604.21.0051
Тематическое направление
Информационно-телекоммуникационные системы
Исполнитель проекта
Федеральное государственное бюджетное учреждение науки Институт системного программирования Российской академии наук
Название доклада
Разработка методов и инструментов для дедуктивной верификации модулей ядра операционной системы Linux.
Докладчик
Хорошилов Алексей Владимирович
Тезисы доклада
Цели и задачи исследования
Целью исследования является разработка методов и инструментов дедуктивной верификации компонентов операционных систем.

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

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

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

Для поддержки подобных случаев в язык спецификации ACSL были введены два новых теневых оператора, то есть оператора, имеющих смысл только для модели программы, но не для исходной программы, – оператор переинтерпретации и оператор разбиения выделенного блока памяти. Смысл первого оператора состоит в преобразовании блока памяти, выделенного для одного типа структур или объединений в блок памяти для структур или объединений другого типа, при условиях, что (1) в обоих этих структурах/объединениях отсутствуют поля-указатели и что либо (2а) размер первого (исходного) композитного типа кратен размеру второго (целевого), –  либо (2б) помимо обратной кратности (размер целевого типа кратен размеру исходного), размер исходного блока также кратен размеру целевого типа. Одного лишь оператора переинтерпретации оказывается недостаточно для представления, к примеру, переинтерпретации массива байт, содержащего две последовательно записанные структуры разных взаимно не кратных размеров, в два соответствующих указателя на структуры (в силу некратности размера массива размеру каждой из структур). Здесь оказывается уместным применение второго оператора – разбиения, смысл которого состоит в разбиении исходного блока памяти непосредственно перед выполнением оператора переинтерпретации на две непрерывные части –  доступную и теневую с целью последующего объединения этих частей вновь в единый блок после того, как будет выполнен обратный оператор переинтерпретации и типы частей разбитого блока вновь совпадут.

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

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

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

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

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

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

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