This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2012 IEEE 17th International Conference on Engineering of Complex Computer Systems
A Design by Contract Approach to Verify Access Control Policies
Paris, France France
July 18-July 20
ISBN: 978-1-4673-2156-3
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.
Index Terms:
Contracts,Access control,Automata,Monitoring,Containers,Design by Contract,Access control specification,verification
Citation:
Hakim Ferrier-Belhaouari, Pierre Konopacki, Regine Laleau, Marc Frappier, "A Design by Contract Approach to Verify Access Control Policies," iceccs, pp.263-272, 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, 2012
Usage of this product signifies your acceptance of the Terms of Use.