Specification and Verification Using Alloy of Optimistic Access Control for Distributed Collaborative Editors

Aurel Randolph 1 Abdessamad Imine 2 Hanifa Boucheneb 1 Quintero Alejandro
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Distributed Collaborative Editors are interactive systems where several and dispersed users edit concurrently shared documents. Generally, these systems rely on data replication and use safe coordination protocol which ensures data consistency even though the users's updates are executed in any order on different copies. Controlling access in such systems is a challenging problem, as they need dynamic access changes and low latency access to shared documents. Usually, a flexible access control protocol is used; it is based on replicating the shared document and its authorization policy at the local memory of each user. To deal with latency and dynamic access changes, the access control is optimistic in such a way that the enforcement of authorizations is retroactive. However, verifying whether the combination of access control and coordination protocols preserves the data consistency is a hard task since it requires examining a large number of situations. In this paper, we specify this access control protocol in the first-order relational logic with Alloy, and we verify that it preserves the correctness of the system on which it is deployed, namely that the access control policy is enforced identically at all participating user sites and, accordingly, the data consistency remains still maintained.
Type de document :
Communication dans un congrès
Charles Pecheur and Michael Dierkes. 18th International Workshop on Formal Methods for Industrial Critical Systems, Sep 2013, Madrid, Spain. Springer, 8187, pp.184-198, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-41010-9_13〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00917001
Contributeur : Abdessamad Imine <>
Soumis le : mercredi 11 décembre 2013 - 10:20:58
Dernière modification le : jeudi 11 janvier 2018 - 06:24:26

Identifiants

Citation

Aurel Randolph, Abdessamad Imine, Hanifa Boucheneb, Quintero Alejandro. Specification and Verification Using Alloy of Optimistic Access Control for Distributed Collaborative Editors. Charles Pecheur and Michael Dierkes. 18th International Workshop on Formal Methods for Industrial Critical Systems, Sep 2013, Madrid, Spain. Springer, 8187, pp.184-198, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-41010-9_13〉. 〈hal-00917001〉

Partager

Métriques

Consultations de la notice

214