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

Permanent Members

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

Associated and Temporary Members

Xiaodong Jia
Post-doctoral researcher, Digicosme
Zhenchao Lyu
Post-doctoral researcher, Digicosme
 

Ph.D. Students

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:

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

Et passés

About LSV

Presentation of SECSI

SECSI presentation at AERES (2013)

Recent Publications

All the SECSI publications

A. DallonVerification of indistinguishability properties in cryptographic protocols - Small attacks and efficient decision with SAT-Equiv.  Thèse de doctorat, École Normale Supérieure Paris-Saclay, France, November 2018. PDF | BibTeX )
D. Baelde, A. Lick and S. SchmitzDecidable XPath Fragments in the Real WorldIn PODS'19. ACM Press, June 2019. To appear. Web page | BibTeX )
V. Cortier, A. Dallon and S. DelauneEfficiently Deciding Equivalence for Standard Primitives and PhasesIn ESORICS'18, LNCS 11098, pages 491-511. Springer, September 2018. Web page | PDF | PDF (long version) | BibTeX )
D. Baelde, S. Delaune and L. HirschiPOR for Security Protocol Equivalences - Beyond Action-DeterminismIn ESORICS'18, LNCS 11098, pages 385-405. Springer, September 2018. Web page | BibTeX )
G. Barthe, X. Fan, J. Gancher, B. Grégoire, C. Jacomme and E. ShiSymbolic Proofs for Lattice-Based CryptographyIn CCS'18. ACM Press, October 2018. To appear. BibTeX )

All the SECSI publications