Case study UCON – Usage control
Modern security architectures depend on robust usage control mechanisms, but verifying their correct implementation remains a significant challenge. In the UCON project, fortiss developed formal semantics, monitoring approaches, and automated analysis tools to support the continuous enforcement and verification of access policies. The outcome is a foundational framework that improves policy reliability in cloud, edge, and IoT environments.
This project was funded by Huawei Technologies Düsseldorf GmbH. The collaboration focused on advancing usage control capabilities to meet the growing security needs of connected systems.
Challenge
Modern access control systems are evolving into continuous usage control systems, especially in dynamic environments like cloud and IoT. However, ensuring these systems behave as intended and comply with policy requirements is difficult without formal methods. Huawei engaged fortiss to develop reliable tools and formal verification methods to ensure that usage control is both enforceable and trustworthy.
Solution
fortiss designed a formal specification framework for continuous usage control systems, providing a foundation for verification and analysis. Using this specification, they developed a novel monitoring approach to verify runtime policy enforcement. The team also created static analysis tools to help developers detect errors and inconsistencies before deployment. The result is a comprehensive toolkit that supports policy authors throughout the lifecycle of access control systems.
Result
- Developed a formal specification language for continuous usage control policies.
- Introduced a runtime monitoring method to verify whether policies are correctly enforced in practice.
- Created automated tools for static policy analysis to detect inconsistencies and improve maintainability.
- Extended the scope of traditional access control semantics to include continuous, real-time enforcement.
- Provided policy developers with better support for writing, testing, and validating security rules.
- Strengthened trust in usage control systems in cloud, edge, and IoT by making behavior verifiable and explainable.
- Improved the security posture of complex environments through rigorous, model-based engineering approaches.
Outcome
The UCON project demonstrates how formal methods, runtime monitoring and automated analysis enable the reliable enforcement and verification of usage control policies. This provides a robust foundation for trustworthy and resilient security architectures in dynamic cloud, edge and IoT environments.
Project partner
