Engineering of Complex Computer Systems, IEEE International Conference on (2012)
Paris, France France
July 18, 2012 to July 20, 2012
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICECCS.2012.4
In the security domain, access control (AC) consists in specifying who can access to what and how, with the four well-known concepts of permission, prohibition, obligation and separation of duty. In this paper, we focus on role-based access control (RBAC) models and more precisely on the verification of formal RBAC models. We propose a solution for this verification issue, based on the use of the Tam ago platform. In Tam ago, functional contracts can be defined with pre/post conditions and deterministic automata. The Tam ago platform provides tools for static verifications of these contracts, generation of test scenarios from the abstract contracts and monitoring facilities for dynamic analyses. We have extended the platform to take into account AC aspects. AC rules, expressed in a subset of EB3SEC, a process algebra-based language, are translated into pre and post conditions of new security contracts. We have also adapted the test case generator to derive suitable test scenarios and the monitoring framework by adding a new security component.
Contracts, Access control, Automata, Monitoring, Containers, Design by Contract, Access control specification, verification
H. Ferrier-Belhaouari, P. Konopacki, R. Laleau and M. Frappier, "A Design by Contract Approach to Verify Access Control Policies," 2012 17th International Conference on Engineering of Complex Computer Systems (ICECCS), Paris, 2012, pp. 263-272.