TLA+ based access control model specification

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