Рассматривается задача о спецификации и проверке свойств безопасности в моделях логического разграничения доступа. Для проверки класса таких свойств, а именно — свойств информационных потоков, предлагается подход, в основу которого положены методы верификации на модели. Описывается применение таких методов в процессе анализа моделей логического разграничения доступа в Unix-подобных операционных системах с учетом древовидной иерархической структуры, заданной на объектах доступа. Ключевые слова: информационная безопасность, модели логического разграничения доступа, верификация на модели.
