Verification of agent knowledge in dynamic access control policies

TL;DR

This paper presents a novel modeling and verification approach for dynamic access control policies, enabling detection of information flow vulnerabilities through temporal-epistemic property analysis, while addressing state explosion issues with abstraction techniques.

Contribution

It introduces a new interpreted systems-based modeling technique and an abstraction-refinement method for verifying knowledge-related properties in dynamic access control policies.

Findings

Effective detection of information flow vulnerabilities.

Successful application of abstraction techniques to mitigate state explosion.

Verification of temporal-epistemic safety properties in access control systems.

Abstract

We develop a modeling technique based on interpreted systems in order to verify temporal-epistemic properties over access control policies. This approach enables us to detect information flow vulnerabilities in dynamic policies by verifying the knowledge of the agents gained by both reading and reasoning about system information. To overcome the practical limitations of state explosion in model-checking temporal-epistemic properties, we introduce a novel abstraction and refinement technique for temporal-epistemic safety properties in ACTLK (ACTL with knowledge modality K) and a class of interesting properties that does fall in this category.