Системы контроля доступа относятся к числу наиболее важных компонентов безопасности. Неправильная политика, неверная конфигурация или дефекты в программной реализации могут привести к серьезным уязвимостям. Спецификация политик контроля доступа часто является сложной проблемой. Часто конфиденциальность и безопасность системы нарушаются из-за неправильной настройки политик контроля доступа, а не из-за сбоя криптографических примитивов или протоколов.
Эта проблема становится все более серьезной, поскольку программные системы становятся все более сложными и развертываются для управления большим количеством конфиденциальной информации и ресурсов, организованных в сложные структуры. Выявление расхождений между спецификациями политики и их свойствами (предполагаемой функцией) имеет решающее значение, поскольку правильная реализация и применение политик приложениями основаны на предпосылке, что спецификации политики являются правильными. В результате спецификации политики должны проходить строгую проверку и валидацию посредством систематического тестирования, чтобы гарантировать, что спецификации политики действительно воплощают желания авторов политики.
Чтобы формально и точно зафиксировать свойства безопасности, которых должен придерживаться контроль доступа, модели контроля доступа обычно пишутся для преодоления довольно широкого разрыва в абстракции между политикой и механизмом. Таким образом, модель контроля доступа обеспечивает однозначное и точное выражение, а также справку для разработки и реализации требований безопасности. Методы необходимы для проверки того, правильно ли модель управления доступом выражена в политиках управления доступом и удовлетворяются ли свойства в модели. На практике одни и те же политики управления доступом могут выражать несколько моделей управления доступом или выражать одну модель в дополнение к дополнительным ограничениям управления доступом вне модели. Обеспечение соответствия моделей и политик контроля доступа является нетривиальной и критической задачей.
Начатая в 2009 году, NIST CSD разработала прототип системы-инструмент политики контроля доступа (ACPT), который позволяет пользователю создавать, проверять, тестировать и генерировать политики контроля доступа. ACPT предоставляет (1) шаблоны графического интерфейса для составления политик AC, (2) проверку свойств моделей политик AC с помощью средства проверки моделей SMV (Symbolic Model Verification), (3) Полный набор тестов, генерируемый комбинаторным инструментом тестирования NIST ACTS, и (4) генерацию политик XACML в качестве выходных данных проверенной модели. С помощью четырех основных функций ACPT выполняет все синтаксические и семантические проверки, а также интерфейс для составления и объединения правил AC для политик AC. Кроме того, CSD опубликовал исследовательские работы, связанные с ACPT.
Большинство исследований по моделям переменного тока или методам проверки политик сосредоточены на одной конкретной модели, и почти все исследования посвящены прикладным методам, которые требуют завершенных политик переменного тока в качестве входных данных для процессов проверки или тестирования для создания отчетов о неисправностях. Несмотря на то, что правильная проверка достигнута и встречные примеры могут быть созданы вместе с найденными ошибками, эти методы не предоставляют никакой информации об источнике ошибок правил, которые могли бы привести к конфликтам в присвоении привилегий, утечке привилегий или разрешениям конфликта интересов. Сложность поиска источника неисправностей возрастает особенно тогда, когда правила АС запутанно охватывают дублированные переменные до некоторой степени сложности. Сложность заключается в том, что ошибка может быть вызвана не одним конкретным правилом; например, правило x предоставляет субъекту/атрибуту s доступ к объекту/атрибуту o, а правило y запрещает группе субъект/атрибут g, членом которой является s, доступ к объекту o. такой конфликт может быть разрешен только путем удаления либо правила x, либо y, либо G-членства s из политики. Но удаление x или Y влияет на другие правила, которые зависят от них (например, члену субъектной группы g k предоставляется доступ к объекту o), а удаление членства s в g отключит законный доступ g к другим объектам/атрибутам через членство. Таким образом, требуется вручную проанализировать каждое правило в политике, чтобы найти правильное решение для ошибки.
Чтобы решить эту проблему, CSD исследовал моделирование логических схем правил переменного тока (ACRLCS) метод, который позволяет авторам AC обнаруживать неисправность, когда вызывающее неисправность правило AC добавляется в политику, поэтому исправление может быть реализовано в режиме реального времени перед добавлением других правил, которые еще больше усложняют усилия по обнаружению. Вместо того чтобы проверять, прослеживая взаимосвязи между правилами после завершения политики, автору политики нужно только проверить вновь добавленное правило на соответствие предыдущим “правильным”. В ACRLCS правила переменного тока представлены в моделируемой логической схеме (SLC). Использование моделирования может ограничить реализацию ACRLCS на физической электронной схеме; однако эта концепция может быть реализована и вычислена с помощью имитационного программного обеспечения.