Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies Using mCRL2

This paper proposes an approach to formally verify XACML policies using the process algebra mCRL2. XACML (eXtensible Access Control Markup Language) is an OASIS standard for access control systems that is much used in health care due to its fine-grained, attribute-based policy definitions, useful in dynamic environments such as emergency wards. A notorious problem in XACML is the detection of conflicts, which arise especially when combining policies, such as when health institutions merge. Our formal translation of XACML policies into mCRL2, using our automated tool XACML2mCRL2, enables us to verify the above property, called consistency, as well as other policy properties such as completeness and obligation enforcement. Verifying policy properties statically allows us to resolve inconsistencies in advance, thus avoiding situations where an access request is denied in a critical situation (e.g., in an ambulance, when lives may be put in danger) just because of incomplete or inconsistent policies. The mCRL2 toolset is especially useful for modeling behaviors of interactive systems, where XACML would be only one part. Therefore, we verify an access control system together with the intended health care system that it is supposed to protect. For this, we exemplify how to verify safety and liveness properties of an assisted living and community care system.