An end to end correctness verification approach for application specific usage control

Usage control is a comprehensive access control model developed to cater the security needs of the wide range of application domains. Safety property of the usage control model ensures only the design level safety whereas the correctness of usage control in software application depends on the correctness of implementation as well. Most of the research in access control left the correctness of implementation as a general software verification problem. Software verification in general requires an extensive exploration of the complete state space, whereas access control of an application evolves over few repeated protection states. This paper presents a method to verify the correctness of usage control implementation by capturing and analyzing only the protection states. We use this method in the end to end correctness verification approach, which ensures the design as well as implementation correctness of usage control and we also provide an illustrative case study.