Сборники трудов ИСП РАН


Спецификация модели управления доступом на языке темпоральной логики действий Лэмпорта

Козачок А.В. (Академия ФСО, Орел, Россия)

Аннотация

В статье представлено описание модели управления доступом на языке темпоральной логики действий Лэмпорта, обеспечивающей выполнение требований мандатного контроля целостности и конфиденциальности с учетом информационных потоков по памяти. Отличительной особенностью модели является учет особенностей жизненного цикла электронных документов (задания прав к метаинформации и содержимому документа отдельно, ограничение числа копий документа). Для задания модели управления доступом был выбран язык темпоральной логики действий Лэмпорта, поскольку его нотация представляется наиболее близкой к общепринятой математической, выразительные возможности и инструментальные средства позволяют описывать и верифицировать системы, заданные в виде конечных автоматов. В модели определены следующие действия: создание/удаление субъекта, чтение, запись, дозапись ("слепая" запись), создание/удаление объекта, назначение/удаление прав доступа, вложение объекта в объект, исключение вложенного объекта, утверждение объекта (документа), отправка объекта (документа) в архив, отмена действия утвержденного объекта (документа), копирование объекта (документа). Также определены следующие инварианты: проверки типов (включает в себя проверку соответствия всех полей объектов, также проверку соответствия типу субъектов и проверку уникальности идентификаторов субъектов и объектов) и проверки безопасности (включает в себя проверку меток конфиденциальности и целостности взаимодействующих субъектов и объектов, а также корректность процедуры назначения прав доступа).

Ключевые слова

модели безопасности, компьютерные системы, верификация, моделирование, темпоральная логика, политика безопасности, управление доступом

Издание

Труды Института системного программирования РАН, том 30, вып. 5, 2018, стр. 147-162.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2018-30(5)-9

Для цитирования

Козачок А.В. Спецификация модели управления доступом на языке темпоральной логики действий Лэмпорта. Труды Института системного программирования РАН, том 30, вып. 5, 2018, стр. 147-162. DOI: 10.15514/ISPRAS-2018-30(5)-9.

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома