Авторитетность издания
ВАК - К1
RSCI, ядро РИНЦ
Добавить в закладки
Следующий номер на сайте
№3
Ожидается:
16 Сентября 2025
Статьи журнала №2 2025
[№2 за 2025 год]
Авторы: Петренко А.К. (petrenko@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, НИУ Высшая школа экономики (профессор, зав. отделом), доктор физико-математических наук; Ефремов Д.В. (efremov@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН (старший научный сотрудник); Корныхин Е.В. (kornevgen@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова (доцент, старший научный сотрудник), кандидат физико-математических наук; Кулямин В.В. (kuliamin@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, НИУ Высшая школа экономики (доцент, ведущий научный сотрудник), кандидат физико-математических наук; Семенов В.А. (vital@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН (профессор, зав. отделом), доктор физико-математических наук;
Аннотация: Работа посвящена методике верификации средств защиты информации (СЗИ) на соответствие формальным моде-лям безопасности. Поддержка такой верификации требуется современными стандартами разработки ПО с высоким уровнем доверия, а именно стандартами группы «Защита информации. Формальная модель управления доступом» и проектом стандарта «Защита информации. Системы с конструктивной информационной безопасностью. Методология разработки». В статье уточняется, что СЗИ – это механизм реализации требований информационной безопасности в программных системах. Обеспечение корректности и надежности его функционирования в рамках базовых программных систем промышленного уровня, таких как операционные системы или СУБД, является самостоятельной и достаточно сложной задачей. Отмечается, что при проектировании подобных систем основные свойства СЗИ должны быть заранее продуманы и точно описаны. Создавать и эффективно использовать строгие описания требований к СЗИ позволяют формальные методы разработки и верификации программ, но в классическом виде эти методы не удается масштабировать для таких крупных и сложных систем, как операционные системы или СУБД. Для верификации промышленной СЗИ предлагается использовать технику динамической верификации, в ходе которой сопоставляются трассы выполнения верифицируемой СЗИ и ее формальной модели. Поскольку мо-дель и ее реализация описаны на разных уровнях абстракции, сопоставление опирается на неклассическое отношение уточнения. Данное уточнение реализовано в виде специального медиатора, строящего последовательность событий в модели по набору событий в самой верифицируемой системе. В статье приводится алгоритм проверки полученной трассы событий на корректность в рамках формальной модели СЗИ.
Keywords: cybersecurity, formal specifications, model-based testing, secure operating systems, Secure-by-Design
Просмотров: 304
Авторы: Петренко А.К. (petrenko@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, НИУ Высшая школа экономики (профессор, зав. отделом), доктор физико-математических наук; Ефремов Д.В. (efremov@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН (старший научный сотрудник); Корныхин Е.В. (kornevgen@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова (доцент, старший научный сотрудник), кандидат физико-математических наук; Кулямин В.В. (kuliamin@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, НИУ Высшая школа экономики (доцент, ведущий научный сотрудник), кандидат физико-математических наук; Семенов В.А. (vital@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН (профессор, зав. отделом), доктор физико-математических наук;
Аннотация: Работа посвящена методике верификации средств защиты информации (СЗИ) на соответствие формальным моде-лям безопасности. Поддержка такой верификации требуется современными стандартами разработки ПО с высоким уровнем доверия, а именно стандартами группы «Защита информации. Формальная модель управления доступом» и проектом стандарта «Защита информации. Системы с конструктивной информационной безопасностью. Методология разработки». В статье уточняется, что СЗИ – это механизм реализации требований информационной безопасности в программных системах. Обеспечение корректности и надежности его функционирования в рамках базовых программных систем промышленного уровня, таких как операционные системы или СУБД, является самостоятельной и достаточно сложной задачей. Отмечается, что при проектировании подобных систем основные свойства СЗИ должны быть заранее продуманы и точно описаны. Создавать и эффективно использовать строгие описания требований к СЗИ позволяют формальные методы разработки и верификации программ, но в классическом виде эти методы не удается масштабировать для таких крупных и сложных систем, как операционные системы или СУБД. Для верификации промышленной СЗИ предлагается использовать технику динамической верификации, в ходе которой сопоставляются трассы выполнения верифицируемой СЗИ и ее формальной модели. Поскольку мо-дель и ее реализация описаны на разных уровнях абстракции, сопоставление опирается на неклассическое отношение уточнения. Данное уточнение реализовано в виде специального медиатора, строящего последовательность событий в модели по набору событий в самой верифицируемой системе. В статье приводится алгоритм проверки полученной трассы событий на корректность в рамках формальной модели СЗИ.
Abstract: The work focuses on the methodology of verifying information security tools for compliance with formal security models. Such verification is due to modern standards of software development with a high level of trust, namely the standards of the group GOST R 59453 “Information security. Formal access control model” and the draft GOST R “Information security. Constructive information security systems. Development methodology”. Information security tools is a mechanism for im-plementing information security requirements in software systems. Ensuring the mechanism correctness and reliability in terms of basic industrial-grade software systems, such as operating systems or database management systems (DBMS), is an independent and rather complex task. Designing such systems implies that the main properties of the information security tools are premeditate and accurately described. Formal methods of software development and verification allow creating and effective using strict descriptions of requirements for information security systems. However, in their classical form, formal methods are non-scalable for such large and complex systems as operating systems or DBMS.
To verify industrial information security tools, the authors propose using runtime verification, which compares execution traces of a verified information security system and its formal model. Since the model and its implementation are described at different abstraction levels, the comparison is based on a non-classical refinement relation. The relation is implemented as a special mediator that builds a sequence of events in the model based on a set of events in the verified system itself. The paper describes an algorithm for checking the obtained event trace for correctness within the framework of the formal model of an information security tool.
Ключевые слова: кибербезопасность, формальные спецификации, тестирование на основе моделей, защищенные операционные системы, конструктивная информационная безопасностьKeywords: cybersecurity, formal specifications, model-based testing, secure operating systems, Secure-by-Design
Просмотров: 304
[№2 за 2025 год]
Просмотров: 304
Работа посвящена методике верификации средств защиты информации (СЗИ) на соответствие формальным моде-лям безопасности. Поддержка такой верификации требуется современными стандартами разработки ПО с высоким уровнем доверия, а именно стандартами группы «Защита информации. Формальная модель управления доступом» и проектом стандарта «Защита информации. Системы с конструктивной информационной безопасностью. Методология разработки». В статье уточняется, что СЗИ – это механизм реализации требований информационной безопасности в программных системах. Обеспечение корректности и надежности его функционирования в рамках базовых программных систем промышленного уровня, таких как операционные системы или СУБД, является самостоятельной и достаточно сложной задачей. Отмечается, что при проектировании подобных систем основные свойства СЗИ должны быть заранее продуманы и точно описаны. Создавать и эффективно использовать строгие описания требований к СЗИ позволяют формальные методы разработки и верификации программ, но в классическом виде эти методы не удается масштабировать для таких крупных и сложных систем, как операционные системы или СУБД. Для верификации промышленной СЗИ предлагается использовать технику динамической верификации, в ходе которой сопоставляются трассы выполнения верифицируемой СЗИ и ее формальной модели. Поскольку мо-дель и ее реализация описаны на разных уровнях абстракции, сопоставление опирается на неклассическое отношение уточнения. Данное уточнение реализовано в виде специального медиатора, строящего последовательность событий в модели по набору событий в самой верифицируемой системе. В статье приводится алгоритм проверки полученной трассы событий на корректность в рамках формальной модели СЗИ.
Петренко А.К. (petrenko@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, НИУ Высшая школа экономики (профессор, зав. отделом), доктор физико-математических наук; Ефремов Д.В. (efremov@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН (старший научный сотрудник); Корныхин Е.В. (kornevgen@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова (доцент, старший научный сотрудник), кандидат физико-математических наук; Кулямин В.В. (kuliamin@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, НИУ Высшая школа экономики (доцент, ведущий научный сотрудник), кандидат физико-математических наук; Семенов В.А. (vital@ispras.ru) - Институт системного программирования имени В.П. Иванникова РАН (профессор, зав. отделом), доктор физико-математических наук;
