Описан процесс разработки и верификации формальных моделей безопасности управления доступом в операционных системах и реализующих их программных компонентов на примере отечественной защищенной операционной системы специального назначения Astra Linux Special Edition. Этот процесс направлен на получение адекватной оценки характеристик защищенности и безопасности операционных систем и достижение высокого уровня доверия к полученной оценке. Помимо этого, монография знакомит читателя с современными технологиями и инструментами моделирования и верификации, используемыми в подобных процессах. Представленный процесс направлен на обеспечение выполнения требований ГОСТ Р ИСО/МЭК 15408 «Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий» и профилей защиты операционных систем общего назначения (типа «А») третьего и второго классов защиты. Для специалистов в области защиты информации, преподавателей, аспирантов; будет полезна студентам, обучающимся по направлениям подготовки и специальностям УГНПС «Информационная безопасность». Это и многое другое вы найдете в книге Моделирование и верификация политик безопасности управления доступом в операционных системах (Девянин П. Н., Ефремов Д. В., Кулямин В. В., Петренко А. К., Хорошилов А. В., Щепетков И. В.)