Published: December 20, 2008
Author(s)
Vincent Hu, Richard Kuhn, Tao Xie
Conference
Name: 2008 IEEE/IFIP International Symposium on Trust, Security and Privacy for Pervasive Applications (TSP-08)
Dates: 12/17/2008 - 12/20/2008
Location: Shanghai, China
Citation: Proceedings of the 5th International Conference on Embedded and Ubiquitous Computing (EUC 2008), vol. 2, pp. 243-250
To formally and precisely capture the security properties that access control should adhere to, access control models are usually written to bridge the rather wide gap in abstraction between policies and mechanisms. In this paper, we propose a new general approach for property verification for access control models. The approach defines a standardized structure for access control models, providing for both property verification and automated generation of test cases. The approach expresses access control 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 these properties for the access control models and generates test cases via combinatorial covering array for the system implementations of the models.
To formally and precisely capture the security properties that access control should adhere to, access control models are usually written to bridge the rather wide gap in abstraction between policies and mechanisms. In this paper, we propose a new general approach for property verification for...
See full abstract
To formally and precisely capture the security properties that access control should adhere to, access control models are usually written to bridge the rather wide gap in abstraction between policies and mechanisms. In this paper, we propose a new general approach for property verification for access control models. The approach defines a standardized structure for access control models, providing for both property verification and automated generation of test cases. The approach expresses access control 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 these properties for the access control models and generates test cases via combinatorial covering array for the system implementations of the models.
Hide full abstract
Keywords
access control; combinatorial testing; modeling; software assurance
Control Families
None selected
