Laboratoire Spécification et Vérification

Fondé en 1997, le Laboratoire Spécification et Vérification (LSV) est le laboratoire d'informatique de l'ENS de Cachan, et est aussi affilié au Centre National de la Recherche Scientifique (CNRS) en tant qu'UMR 8643. La recherche au LSV est centrée sur la vérification de logiciels et systèmes critiques, et sur la vérification de la sécurité des systèmes informatiques.

À la une

LSV 20th Year Anniversary

Visiter le site web pour cet événement

In celebration of two decades of activity, LSV is hosting a workshop to look back at achievements in our field and to discuss challenges ahead. The programme include invited talks by partners and members of the laboratory.

Members, former members, and other interested colleagues are cordially invited to join us in Cachan on 11 and 12 May. Attendance is free, but registration is required.


Actualités

Hubert Comon membre senior de l'IUF

Visiter le site web pour cet événement

Hubert Comon named Senior Member of Institut Universitaire de France

Hubert Comon est nommé membre senior de l'Institut universitaire de France à compter du 1er octobre 2016 pour une durée de 5 ans. Il mettra en oeuvre un projet de recherche sur les methodes formelles pour la sécurité informatique.


Un ancien du LSV casse l'algorithme cryptographique SHA1

Visiter le site web pour cet événement

Elie Bursztein, ancien doctorant du LSV sous la direction de Jean Goubault-Larrecq, et à la tête de l'"anti-abuse research team" chez Google, Inc., à Mountain View, CA, USA, vient de démontrer une faille majeure dans l'algorithme cryptographique SHA1, dans un travail commun entre son équipe et le CWI d'Amsterdam. Cette attaque, produite par une combinaison de techniques récentes de cryptanalyse exécutées sur des clusters de CPU et des clusters de GPU chez Google, permet de produire des documents contrefaits.

Elle a des conséquences importantes du fait que SHA1 est utilisé couramment pour la sécurisation des sites Web et notamment des sites marchands (SSL/TLS), du courrier électronique (PGP/GPG), des systèmes de sauvegarde sécurisés, ou dans des outils courants comme Git. Son coût, estimé à seulement 110 000 dollars, la rend accessible en pratique.

Les détails concernant cette attaque sont disponibles sur le site de la collaboration: shattered.io.


Motion sur l'instauration du Fichier TES

Visiter le site web pour cet événement

Le Laboratoire Spécification et Vérification (LSV), laboratoire d'informatique de l'ENS Paris-Saclay et du CNRS affirme que l'instauration du nouveau fichier "titres électroniques sécurisés" prévue par le décret №2016-1460, comporte un risque inhérent majeur d'attaque, vol et détournement à l'heure où les attaquants informatiques disposent de moyens considérables et croissants. Le LSV ne connaît pas de solution technique centralisée permettant de réaliser toutes les fonctionnalités prévues par le décret tout en garantissant la confidentialité des données des citoyens.


Propositions de thèses et post-doctorats au LSV

Voir les propositions de stage

Les candidatures en thèse dans les thématiques du LSV sont bienvenues. Nous proposons en particulier des thèses et des post-doctorats financés :

Publications Récentes

Visiter le site web associé S'abonner au flux RSS des publications du LSV

L. HirschiAutomated Verification of Privacy in Security Protocols: Back and Forth Between Theory & Practice.  Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, April 2017. PDF | BibTeX )
C. Aiswarya, B. Bollig and P. GastinAn Automata-Theoretic Approach to the Verification of Distributed AlgorithmsInformation and Computation, 2017. To appear. PDF | BibTeX )
D. StanRandomized Strategies in Concurrent Games.  Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, March 2017. Web page | PDF | BibTeX )

À propos du LSV

Contacter le LSV

Exporter l'adresse au format vCard | Informations d'accès

photo LSV
Adresse
LSV, CNRS & ENS de Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex, France
Téléphone
+33 1 47 40 75 20
Fax
+33 1 47 40 75 21

Informations d'accès

Agenda

Exporter l'agenda au format iCalendar | Page des séminaires du LSV

mar. 13 juin
mar. 20 juin
mar. 27 juin
mar. 11 juillet
mar. 3 octobre

Distinctions

EATCS Distinguished Dissertation Award 2016

Visiter le site web pour cet événement

EATCS Distinguished Dissertation Award 2016

Georg Zetzsche a reçu le Prix de thèse distingué 2016 dé'cerné par l'EATCS pour sa thèse intitulée Monoids as storage mechanisms soutenue à l'Université de Kaiserslautern en Allemagne.


Prix EASST du meilleur article à ETAPS 2016

EASST Best Paper Award at ETAPS 2016

Véronique Cortier, Antoine Dallon et Stéphanie Delaune ont reçu le prix EASST du meilleur article à ETAPS 2016 pour leur article intitulé Bounding the number of agents, for equivalence too et présenté à POST 2016.


Stéphanie Delaune - ERC Starting Grant

Visiter le site web pour cet événement

Stéphanie Delaune  
 awarded ERC Starting Grant

Nous félicitons Stéphanie Delaune pour son ERC Starting Grant POPSTAR - Physical properties Of security Protocols with an Application To contactless Systems. L'objectif principal du projet est de développer les fondations et les outils pour analyser les protocoles modernes dont la sécurité repose sur des propriétés du monde physique. Ce project est ambitieux. Le but est de garantir un bon niveau de sécurité dans les applications et les systèmes sans contact, et ainsi répondre aux attentes des consommateurs et des citoyens.

Stéphanie a été chargée de recherche CNRS au LSV depuis 2007 ; elle a rejoint l'équipe EMSEC à IRISA, Rennes en septembre 2016. Retrouvez Stéphanie sur Interstices dans un podcast intitulé : Comment sécuriser notre environnement communicant ?