Cérémonies de sécurité pour les systèmes socio-techniques

Contexte À l'aube de la révolution numérique, l'utilisation de la technologie était réservée aux privilégiés, par exemple des armées, des services de renseignement, des ingénieurs. Certains risques pouvaient alors être écartés, car ces spécialistes peu nombreux étaient bien formés à l'exploitation de nouveaux outils de pointe. La préoccupation de la cybersécurité était donc focalisée sur des aspects purement techniques, tels que le cassage d'un mécanisme cryptographique, par exemple. Les principales sources de menace étaient des organisations ou des individus malicieux, orientés vers une cible bien définie.

Mais avec l'invention des ordinateurs personnels et surtout de l'Internet, la technologie est à présent accessible à tous. On ne peut plus garantir que tout utilisateur applique des règles de sécurité de base et chaque usager constitue donc une menace potentielle. Même si des utilisateurs actuels ne sont pas tous malicieux, ils sont souvent inexpérimentés, inattentifs ou dépassés par les opportunités offertes par une pléthore de solutions innovantes : objets connectés, messageries instantanés, matériel embarqué, voitures autonomes, e-solutions, etc. De plus, le comportement des humains, contrairement à celui des machines, est non-déterministe et peut être facilement influencé par leur état mental (émotions, colère, stress, etc.) ou des aspects physiques ou environnementaux (météo, visibilité, etc.). Dans ce nouveau contexte de la technologie omniprésente, une solution de sécurité purement technique ne suffit plus. Il faut la remplacer par une approche interdisciplinaire où les aspects techniques, physiques, sociaux et humains peuvent tous être pris en compte.

Verrou scientifique Dans le domaine de la vérification des protocoles cryptographiques, les méthodes formelles ont fait preuve d'une grande utilité, en contribuant à la découverte de failles de sécurité dans des protocoles employés par des passeports électroniques ou des procédures d'authentification utilisés par 5G. Grâce à ces résultats, les standards commercialisés pouvaient être corrigés et sécurisés d'avantage. Néanmoins, les outils existants de vérification des protocoles ne s'intéressent généralement qu'au contenu cryptographique des messages échangés. Ils sont donc inappropriés pour analyser le comportement des systèmes appelés socio-techniques qui sont composés de briques technologiques (ordinateurs, protocoles), d'éléments physiques (objets, temps, espace) et surtout des humains avec leur état mental et émotionnel. Dans le contexte d'un système socio-technique la notion d'un protocole de communication est remplacée par celle d'une cérémonie de sécurité qui regroupe l'ensemble d'interactions entre les composants du système, y compris ses utilisateurs humains. Les cérémonies de sécurité sont alors en mesure de capturer aussi bien les attaques classiques contre les protocoles de communication, que celles reposant sur les canaux auxiliaires et l'ingénierie sociale.

L'objectif de cette thèse est de développer un paradigme de modélisation novateur ainsi que des outils informatiques dédiés permettant de spécifier des systèmes socio-techniques de manière formelle et d'analyser des cérémonies de sécurité sous-jacentes.

Le travail du doctorant consistera en :
- développement d'un langage formel permettant de modéliser des systèmes socio-techniques ;
- conception des outils de vérification pour des cérémonies de sécurité ;
- validation du modèle proposé sur des cas issus de la vie réelle : un réseau d'objets connectés domotiques partagés par plusieurs utilisateurs ; et une solution robotique destinée aux personnes en situation de handicap.