Assessing Quality of Policy Properties in Verification of Access Control Policies

PDF
0.4MB

Evan Martin
North Carolina State University
United States

JeeHyun Hwang
North Carolina State University
United States

Tao Xie
North Carolina State University
United States

Vincent Hu
National Institute of Standards and Technology
United States

Abstract:
As users often access to sensitive information via a network (e.g., Internet), correctly specified access control, which allows or denies user’s access to that information, is very important. The access control policy authors make sure that only authorized information on that user can be accessed through access control. Otherwise, unauthorized access indicates the security leakage, which should be fixed.
To facilitate managing, maintaining, and analyzing access control, access control policies are often specified in domain-specific, declarative languages. To increase confidence in the correctness of specified policies, policy authors can use policy verification tools to formally verify policies against a set of properties, which are often manually specified. Policy verification is an important technique for high assurance of the correct specification of access control policies. The effectiveness of the verification is directly related to the quality of the properties, i.e., how comprehensively the properties cover various behaviors of the policy and thus assure correctness of these behaviors once verified.
In this paper, we propose a novel approach to assess the quality of properties specified for a policy and, in doing so, the quality of the verification itself. Similar to the way mutation testing is used to assess the quality of a test suite in terms of fault-detection capability, we propose mutation verification to assess the quality of a set of properties. Given a policy and a set of properties, we first mutate the policy to generate various mutant policies, each with a single fault. We then verify whether the properties hold for each mutant policy. If the properties fail to hold for a given mutant policy, then the verification process accurately identifies the fault in the mutant policy. We have implemented Mutaver, a mutation verification tool for XACML, and applied it to policies and properties from a real-world software system.