Verification of agent knowledge in dynamic access control policies
This work addresses security vulnerabilities in access control systems for domains like cybersecurity, but it appears incremental as it builds on existing model-checking methods with a new abstraction technique.
The authors tackled the problem of detecting information flow vulnerabilities in dynamic access control policies by developing a modeling technique based on interpreted systems to verify temporal-epistemic properties, and they introduced a novel abstraction and refinement technique to overcome state explosion in model-checking, though no concrete numerical results are provided.
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.