Алексей Хорошилов

Avatar1

Алексей Хорошилов, ведущий научный сотрудник ИСП РАН.
Кандидат физико-математических наук (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.

СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ

  1. Безопасность операционной системы специального назначения Astra Linux Special Edition. Учебное пособие для вузов / П.В. Буренин, П.Н. Девянин, Е.В. Лебеденко и др.; Под редакцией доктора техн. наук П.Н. Девянина. 2-е издание, стереотипное. М.: Горячая линия – Телеком, 2016. 312 с.
  2. ГОСТ Р ИСО/МЭК 15408-2013. Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий.
  3. Девянин П.Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками. Учебное пособие для вузов. 2-е изд., испр. и доп. М.: Горячая линия — Телеком, 2013. 338 с.: ил.
  4. Девянин П.Н. О результатах формирования иерархического представления МРОСЛ ДП-модели // Прикладная дискретная математика. 2016. Приложение № 9. С. 8387.
  5. Девянин П.Н., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В. Сравнение способов декомпозиции спецификаций на Event-B // Программирование. 2016. № 4. С. 1726.
  6. Документы по сертификации средств защиты информации и аттестации объектов информатизации по требованиям безопасности информации. URL: http://fstec.ru/tekhnicheskaya-zashchita-informatsii/dokumenty-po-sertifikatsii/120-normativnye-dokumenty.
  7. Информационное сообщение об утверждении  Требований безопасности информации к операционным системам от 18 октября 2016 г. № 240/24/4893 / ФСТЭК России. URL: http://fstec.ru/component/attachments/download/1051.
  8. Операционные системы Astra Linux. URL: http://www.astra-linux.ru/.
  9. ANSI/ISO C Specification Language. URL: http://frama-c.com/acsl.html.
  10. P.N. Devyanin, V.V. Kuliamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov. Using Refinement in Formal Development of OS Security Model // In Lecture Notes in Computer Sciences vol. 9609 "Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference", pp. 107-115. Springer International Publishing, 2016. URL: http://dx.doi.org/10.1007/978-3-319-41579-6_9.
  11. Filliatre J.C., Paskevich A. Why3: Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Proceedings of the 22nd European Conference on Programming Languages and Systems. pp. 125–128. ESOP’13, Springer-Verlag, Berlin, Heidelberg (2013). URL: http://dx.doi.org/10.1007/978-3-642-37036-6_8.

Организаторы

При поддержке

Информация

Уважаемые коллеги! Для прохода в здание РАН просим принести документ, удостоверяющий личность.