Skip to main content
U.S. flag

An official website of the United States government

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

Model Checking for Verification of Mandatory Access Control Models and Properties



Chung Tong Hu, David R. Kuhn, Tao Xie, J Hwang


Mandatory access control (MAC) mechanisms control which users or processes have access to which resources in a system. MAC policies are increasingly specified to facilitate managing and maintaining access control. However, the correct specification of the policies is a very challenging problem. To formally and precisely capture the security properties that MAC should adhere to, MAC models are usually written to bridge the rather wide gap in abstraction between policies and mechanisms. In this paper, we propose a general approach for property verification for MAC models. The approach defines a standardized structure for MAC models, providing for both property verification and automated generation of test cases. The approach expresses MAC models in the specification language of a model checker and expresses generic access control properties in the property language. Then the approach uses the model checker to verify the integrity, coverage, and confinement of these properties for the MAC models and finally generates test cases via combinatorial covering array for the system implementations of the models.
International Journal of Software Engineering and Knowledge Engineering


access control, policy, model, testing


, C. , Kuhn, D. , Xie, T. and Hwang, J. (2011), Model Checking for Verification of Mandatory Access Control Models and Properties, International Journal of Software Engineering and Knowledge Engineering, [online], (Accessed May 18, 2024)


If you have any questions about this publication or are having problems accessing it, please contact

Created February 28, 2011, Updated November 10, 2018