Formal methods applied to access control policy design, verification and enforcement

The evolution of classical information systems has introduced new technologies and services forinformation managing and sharing. With the spread of the Internet, it is now possible to easilyshare vast amounts of electronic information and computer resources in open distributed envi-ronments. These environments serve as a common platform for heterogeneous users by hostingservices, user applications and data. This evolution has opened new threats to informationsecurity and new challenges to access control modeling. In order to meet these challenges,many research works went towards extending traditional access control models towards mod-els tailored for managing data access and privilege definition within distributed and dynamicsystems.In this manuscript, we contribute to this line of research by introducing a modular frameworkfor the specification of interoperable access control policies developed autonomously in differentadministrative domains. The rule-based formalisation we propose allows for policy analysis andvalidation by verification of policy properties and simulation of execution scenarios. We havealso investigated access control in the context of collaborative decision making systems. In par-ticular, we propose a solution for controlling access in cooperating web services with transitivedependencies, as well as in data fusion processes. Finally, we consider authorization policiesand constraints related to workflow management systems and workflow-driven applications.We propose a methodology to monitor a workflow and its associated access control policy inorder to ensure a successful termination of the workflow or, if not possible, an execution witha minimal violation of the authorization constraints.
L’evolution des systemes d’information classiques a introduit des nouvelles technologies et desnouveaux services pour la gestion et le partage d’informations. Avec la diffusion d’Internet, ilest desormais possible de partager facilement de grandes quantites d’informations ́electroniqueset de ressources informatiques dans des environnements distribues ouverts. Ces environnementsservent de plateforme commune pour des utilisateurs heterogenes (par exemple, les entreprises,les particuliers, etc.) en h ́ebergeant des services, des applications utilisateur et des donn ́ees.Cette evolution a introduit des nouvelles menaces pour la s ́ecurit ́e de l’information et desnouveaux d ́efis pour la modelisation du contrˆole d’acc`es. Afin de relever ces d ́efis, de nombreuxtravaux de recherche etudient l’extension des mod`eles traditionnels de contrˆole d’acc`es vers desmod`eles con ̧cus pour gerer l’acces aux donn ́ees et la d ́efinition des privil`eges dans les syst`emesdistribu ́es et dynamiques.Dans ce manuscrit, nous contribuons `a cette ligne de recherche en introduisant un formalismepour la sp ́ecification de politiques de contrˆole d’acc`es interop ́erables et d ́evelopp ́ees de mani`ereautonome dans diff ́erents domaines administratifs. La formalisation `a base de r`egles que nousproposons permet l’analyse et la validation des politiques par la v ́erification des propri ́et ́estelles que la consistance et l’efficacit ́e, ainsi que la simulation de sc ́enarios d’ex ́ecution. Nousavons ́egalement ́etudi ́e le contrˆole d’acc`es dans le contexte des syst`emes avec une prise ded ́ecision collaborative. Nous proposons notamment une solution pour le contrˆole d’acc`es dansles services web cooperatifs avec des dependances transitives, ainsi que dans les processus defusion de donnees.Enfin, nous considerons les politiques d’autorisation et les contraintes liees aux systemes degestion de flux de travail (workflows) et leurs applications. Nous proposons une methodologiepour surveiller un workflow et sa politique de controle d’acces associee, afin d’en assurer laterminaison en respectant toutes les contraintes de securite ou, si ce n’est pas possible, uneexecution avec une violation minimale de ces contraintes.