Sujet du stage : vérification formelle de mécanismes de contrôle d’accès

Au sein de l’Institut de Recherche Technologique SystemX, situé au cœur du campus scientifique d’excellence mondiale de Paris-Saclay, vous prendrez une part active au développement d’un centre de recherche technologique de niveau international dans le domaine de l’ingénierie numérique des systèmes. Adossé aux meilleurs organismes de recherche français du domaine et constitué par des équipes mixtes d’industriels et d’académiques, ce centre a pour mission de générer de nouvelles connaissances et solutions technologiques en s’appuyant sur les percées de l’ingénierie numérique et de diffuser ses compétences dans tous les secteurs économiques.

Vous serez encadré par un.e ingénieur.e-chercheur.euse SystemX de l’équipe Ingénierie Système et Sûreté de fonctionnement.

Vous travaillerez au sein du projet de recherche Modélisation et Simulation d’un système de navettes Autonomes (MSA) en partenariat avec le groupe industriel Transdev.

Le poste est basé à l’IRT SystemX – Palaiseau

Présentation du sujet du stage

Contexte

La mise en place d’une Politique de Sécurité du Système d’Information (PSSI) [FSD08] passe par une politique de sécurité des données qui repose sur une protection des données sensibles. Les données sensibles font plus particulièrement l’objet d’une protection au niveau du contrôle d’accès, du traitement, du stockage, du transport ou de l’échange pour en assurer la confidentialité.

Tel qu’exposé dans le document Authentication, Authorisation & Accountability CyBOK Knowledge Area [Gollmann21], il existe un large éventail de langages dans lesquels les administrateurs peuvent spécifier des politiques de contrôle d’accès. Plusieurs types de modèles de sécurité ont été proposés et en particulier des types de contrôle d’accès [Coma09]. Ces modèles définissent des politiques abstraites de sécurité pour garantir la satisfaction des propriétés spécifiques à implanter dans les systèmes. Ils peuvent être centralisés (ex. MAC [Fayad01]), décentralisés (ex. DAC [DoD85]) ou s’adapter au facteur d’échelle (grands nombres d’utilisateurs ou de ressources à gérer) avec des notions comme les rôles (ex. RBAC [Sandhu96], ou ses variantes [Ferraiolo01] – contrôle d’accès statique), ou les attributs (ex. ABAC [Yuan05, Fernandez19, Chakraborty20] – modèle d’accès contextuel).

Les politiques doivent être précises, non ambiguës, explicites, cohérentes et consistantes. Une politique de sécurité est décrite par des objectifs de sécurité qui se déclinent en un ensemble de propriétés de sécurité. Ces dernières peuvent être définies sous une forme littéraire (approche classique) ou formelle (approche visée par notre étude), et sont regroupées en trois grandes classes [DoD85] : confidentialité (non-occurrence de divulgations non autorisées de l’information), intégrité (non-occurrence d’altérations inappropriées de l’information) et disponibilité (accessibilité et temps de réponse des services).

Description du stage

L’étude concerne la confidentialité, et plus particulièrement la vérification et la validation formelle de politiques de contrôle d’accès. En effet, elle se place dans le contexte d’une mise en œuvre de Keycloak, un logiciel permettant d’instaurer une méthode d’authentification unique au travers de la gestion par identité et par accès. Keycloak prend en charge des politiques d’autorisation et est capable de combiner différents mécanismes de contrôle d’accès tels que (liste non exhaustive) :

  • le contrôle d’accès basé sur les rôles (Role-based Access Control – RBAC) ;
  • le contrôle d’accès basé sur les attributs (Attribut Based Access Control – ABAC) ;
  • le contrôle d’accès basé sur l’utilisateur (User Based Access Control – UBAC) ;
  • le contrôle d’accès basé sur le contexte (Context Based Access Control – CBAC).

Un certain nombre de travaux se sont intéressés à la validation du contrôle d’accès, et notamment au modèle historique RBAC (ex. [Jha08]), suivant des approches visant à réaliser une validation de contraintes statiques (ex. [Abdallah06, Yuan06, Zao03]), ou de validation de contraintes dynamiques (ex. [Ledru11, Yu09]). Le spectre des méthodes va d’approches déductives (Ex. B, Z, Coq cf. réfs. ci-avant), au model checking (ex. [Mondal08]).

Dans une première phase, l’objectif du stage est de recenser et cartographier les approches formelles existantes autour de ces quatre mécanismes. La réalisation d’un tel état de l’art nécessite la mise en œuvre d’une démarche de recherche bibliographique et de synthèse.

La seconde phase du stage portera sur une mise en œuvre d’une validation formelle d’un mécanisme de contrôle d’accès choisi par le partenaire du projet, et ce, afin de participer au dossier de justification de la solution retenue. Il s’agira de vérifier formellement que les politiques d’administration du contrôle d’accès sont conformes aux règles de sécurités, et donc de réaliser un modèle et de décliner les propriétés d’accès dans le cadre formel choisi. Il n’y a pas de contrainte a priori sur l’approche de formalisation. En résumé, les missions sont :

  • La réalisation d’un état de l’art sur l’application des méthodes formelles aux mécanismes de contrôle d’accès ;
  • La mise en œuvre d’une approche de validation formelle sur un des quatre mécanismes dans un cadre formel, dans le contexte applicatif du projet.

Références bibliographiques

