SECSI: Sécurité des systèmes d'information
Thématiques de recherche
Dans notre société numérique, la nécessité d'assurer la sécurité des systèmes informatiques semble évidente. Si certains enjeux de sécurité sont anciens (paiment en ligne, citoyenneté numérique, etc.), leur forme évolue rapidement et de nouvelles problématiques apparaissent avec le développement de nouvelles technologies et de nouvelles pratiques, chez les utilisateurs, les industriels et même les acteurs étatiques. En particulier, la multiplication des traces numériques engendre des craintes légitimes concernant la protection de la vie privée: on pense en particulier aux trackers sur le web, au développement de la téléphonie mobile, aux réseaux sociaux, au paiement sans contact et autres cartes RFID, etc.
La thématique principale de l'axe de recherche SECSI est l'utilisation de méthodes de vérification issues de la logique telles que la démonstration automatique, les équivalences observationnelles dans les algèbres de processus et la théorie des domaines, appliquées aux protocoles visant à assurer la sécurité des systèmes. Nous développons également des techniques formelles pour la sécurité des réseaux, en particulier la détection d'intrusion.
Membres
Membres permanents | ||
|
David Baelde
Assistant professor, ENS Paris-Saclay |
Caroline Fontaine
Researcher, CNRS |
|
|
Hubert Comon-Lundh
Professor, ENS Paris-Saclay |
Jean Goubault-Larrecq
Professor, ENS Paris-Saclay |
|
Membres détachés, associés ou temporaires | ||
|
Xiaodong Jia
Post-doctoral researcher, Digicosme |
Zhenchao Lyu
Post-doctoral researcher, Digicosme |
|
Doctorants | ||
|
Charlie Jacomme
PhD student, ENS Paris-Saclay |
Adrien Koutsos
PhD student, ENS Paris-Saclay |
|
Présentation détaillée
L'axe de recherche SECSI porte sur la vérification de propriétés de sécurité. Nous présentons ci-dessous les principales problématiques auxquelles nous nous intéressons.
Propriétés du type respect de la vie privée
Les propriétés ayant trait à la vie privée, comme l'anonymat ou la non-traçabilité
des utilisateurs, sont particulièrement délicates à analyser. Formellement,
elles s'expriment par le biais d'équivalences comportementales de protocoles,
dont la vérification automatique est encore toute jeune.
De nombreuses applications avec un fort enjeu sociétal sont concernées,
par exemple le vote électronique,
ou les puces RFID présentes dans de nombreux objets comme le passeport
électronique.
L'équipe (co-)développe plusieurs outils automatisant l'analyse de ce type de propriétés:
- SAT-Equiv est un vérificateur d'équivalences très efficace, s'appuyant sur les solveurs SAT et des techniques de planning.
- UKano est un vérificateur d'anonymat et de non-traçabilité pour des protocoles à deux agents, offrant des garanties pour des exécutions non bornées.
- Akiss et APTE vérifie l'équivalence de traces pour des exécutions bornées, chacun supportant une large classe de protocoles; en particulier, Akiss supporte la primitive xor.
Garanties dans le monde calculatoire
En cryptographie, les modèles de sécurité standards sont calculatoires: les messages sont des chaînes de bits, les attaquants sont des machines probabilistes s'exécutant en temps polynomial, dont on doit montrer que les chances de succès sont négligeables. De tels modèles sont plus réalistes que les modèles symboliques, et permettent a priori de rendre compte de plus d'attaques, mais se prêtent généralement moins bien à la vérification automatique.
Bana et Comon ont proposé une approche pour conduire des preuves formelles automatisables et valides dans le modèle calculatoire. Il s'agit en bref d'axiomatiser ce que l'attaquant ne peut pas faire plutôt que ce qu'il peut faire. Cette méthode a été developpée dans le cadre de la thèse de G. Scerri et du prototype SCARY, pour les preuves d'accessibilité. Elle est en développement pour les preuves d'indistinguabilité calculatoire.
Détection d'intrusion
Malgré les avancées présentées ci-dessus, on ne peut pas aujourd'hui garantir l'absence d'attaques sur un système informatique complexe. Des techniques telles que la détection d'intrusion vont alors être utilisées pour reconnaître les comportements anormaux typiquement liés à une attaque.
Nous développons la plateforme de détection d'intrusion ORCHIDS, dont le coeur est un algorithme de model-checking analysant à la volée les séquences d'évènements ayant lieu sur un système informatique. ORCHIDS est un projet open-source, et regroupe une communauté comprenant la DGA, l'ANSSI, Bertin, Thalès, EADS, l'UQàM.
Suivant une approche différente, l'outil NetQi implémente un algorithme de model-checking pour les jeux d'anticipation, permettant de prédire des attaques et proposer des contre-mesures.
Projets
En cours
- ANR TECAP, Protocol Analysis - Combining Existing Tools (2018-2022).
- ANR-FNR Sequoia, Security properties, process equivalences and automated verification (2015-2019).
- Convention INRIA-DGA 12 81 0312, Prototypage d'une sonde de détection d'intrusions.
Et passés
- ANR JCJC VIP, Vérification de propriétés d'indistinguabilité (2012-2016).
- ANR VERSO ProSe, Protocoles de sécurité : modèle formel, modèle calculatoire, et implémentations.
- INRIA project lab CAPPRIS, Collaborative Action on the Protection of Privacy Rights in the Information Society.
- ANR Programme Blanc CPP, Confidence, Proof and Probabilities (2009-2013).
- Projet ARA SESUR AVOTÉ, Analyse formelle de protocoles de vote électronique (2008-2011).
- Projet PFC (Plateforme de Confiance) du pôle de compétitivité System@tic Paris Region (2007-2010).
- Projet ARA SSIA Formacrypt (2006-2009). .
