Продолжаем пополнять библиотеку разработчика кибериммунных систем. И сегодня у нас научная статья для ценителей жанра: Владимир Буренков взялся за трудную задачу формализации и верификации модели мандатного контроля целостности, реализованного в KasperskyOS.
Автор описал выбор метода и инструмента верификации (использован язык Event-B), напомнил архитектуру KasperskyOS, провёл параллели с архитектурой MILS, описал ключевые сущности, использующиеся при формулировке политик безопасности на языке PSL.
В разделе 4 данной статьи приводится формальная модель мандатного контроля целостности, включая описание контекста, сущностей и объектов, доступов и информационных потоков, уровней целостности. Описывается машина модели, сущности и объекты, доступы и информационные потоки, события модели. Автор формализует, анализирует и доказывает свойства безопасности, обеспечиваемые моделью.
Рекомендуем изучить эту статью специалистам в области разработки операционных систем, безопасных решений, разработчикам политик безопасности.
Продолжаем пополнять библиотеку разработчика кибериммунных систем. И сегодня у нас научная статья для ценителей жанра: Владимир Буренков взялся за трудную задачу формализации и верификации модели мандатного контроля целостности, реализованного в KasperskyOS.
Автор описал выбор метода и инструмента верификации (использован язык Event-B), напомнил архитектуру KasperskyOS, провёл параллели с архитектурой MILS, описал ключевые сущности, использующиеся при формулировке политик безопасности на языке PSL.
В разделе 4 данной статьи приводится формальная модель мандатного контроля целостности, включая описание контекста, сущностей и объектов, доступов и информационных потоков, уровней целостности. Описывается машина модели, сущности и объекты, доступы и информационные потоки, события модели. Автор формализует, анализирует и доказывает свойства безопасности, обеспечиваемые моделью.
Рекомендуем изучить эту статью специалистам в области разработки операционных систем, безопасных решений, разработчикам политик безопасности.
