ИСТИНА

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

Nowadays a systematic approach is needed to solve security problems of a certain software and hardware system, including such elements as methods of preventing problems and attacks; Methods for detecting problems and attacks How to solve problems and stop attacks. The prevention and detection of security problems on a systematic basis is possible only with a clear description of the types of possible system security problems, as well as the solutions used in the architecture and design of the system, aimed at blocking them and monitoring the signs of their occurrence. The main way to describe the most important design solutions for system protection and the safety properties implemented by them are safety models.

Будет предложен метод оформления таких моделей (моделей безопасности) на основе языка формальных спецификаций. Такой метод позволит в явном и строгом виде сформулировать гарантируемые свойства безопасности и применить его для описания сложных моделей безопасности современных операционных систем, а также использовать полученное описание для дальнейших более сложных задач разработки, прежде всего, анализа, верификации и тестирования моделей безопасности.

В период с 2020г. по 2025 г. на кафедре системного программирования в рамках госбюджетной темы №121042600045-5 были проведены исследования методов построения моделей безопасности ответственных программно-аппаратных систем. предложен метод оформления таких моделей на основе языка формальных спецификаций. Такой метод позволит в явном и строгом виде сформулировать гарантируемые свойства безопасности и применить его для описания сложных моделей безопасности современных операционных систем, а также использовать полученное описание для дальнейших более сложных задач разработки, прежде всего, анализа, верификации и тестирования моделей безопасностиПредложен метод оформления таких моделей на основе языка формальных спецификаций. Такой метод позволяет в явном и строгом виде формулировать гарантируемые свойства безопасности и применять его для описания сложных моделей безопасности современных операционных систем, а также использовать полученное описание для дальнейших более сложных задач разработки, прежде всего, анализа, верификации и тестирования моделей безопасности. Совместно с Институтом системного программирования РАН выполнены работы по исследованию используемых на практике методов верификации свойств безопасности кода базового программного обеспечения.

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