Алексей Хорошилов, ведущий научный сотрудник ИСП РАН.
Кандидат физико-математических наук (2006 г.), тема диссертации - «Спецификация и тестирование компонентов с асинхронным интерфейсом», руководитель А. К. Петренко. С 1999 года работает в Институте
системного программирования РАН. С 2009 года работает на кафедре Системного программирования факультета Вычислительной математики и кибернетики МГУ. Основные научные результаты: участие в создании технологии разработки тестов на основе формальных
моделей UniTESK и поддерживающих ее инструментов, разработка унифицированной архитектуры тестового набора и правил построения расширений языков программирования для разработки тестов на основе контрактных спецификаций, разработка методов построения
тестов для математических библиотек, разработка специализированной технологии быстрого создания тестов работоспособности.
В феврале 2017 г. ФСТЭК России были приняты профили защиты операционных систем общего назначения (типа «А») [6], основанные на «Требованиях безопасности информации к операционным системам» [7] и ГОСТ Р ИСО/МЭК 15408 [2]. Эти профили включают требования доверия (например, содержащиеся в компонентах доверия ADV_FSP.6 «Полная полуформальная функциональная спецификация с дополнительной формальной спецификацией», ADV_SPM.1 «Формальная модель политики безопасности», AVA_CCA_EXT.1 «Анализ скрытых каналов» и др.), которые ставят перед научным сообществом задачи по разработке соответствующих научно обоснованных технологий их реализации, без чего успешное применение новых профилей защиты будет крайне затруднено.
По данному направлению, в том числе при участии авторов, уже получен ряд результатов.
Во-первых, разработана и изложена в математической нотации мандатная сущностно-ролевая ДП-модель безопасности управления доступом и информационными потоками в ОС семейства Linux (МРОСЛ ДП-модель) [1, 3]. Эта модель включает описание требований к реализации в ОС мандатного, ролевого управления доступом и мандатного контроля целостности, а также условий предотвращения в ней запрещённых информационных потоков (скрытых каналов) по памяти и по времени. Для удобства использования модели на практике она представлена иерархически [4], кроме имеющихся на данный момент её четырёх уровней (первого – модель системы ролевого управление доступом; второго – модель системы ролевого управление доступом и мандатного контроля целостности; третьего – модель системы ролевого управление доступом, мандатного контроля целостности и мандатного управления доступом только с информационными потоками по памяти; четвёртого – модель системы ролевого управление доступом, мандатного контроля целостности и мандатного управления доступом с информационными потоками по памяти и по времени) в разработке находятся ещё три, ориентированных на моделирование невырожденной решётки уровней целостности, запрещающих ролей и их сочетания.
Во-вторых, для упрощения и автоматизации проверки корректности МРОСЛ ДП-модели её иерархическое представление переведено в формализованную нотацию Event-B [5, 10]. При этом элементам, задающим в рамках модели состояния системы, в формализованной нотации ставятся в соответствие переменные Event-B и их инварианты, а де-юре и де-факто правилам преобразования состояний – события Event-B, описываемые при помощи своих предусловий и постусловий. При помощи инструментов дедуктивной верификации платформы Rodin доказывается, что любое преобразование состояния, заданное событиями Event-B, сохраняет все инварианты состояния, что позволяется убедиться в корректности формализации МРОСЛ ДП-модели. Такая же техника применяется и для доказательства безопасности системы.
В-третьих, МРОСЛ ДП-модель, представленная в формализованной нотации Event-B, транслирована в нотацию ACSL [9], которая позволяет сформулировать требования непосредственно к реализации интерфейса Linux Security Module (LSM) на языке Си с учётом всех его особенностей. При этом требования описаны в виде предусловий и постусловий интерфейсных операций и затем при помощи методов дедуктивной верификации, реализованных в инструменте Why3 [11], доказано, что реализация модуля управления доступом, соответствующего МРОСЛ ДП-модели, отвечает этим требованиям.
В-четвёртых, все перечисленные научные подходы были апробированы при разработке и верификации механизма управления доступом отечественной операционной системы специального назначения (ОССН) Astra Linux Special Edition [1, 8], около ста тысяч лицензий на использование которой уже приобрели министерства, ведомства, государственные корпорации и предприятия оборонно-промышленного комплекса Российской Федерации. В настоящее время завершаются сертификационные исследования ОССН по профилю защиты операционных систем типа «А» второго класса защиты.
Подводя итог сказанному, можно констатировать, что создана и апробирована при разработке ОССН научно-технологическая платформа моделирования и верификации политик безопасности управления доступом в ОС. Для передачи полученного опыта заинтересованным разработчикам защищённых ОС, других средств защиты информации, испытательным лабораториям, представителям научного сообщества в ближайшее время готовится к опубликованию описание первого уровня иерархического представления МРОСЛ ДП-модели в математической нотации и формализованной нотации Event-B.
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
Уважаемые коллеги! Для прохода в здание РАН просим принести документ, удостоверяющий личность.
