Model Checking for Verification of Mandatory Access Control Models and Properties

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.

• Type: Journal
• Year: 2011
• Where: IJSEKE
• Authors: Vincent C. Hu, D. Richard Kuhn, Tao Xie, JeeHyun Hwang
• Keywords: IJSEKE 2011, Mac Models, Model Checker, System Implementations