SECSI: Sécurité des systèmes d'information

Thématiques de recherche

Les attaques contre les ordinateurs personnels (virus, spam, etc.), le paiement en ligne, les téléphones portables… devenant de plus en plus fréquentes, la sécurité est aujourd'hui un sujet crucial. 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 Cachan
Stéphanie Delaune
Researcher, CNRS
 
Hubert Comon-Lundh
Professor, ENS Cachan
Jean Goubault-Larrecq
Professor, ENS Cachan

Associated and Temporary Members

Amina Doumane
PhD student, Région Île-de-France (joint with Paris 7)
Ivan Gazeau
Post-doctoral researcher, ANR VIP
Pierre-Arnaud Sentucq
Engineer, INRIA

Ph.D. Students

Antoine Dallon
PhD student, DGA
Jérémy Dubut
PhD student, ENS Cachan
Lucca Hirschi
PhD student, ENS Cachan

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.


Plusieurs outils ont été developpés pour automatiser 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 prettent généralement moins bien à la vérification automatique. On se demande alors naturellement dans quelles circonstances la sécurité dans le modèle symbolique entraîne la sécurité dans le modèle calculatoire. Nous nous intéressons au développement de tels résultats, mais aussi de cadres généraux permettant de les comprendre et les composer. Une autre direction que nous explorons est l'utilisation du modèle de Comon-Bana qui vise à réconcilier la précision du modèle calculatoire avec la possibilité d'approches automatiques, en axiomatisant ce que l'attaquant ne peut pas faire plutôt que ce qu'il peut faire.

API de sécurité

Les API de sécurité utilisées dans des périphériques tels que les tokens de sécurité USB, distributeurs automatiques de billets, smartcards, etc. constituent un chaînon important de la sécurité des systèmes. Grâce à des avancées théoriques récentes, nous avons montré qu'il est possible de vérifier automatiquement diverses API ainsi que leurs implémentations.

Les travaux dans ce domaine ont mené à l'outil Tookan et à la startup Cryptosense.

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

About SECSI

A joint team with

Logo INRIA Saclay

Presentation of SECSI (2013)

SECSI presentation at AERES (2013)

Recent Publications

All the SECSI publications

J. Dubut, É. Goubault and J. Goubault-LarrecqThe Directed Homotopy HypothesisIn CSL'16, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, September 2016. To appear. BibTeX )
A. Doumane, D. Baelde and A. SaurinInfinitary proof theory: the multiplicative additive caseIn CSL'16, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, September 2016. To appear. BibTeX )
J. Dubut, É. Goubault and J. Goubault-LarrecqBisimulations and unfolding in P-accessible categorical modelsIn CONCUR'16, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, August 2016. To appear. PDF | BibTeX )
J. Dubut, É. Goubault and J. Goubault-LarrecqDirected homology theories and Eilenberg-Steenrod axiomsApplied Categorical Structures, 2016. To appear. PDF | BibTeX )
J. Goubault-Larrecq and S. SchmitzDeciding Piecewise Testable Separability for Regular Tree LanguagesIn ICALP'16, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, July 2016. To appear. Web page | BibTeX )

All the SECSI publications