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

Aurel Randolph 1 Abdessamad Imine 2 Hanifa Boucheneb 1 Quintero Alejandro 3
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 (UMR 6174), 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.
Complete list of metadatas

https://hal.inria.fr/hal-00917001
Contributor : Abdessamad Imine <>
Submitted on : Wednesday, December 11, 2013 - 10:20:58 AM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM

Links full text

Identifiers

Citation

Aurel Randolph, Abdessamad Imine, Hanifa Boucheneb, Quintero Alejandro. Specification and Verification Using Alloy of Optimistic Access Control for Distributed Collaborative Editors. FMICS 2013 - 18th International Workshop on Formal Methods for Industrial Critical Systems, Sep 2013, Madrid, Spain. pp.184-198, ⟨10.1007/978-3-642-41010-9_13⟩. ⟨hal-00917001⟩

Share

Metrics

Record views

454