[FSD08] Guide d’élaboration d’une PSSI opérationnelle d’unité, Référence 08.2378/FSD, CNRS/FSD/Sécurité des Systèmes d’Information En date du 23 mai 2008.

[Gollmann21] D. Gollmann, The Cyber Security Body of Knowledge. University of Bristol, 2021, ch. Authentication, Authorisation & Accountability, version 1.0.2. [Online]. Available: https://www.cybok.org/

[DoD85] Technical Report DoD 5200.28-STD. Trusted Computer System Evaluation Criteria. Department of Defense, 1985.

[Fayad01] Amgad Fayad, Sushil Jajodia, Don Faatz, and Vinti Doshi. Going beyond mac and dac using mobile policies. In 16th international conference on Information security: Trusted information (Sec ’01), pages 245:260, 2001.

[Coma09] Céline Coma. Interoperabilité et cohérence de politiques de sécurité pour les systèmes auto-organisants. In Thèse de doctorat, Telecom Bretagne, April 2009.

[Sandhu96] Ravi S. Sandhu, Edward J. Coyne, Hal L. Feinstein, and Charles E. Youman. Role-based access control models. Computer, 29(2): 38 :47, 1996.

[Ferraiolo01] David F. Ferraiolo, Ravi Sandhu, Serban Gavrila, D. Richard Kuhn, and Ramaswamy Chandramouli. Proposed nist standard for role-based access control. In ACM Transactions on Information and System Security, volume 4, pages 224:274, Août 2001.

[Yuan05] Eric Yuan and Jin Tong. Attributed based access control (ABAC) forWeb services. In IEEE International Conference on Web Services (ICWS’05), July 11-15 2005.

[Abdallah06] Abdallah, A. E. et E. J. Khayat. 2006, «Formal Z Specifications of Several Flat Role-Based Access Control Models», dans 2006 30th Annual IEEE/NASA Software Engineering Workshop, ISSN 1550-6215, p. 282–292

[Yuan06] Yuan, C., Y. He, J. He et Z. Zhou. 2006, A Verifiable Formal Specification for RBAC Model with Constraints of Separation of Duty, Springer Berlin Heidelberg, Berlin, Heidelberg, ISBN 978-3-540-49610-6, p. 196–210.

[Zao03] Zao, J., H. Wee, J. Chu et D. Jackson. 2003, «RBAC schema verification using lightweight formal model and constraint analysis», dans Proceedings of the 8th ACM Symposium on Access Control Models and Technologies, SACMAT ’03, ACM.

[Ledru11] Ledru, Y., N. Qamar, A. Idani, J.-L. Richier et M.-A. Labiadh. 2011, «Validation of security policies by the animation of z specifications», dans Proceedings of the 16th ACM Symposium on Access Control Models and Technologies, SACMAT ’11, ACM, New York, NY, USA, ISBN 978-1-4503-0688-1.

[Yu09] Yu, L., R. France, I. Ray et S. Ghosh. 2009, «A rigorous approach to uncovering security policy violations in uml designs», dans Proceedings of the 2009 14th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS ’09, IEEE Computer Society, Washington, DC, USA, ISBN 978-0-7695-3702-3, p. 126–135.

[Mondal08] Mondal, S. et S. Sural. 2008, A Verification Framework for Temporal RBAC with Role Hierarchy (Short Paper), Springer Berlin Heidelberg, Berlin, Heidelberg, ISBN 978-3-540-89862-7, p. 140–147.

[Fernandez19] Fernandez, M., Mackie, I., and Thuraisingham, B. (2019). Specification and Analysis of ABAC Policies via the Category-Based Metamodel. In Proc. 9th ACM Conf. on Data and App. Secur. and Priv., pages 173–184.

[Chakraborty20] Chakraborty, S., Sandhu, R., and Krishnan, R. (2020). On the Feasibility of RBAC to ABAC Policy Mining: A Formal Analysis. In Proc. 8th Int. Conf. on Sec. Knowl. Managem. in Artific. Intell. Era, pages 147–163.

[Jha08] S. Jha, N. Li, M. Tripunitara, Q. Wang and W. Winsborough, « Towards Formal Verification of Role-Based Access Control Policies, » in IEEE Transactions on Dependable and Secure Computing, vol. 5, no. 4, pp. 242-255, Oct.-Dec. 2008, doi: 10.1109/TDSC.2007.70225.

Profil et compétences

De formation : BAC +5/école d’ingénieur 3ème année dans le domaine de la vérification formelle des systèmes. Une connaissance en cybersécurité (politique d’accès) sera largement appréciée.

Compétences :

  • Méthodes formelles : approches déductives, vérification de logiciel/système.

Aptitudes personnelles :

  • Bon relationnel.
  • Curiosité, esprit d’initiative, capacité d’analyse et rigueur.

 

L’IRT SystemX est engagé en faveur de l’égalité des chances. A ce titre, tous nos postes sont ouverts aux candidats en situation de handicap.

Informations clés

Durée du stage : 6 mois
Date de démarrage envisagée : février-mars 2022
Localisation du poste : Cluster Paris Saclay (91)
Référence de l’offre : DSR-2022-17-MSA


Postuler à cette offre d’emploi


Mots-clés :


Partager cette offre d’emploi :

Inscrivez-vous à la newsletter de l'IRT SystemX

et recevez chaque mois les dernières actualités de l'institut :