Reliable, continuous usage control through formal specification and verification
UCON
Project description
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:
- Formalization: Define a clear and rigorous specification for policies and continuous usage control.
- Verification: Develop a monitoring approach for verifying that usage control systems correctly implement the specification.
- Analysis: Support the correct use of usage control systems with automated policy analysis methods that may be used to assist writing and maintaining policies.
Research contribution
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.
Project duration
01.11.2021 – 31.05.2023
Contact
Project partner
Publications
- Static and Dynamic Analysis of a Usage Control System In SACMAT 2024: Proceedings of the 29th ACM Symposium on Access Control Models and Technologies, 2024. Details DOI BIB
- Specifying a Usage Control System In Proceedings of the 28th ACM Symposium on Access Control Models and Technologies (SACMAT ’23), pages 8, New York, NY, USA, 2023. ACM. Details DOI BIB