Convergence et sécurité d'accès dans les systèmes d'édition collaborative massivement répartis

Parmi les défis des systèmes d'édition collaborative figure la cohérence des objets partagés. Dans la perspective d'une édition cohérente, le système doit garantir la convergence. Pour assurer la cohérence des objets partagés, la littérature propose plusieurs solutions. Les différentes approches majeures proposées sont : l'approche des types de données commutatives répliquées (CRDT) et l'approche de la transformée opérationnelle (OT). L'approche CRDT considère des opérations commutatives qui peuvent être exécutées dans un ordre différent. L'une des difficultés auxquelles CRDT se bute réside en la commutativité des opérations. Toutes les opérations d'édition doivent être commutatives afin d'être exécutées dans un ordre quelconque. L'approche de la transformée opérationnelle quant à elle propose une transformation des opérations distantes reçues par rapport aux opérations qui lui sont concurrentes ; même si elles sont déjà exécutées. Pour effectuer les transformations, l'approche OT utilise un algorithme de transformation inclusive (IT). Dans la littérature, plusieurs travaux ont prouvé que les principaux algorithmes de transformation inclusive proposés ne satisfont pas le critère de convergence. Outre la cohérence, la sécurisation des interactions est un autre défi des systèmes d'édition collaborative. Le contrôle d'accès est l'un des modèles de politiques de sécurité applicable dans ce cadre. Il s'agit d'autoriser ou d'interdire l'édition à certains utilisateurs. Le contrôle d'accès doit être uniformément déployé pour éviter de compromettre la cohérence des opérations d'édition. Une opération d'édition valide sur un site doit l'être partout. Une opération refusée sur un site doit être refusée partout. Dans le contexte étudié, le protocole de sécurité est fiable s'il préserve la cohérence du système. Fournir cette preuve de fiabilité est une tâche ardue. Le nombre de cas à examiner est infini. De plus, pour une vérification automatique, le défaut de ressources survient si des techniques appropriées ne sont pas exploitées. Dans cette thèse, nous nous intéressons aux défis que constituent la convergence et le contrôle d'accès dans les systèmes d'édition collaborative répartis. Nous considérons un objet textuel à structure linéaire qui est massivement édité dans une architecture répartie. L'approche de gestion de cohérence utilisée est la transformée opérationnelle. Ainsi, chaque utilisateur a sa copie locale du document partagé. Les opérations générées sur un site sont aussitôt diffusées aux autres utilisateurs. Elles peuvent être exécutées dans un ordre quelconque. Les types d'opérations d'édition sont : l'insertion d'un caractère et la suppression de caractère. Nous intégrons également un protocole de contrôle d'accès à l'édition collaborative. Notre thèse se présente sous la forme de trois articles scientifiques, chacun traitant d'une problématique bien spécifique. Dans le premier article, nous abordons la problématique de la convergence. Nous avons adopté une démarche en plusieurs étapes. Une exploration a été initialement faite afin de vérifier s'il est possible d'avoir une fonction IT convergente. En utilisant la méthode de la synthèse de contrôleur et les automates de jeu, nos investigations ont révélé qu'aucune IT basée uniquement sur le caractère et la position ne peut garantir une convergence. L'identification des causes de divergence a permis d'amorcer la résolution du « problème de synthèse de contrôleur ». Ainsi, un troisième paramètre a été ajouté aux opérations d'insertion. Il permet de manipuler le nombre de caractères supprimés avant la position d'insertion indiquée. Une fonction de détermination de la valeur de ce paramètre a été proposée. Une fonction IT a été par la suite proposée, en tenant compte des propositions précédentes. En utilisant la vérification sur modèle (model-checking), la preuve a été apportée que notre IT garantit bien la convergence. Le deuxième article propose l'intégration d'un protocole de sécurité optimiste. L'article aborde la problématique de la fiabilité du protocole dans un espace d'états infini. Il est déployé au dessus de protocole de synchronisation du système d'édition collaborative. Nous faisons l'hypothèse que le système vérifie la propriété de cohérence en l'absence du contrôle d'accès. Pour affronter les difficultés relatives à la preuve de fiabilité, l'approche du model-checking symbolique a été préférée. Le model-checking borné a été utilisé avec l'outil Alloy. L'exploration faite pour des instances dont la taille maximale est de treize « signatures », a permis de conclure la préservation de la cohérence par le protocole de contrôle d'accès. Notons que ces instances ne sont pas massives mais la combinatoire résultante n'est pas négligeable. Le troisième article aborde la problématique de réduction de système. Des investigations ont été menées afin d'avoir un modèle fini équivalent au système d'édition collaborative, au regard de la propriété de cohérence. Le modèle abstrait proposé comporte trois sites coopératifs, dont l'un est administrateur. Ce modèle à espace d'états fini étant prouvé équivalent par rapport à la propriété de cohérence, au système à espace d'états infini, il a servi de cadre pour la vérification automatique. En utilisant l'outil Uppaal et le formalisme d'automate, nous avons prouvé par model-checking que le modèle abstrait préserve la cohérence. Par conséquent, le protocole de contrôle d'accès préserve la cohérence de système d'édition collaborative. Nos travaux comportent quelques limitations liées à leur portée. Nous avons manipulé des objets textuels à structure linéaire sur lesquels ne sont appliquées que des opérations d'insertion et de suppression de caractères. De plus, la gestion des droits d'accès est basée sur un modèle mono-administrateur. La performance du protocole de contrôle d'accès n'a pas non plus été prise en compte. Les travaux auraient sans doute plus d'envergure s'ils couvraient plusieurs types d'objets, plusieurs types d'opérations d'édition, plusieurs administrateurs et une étude de performance. Nos futures travaux pourraient être consacrés à l'élargissement de la portée de la présente thèse.