Spécification et Analyse d’un Protocole de Contrôle d’Accès Optimiste pour Éditeurs Collaboratifs Répartis

National audienceLes éditeurs collaboratifs répartis sont des systèmes interactifs dans lesquels des utilisateurs géographiquement éloignés éditent simultanément des documents partagés. Généralement, ces systèmes ont recours à la réplication de données et un protocole de synchronisation, qui permet d’assurer la cohérence des données même si les mises à jour des utilisateurs ne sont pas exécutées dans le même ordre sur les différentes copies. Contrôler l’accès dans les éditeurs collaboratifs est un défi car ils nécessitent un changement dynamique des droits d’accès et une faible latence pour partager les documents. Dans (Imine et al., 2009), un protocole flexible de contrôle d’accès a été proposé. Il est basé sur la réplication du document partagé ainsi que ses autorisations d’accès dans la mémoire locale de chaque utilisateur. Pour faire face à la latence et au changement dynamique des droits d’accès, une technique optimiste a été utilisée qui consiste à appliquer de manière rétroactive les autorisations d’accès. Cependant, vérifier que l’utilisation combinée du contrôle d’accès et du protocole de synchronisation préserve la cohérence des données est une tâche difficile, car elle requiert d’examiner un grand nombre de cas. Dans ce papier nous montrons comment spécifier et vérifier formellement, en utilisantla suite d’outils Alloy, un protocole de contrôle d’accès conçu pour les éditeurs collaboratifs répartis. L’analyse a permis de conclure que le contrôle d’accès est uniformément appliqué sur tous les sites participant à l’édition et, par conséquent, le protocole préserve la cohérence. Plusimportant encore, cette analyse a conduit à valider certains choix conceptuels du protocole.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 synchronization 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. In (Imine et al., 2009), a flexible access control protocol is proposed; 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, an optimisticaccess control technique is used where enforcement of authorizations is retroactive. However, verifying whether the combination of access control and synchronization protocol preserves the data consistency is a hard task since it requires examining a large number of situations.In this paper, we show how to specify and verify formally an access control protocol designed for Distributed Collaborative Editor. The analysis let to conclude that the protocol preserves consistency in such a way that the access control policy is enforced identically at all participating user sites. Most importantly, this analysis enables us to validate some conceptual choices of the protocol