Formal Semantics for Attribute Access and Usage Control
The project develops analysis and verification methods for modern continuous usage control systems deployed in cloud, edge, and IoT environments. To make the analysis of usage control possible, we develop a formal specification of the intendent system behavior and use it to develop methods for verification and analysis.
There are three main goals:
The formal specification of usage control provides the basis that makes automated analysis and verification possible. The project extends the scope of the formal semantics of access control systems, particularly by capturing models of continuous usage control. It applies the results to develop a monitoring method for verifying that usage control policies are enforced correctly. It develops new automated methods for analyzing properties of policies statically before they are deployed.
01.11.2021 – 31.05.2023