Верификация разграничения доступа в системах больших данных с использованием временных логик

Обеспечение согласованного управления доступом является одной из ключевых задач безопасности в гетерогенных системах больших данных. Проблема представляет собой большое число инструментов обработки данных, источников и пользователей информации; разнородность моделей безопасности; сложность гранулированных правил доступа. Анализ временного фактора в данном случае позволит повысить согласованность и надежность разграничения доступа. Целью работы является выбор методологии и инструментария для имплементации временной логики в процессы верификации контроля доступа систем больших данных. Анализируются виды временной логики и методы верификации на основе TLA (Temporal Logic of Actions). Предлагается использование TLA+ для решения поставленной задачи, приводится пример соответствующей спецификации