La sécurité et la privacy dans les réseaux 5G – MobiS5

Pour tous les objectifs présentés à la section 3.1, nous utilisons les approches combinées de la sécurité prouvable, des implémentations sécurisées et de la validation expérimentale. Nous décrivons plus en détail certaines de ces approches, ainsi que leurs similitudes et leurs différences ci-dessous. Nous tenterons en particulier de souligner la complémentarité entre ces méthodologies, et la manière dont elles contribueront à nous donner une image complète - non seulement des exigences de la sécurité de la 5G - mais aussi de la faisabilité et des propriétés concrètes garanties par nos solutions.

Sécurité prouvable. La sécurité prouvable est un outil puissant qui permet de prouver que les primitives et les protocoles sont sûrs dès leur conception d'une manière rigoureuse et mathématique. La principale force de cette méthodologie est sa capacité à garantir qu'une primitive ou un protocole reste sûr même lorsqu'il est soumis à de nouvelles attaques arbitraires, dans le cadre du modèle contradictoire. En outre, la preuve permet d'estimer la taille des paramètres en fonction du niveau de sécurité requis. Cependant, la sécurité prouvable présente également une limitation importante : une preuve de sécurité ne peut assurer la sécurité dans la vie réelle que si le modèle de sécurité est capable de capturer la réalité des attaques réalistes. Cela conduit à un compromis entre la précision du modèle de sécurité (par rapport à la réalité) et la complexité de la preuve. L'objectif de ce projet est de fournir des solutions sûres et préservant la vie privée dès leur conception.

Analyse formelle. En 1995, G. Lowe a utilisé un outil de vérification automatique pour trouver une faille dans le célèbre protocole d'échange de clés Needham-Schroeder proposé en 1978. Ce protocole est simple, puisqu'il n'implique que trois échanges ; pourtant, l'attaque présentée (qui permet d'obtenir la clé secrète établie par les participants) avait jusqu'à présent échappé à la détection. Cet exemple célèbre a montré les avantages de l'utilisation d'outils de vérification formelle automatique pour établir la sécurité des protocoles. Au cours des dernières décennies, plusieurs outils de vérification automatique ont été conçus, par exemple Proverif, Scyther, Tamarin, Avispa. Chaque outil a sa propre approche de la vérification des protocoles cryptographiques et exploite l'importante puissance de calcul d'un ordinateur pour effectuer des analyses à des échelles beaucoup plus grandes que ce qui pourrait être fait à la main.

Analyse des canaux auxiliaires. La plupart des appareils 5G sont vulnérables à des attaques physiques, car un attaquant aura un accès physique à des appareils personnels volés ou perdus et à une variété de petits appareils connectés. En outre, l'adversaire peut être en mesure de faire fonctionner son propre logiciel sur les appareils intelligents (par exemple, une application mobile). Dans ce projet, nous avons exploité des techniques telles que Screaming Channels.

On estime que plus de 7 milliards de smartphones (https://www.statista.com/statistics/330695/number-of-smartphone-users-worldwide/) sont utilisés aujourd'hui. Avec le déploiement des réseaux 5G, les utilisateurs mobiles bénéficient de services plus rapides, plus flexibles et plus variés que jamais.

En outre, les années de la pandémie de Covid-19 ont accru la dépendance à l'égard des services mobiles.

Notre projet MobiS5 visait à relever les défis posés par l'émergence des infrastructures 5G en fournissant une boîte à outils cryptographiques pour améliorer la sécurité et la confidentialité des utilisateurs mobiles.

Voici quelques exemples de nos réalisations (par exemple) :

- l'introduction, pour la première fois, d'un échange de clés conforme à la loi et préservant la vie privée (Lawful-interception)

- une série d'analyses et d'améliorations de la messagerie asynchrone sécurisée après compromis (comme Signal)

- des applications de canaux hurlants aux dispositifs Bluetooth, y compris dans l'IdO.

- intégration des protocoles dans la norme ISO 20008-2

- attestation approfondie de service dans 5G NFV, permettant la création de confiance dans les nœuds virtualisés et les composants d'infrastructure individuellement -- dans un environnement uni-propriétaire ou multi-propriétaire-- ou séquentiellement dans l'attestation collective à distance.

En outre, nos résultats ont été intégrés dans un démonstrateur de preuve de concept centré sur un serveur sécurisé, permettant l'attestation anonyme, la détection des intrusions et des logiciels malveillants, et le traitement des données préservant la vie privée. Ce démonstrateur montre que non seulement nos solutions sont viables, mais qu'elles sont aussi efficaces.

- Travaux complémentaires sur l'échange de clés pour l'interception légale, basés sur nos solutions LIKE, à discuter dans le contexte de la norme LAKE (protocole EDHOC). Ces travaux sont menés conjointement par XLIM (Limoges) et l'équipe AIO de l'Inria.

- Orange et XLIM ont organisé un atelier sur l'attestation approfondie et les applications : crypto.orange-labs.fr/acg/workshop/workshop.php . Au cours de cet atelier, les bases des travaux futurs ont été établies. Une proposition de PRCI ANR franco-suisse intitulée PATs sera soumise suite à cette collaboration dans le cadre de l'appel ANR AAPG 2025, avec le soutien d'autres industriels tels qu'Intel.

- XLIM a organisé la deuxième édition du workshop TRUSTNET Days à Limoges en 2024. Cela a permis de présenter des sujets de recherche importants, tels que les travaux sur la délégation d'authentification, Lawful-Interception Key-Exchange, l'attestation profonde, et un cadre pour la sécurité post-compromission prouvable dans la 5G et les protocoles de messagerie asynchrones. Nous avons pu jeter les bases d'interactions futures avec des experts en cryptographie post-quantique et des technologies d'apprentissage automatique et d'intelligence artificielle.

- La mise en œuvre PoC du cas d'utilisation du serveur sécurisé est une plateforme sur laquelle de nouvelles primitives et de nouveaux protocoles peuvent être mis en œuvre.

Depuis 20 ans, les réseaux mobiles de 3ème et 4ème générations nous permettent de communiquer à haut débit, à l’aide d’un simple téléphone. L’avènement de la 5 G va nous permettre de franchir une nouvelle étape vers des communications universelles, grâce à une architecture décentralisée prenant en compte le développement massif de l’Internet des Objets (IoT).

Le 3GPP (3rd Generation Partnership Project) a publié 4 documents (TR 22.861, 862, 863, 864) définissant les contours du monde la 5G, en décrivant respectivement l’intégration de l’IoT, la gestion des communications sensibles, un réseau haut-débit amélioré et les garanties de sécurité et de confidentialité attendues d’un tel réseau. Ces documents suggèrent que, du point de vue cryptographique, les défis les plus importants sont (1) l’intégration de périphériques de faible puissance potentiellement vulnérables, (2) la sécurisation d’un réseau décentralisé et (3) la sécurisation des communications directes entre les périphériques, avec un engagement limité de l’opérateur.

Une différence importante avec les précédentes générations de réseaux mobiles est la grande diversité des périphériques qui seront intégrés dans la 5G. Ainsi, il ne s’agira pas seulement de protéger des téléphones mobiles contre d’éventuels malware ou dénis de service (DoS) mais plutôt de protéger l’intégralité des périphériques induits par l’IoT, pour éviter des cyber-attaques à très grande échelle. En effet, la transition vers la 5G ne va pas seulement combiner les risques existants, elle va également les amplifier.

Dans ce contexte, l’objectif du projet MobiS5 sera de prévoir et de contrer les menaces dont les réseaux 5G seront l’objet. Concrètement, nous construirons l’équivalent d’une boîte à outils cryptographique répondant à l’ensemble des besoins de sécurité de la 5G, dont chaque élément sera évalué tant formellement qu’expérimentalement. Ces travaux seront découpés en 3 parties distinctes, comme suit :

* Défi 1. Sécurité de l’infrastructure réseau et des périphériques, incluant la sécurité du cœur de réseau mais aussi la définition d’une sécurité de bout-en-bout permettant de répondre aux besoins d’interceptions légales ou de détection d’attaques.

* Défi 2. Définition des primitives et protocoles cryptographiques, incluant la sélection de primitives de base ainsi que la conception de protocoles d’échange de clés authentifiés, d’outils pour traiter des données chiffrées ainsi que de quelques contre-mesures post-quantiques.

* Défi 3. Applications mobiles, notamment dans le contexte du smart-home ou dans celui d’un serveur capable d’apporter son aide à des périphériques de faible puissance.

Pour chacun de ces défis, nous identifierons les besoins de sécurité et de confidentialité, avant de les formaliser au travers d’un modèle de sécurité cryptographique mais également en suivant une approche basée sur les méthodes formelles. Chaque outil cryptographique sera évalué différemment en fonction de sa nature. Pour les primitives symétriques, pour lesquelles la sécurité prouvable offre peu de garanties, nous opterons pour une cryptanalyse complète. Pour les autres, nous proposerons des preuves de sécurité correspondantes aux modèles de sécurité que nous aurons définis. Pour finir l’implémentation de chaque primitive sera également évaluée, notamment pour tester sa résistance aux attaques par des canaux auxiliaires, afin de tester les vulnérabilités qui ne sont pas prises en compte par des modèles formels.