Xavier Leroy : prouver l’absence de Bugs

Le 24 novembre 2016, dans les locaux de la Royal Society à Londres, Xavier Leroy reçoit le Milner Award. C’est le plus grand prix européen en informatique, décerné conjointement par la Royal Society, l’Académie des sciences, et l’Académie allemande Leopoldina en l’honneur du grand informaticien britannique Robin Milner (prix Turing 1992). Xavier Leroy est Directeur de recherche à Inria, et dirige l’équipe-projet Gallium.

Xavier Leroy © Inria/Photo G. Scagnelli
Xavier Leroy © Inria/Photo G. Scagnelli

Nous cherchons depuis longtemps des langages qui permettent d’écrire des programmes efficaces (qui arrivent rapidement aux résultats) et sûrs (avec le moins possible de bugs et de trous de sécurité). Même si plusieurs centaines de langages et plusieurs milliers de dialectes ont été introduits depuis les années 1950, la quête continue. Les langages Caml puis OCaml ont été parmi les grandes réussites dans ce domaine. (Voir l’article « Poésie et esthétisme du logiciel » de ce blog.)

Pour utiliser un langage de programmation, on a besoin d’un « compilateur ». Un compilateur pour un langage Caml, C, Java, etc., est un programme informatique qui transforme un programme écrit dans ce langage de haut niveau (le langage source) en un autre programme équivalent mais écrit en langage machine (le langage cible), donc directement exécutable par un ordinateur.

Au milieu des années 1990, Xavier Leroy, alors thésard dans l’équipe de Gérard Huet, reprit à zéro le développement d’un compilateur pour le langage Caml, une version améliorée du langage ML, le Meta-Langage de Robin Milner (celui du prix). En collaboration avec son collègue Damien Doligez, il réalisa un compilateur très simple mais très efficace d’un sous ensemble de Caml, appelé Caml-Light. Le langage Caml-Light et son compilateur se sont répandus en France pour l’enseignement de la programmation. Caml a maintenant évolué vers un langage très complet nommé Ocaml, très utilisé dans la recherche et aussi dans des industries de haute sécurité (banque, avionique, etc.).

Xavier Leroy est un développeur de système exceptionnel. Mais il a aussi apporté des contributions théoriques exceptionnelles sur les théories des types (*).

La lettre C en langage des signes

CompCert, l’autre grande contribution de Xavier Leroy et de son équipe, est une aventure encore unique sur le plan mondial. Il s’agit d’un compilateur pour le langage C, un langage de programmation développé dans les années 70 qui a eu un énorme succès. Le langage C est encore beaucoup utilisé et des langages comme C++ et Java s’en sont inspirés.

Que CompCert a-t-il de si particulier ? De si génial ? Quand on veut garantir la qualité d’un logiciel, on cherche à obtenir une « certification » de la qualité des méthodes utilisées dans son développement et des méthodes de test. Par exemple, en appliquant une norme industrielle, comme la norme avionique DO-178C, qui précise des méthodes à suivre. Si ces méthodes ont été suivies, on peut « espérer qu’il n’y a pas trop de bugs ». CompCert a lui été bel et bien « prouvé mathématiquement correct». Il n’est pas nécessaire d’espérer quoi que ce soit, de croire en quoi que ce soit, la preuve garantit formellement que le logiciel est sans aucun bug !

Un tel développement est une course de haies : il faut d’abord choisir un sous-ensemble C-light de C qui corresponde aux besoins d’industriels mais qui soit plus simple à prouver que le langage complet. Il faut ensuite formellement définir une machine cible M (en fait, plusieurs sont considérées). Enfin, il faut démontrer un théorème du genre : « pour tout programme P écrit en C, si CompCert traduit P en un code machine P’, alors exécuter P’ sur la machine M donne pour toute entrée le même résultat que celui spécifié par la sémantique formelle du langage C. » Pour faire simple : le compilateur n’introduit pas de bug.

Un bug, « insecte » en anglais

Cette preuve, très complexe, est réalisée à l’aide de l’assistant de preuves Coq développé en France et en OCaml, qui est devenu la référence du domaine. Le code qu’il génère est du même niveau d’efficacité que celui généré par les compilateurs standards. Si tout cela vous paraît un peu abstrait, voici une illustration. Un outil pour chercher des bugs dans les programmes, Csmith développé à l’Université d’Utah, a été utilisé sur CompCert et les principaux autres compilateurs C. Sur les concurrents de CompCert, il a permis de détecter des centaines de bugs. Mais aucun dans CompCert ; en fait, il en a détecté deux, dans un premier temps, mais dans les parties assez imprécises de C, et ces bugs ont été corrigés. Oui, vous avez bien lu : le compilateur n’introduit pas de bug. (Attention : rien n’empêche le programmeur d’en faire !)

Ce résultat était inimaginable il y a encore 15 ans. Être parvenu à construire CompCert est véritablement un superbe exploit scientifique et technique, qui aura beaucoup de successeurs. D’ailleurs, un groupe d’universités américaines vient de lancer un grand projet DeepSpec spécifiquement sur ce genre de sujet.

Serge Abiteboul, Inria, et Gérard Berry, Collège de France

(*) Théorie des types : En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d’alternatives à la théorie des ensembles comme fondation des mathématiques. Grosso modo, un type est une « caractérisation » des éléments qu’un terme qualifie. En théorie des types, chaque terme possède un type et les opérations décrites par le système imposent des restrictions sur le type des termes qu’elles combinent. Wikipédia, 2016.

Pour aller plus loin

 

 

Être une femme libérée c’est pas si difficile.

femme-actuelle-libereeDans le Femme Actuelle N°1676 du 7 au 13 novembre 2016, page 5, Clémence Levasseur, donne la parole au « pour » et au « contre » à propos du fait que le code informatique arrive à l’école. Décryptage.

 

Mensonges, salades ou vérité ?

Un apprentissage progressif et innovant ou un effet d’annonce ? Apprendre à prendre le contrôle sur la machine ou ajouter de nouvelles connaissances vites obsolètes ? Combattre les inégalités ou ne se concentrer que sur les fondamentaux ?

La démarche journalistique correspond à la nécessité d’informer sur ce sujet pour lequel les parents et les enseignants se posent encore beaucoup de questions.

Class’Code a fait le travail de décodage de ces opinions pour les confronter aux faits :

Expliciter ce qui correspond aux faits, ou relève d’une méconnaissance du sujet, ou correspond à une affirmation invérifiable ou maladroite.

Pour en savoir plus: c’est par ici.

 

Et qu’en pense l’éco-système de Binaire ?

sondage-femme-actuelle

Et la question sous-jacente finalement est  : les actions pour l’enseignement de l’informatique à l’école doivent-elles se poursuivre ? Mais Alan McCullagh donne la réponse de sagesse :

sondage-femme-actuelle-2Être un homme ou une femme actuelle, c’est bien, et s’initier à la pensée informatique pour être une femme ou un homme libéré par rapport au numérique, c’est peut-être pas si difficile.

Marie-Agnès Énard.

 

Les Français l’ont rêvé, les Wallons l’ont fait

Binaire poursuit la série des visites de musées informatiques. Après Londres , deux amis de Binaire sont allés « Outre-Quiévrain » pour les premiers jours du Musée de l’Informatique Pionnière en Belgique. Un historien de l’informatique, Pierre Mounier-Kuhn, CNRS & Université Paris-Sorbonne et notre correspondant en Belgique en la personne de Jean-Jacques Quisquater de l’UCL pour les photos. Pierre Paradinas

Non, il ne s’agit pas de l’opposition de Paul Magnette aux traités transatlantiques.

carteperforee
Ph : J.-J. Quisquater

Vendredi 28 octobre, à quelques pas du parlement wallon où se jouait le psychodrame belgo-canadien à propos du CETA, un nouveau Musée de l’informatique s’inaugurait à Namur. Tandis qu’en France les historiens des techniques, paléoinformaticiens et responsables du patrimoine voyaient retoqué par les pouvoirs publics leur projet, élaboré depuis quatre ans, d’un Musée de l’informatique et du numérique en France (#MINF), en Belgique un ensemble d’initiatives privées parvenaient à se fédérer pour bâtir un véritable conservatoire du traitement de l’information.

À l’origine, quatre collections belges indépendantes, constituées sur quatre sites différents. Celle des anciens de Bull Belgique, liée à la Fédération des équipes Bull, animée par Gibert Nathan à Grimbergen. Celle des anciens d’Unisys, résultant de la fusion dans les années 1980 de trois grands constructeurs historiques : Burroughs, NCR et Univac, installée par Jacques Laffut dans les sous-sols d’Unisys à Dieghem. La collection d’outils de calcul rassemblée par un ingénieur de l’université de Louvain, Jacques Lemaire. Et la collection Informatique et Bible, constituée à l’abbaye de Maredsous autour des techniques d’analyse textuelle et linguistique par le frère Ferdinand Poswick, infatigable animateur du projet et maintenant directeur du musée.

Ce petit groupe de passionnés a réussi à s’entendre sur un projet commun, impliquant un véritable transfert de souveraineté de chacun vers une nouvelle entité. Ils ont négocié avec la Fondation Roi Baudouin le financement d’un Fonds Informatique Pionnière en Belgique. Et obtenu des autorités locales la cession d’un vaste gymnase couvert, proche de l’antique citadelle de Namur entre la Sambre et la  Meuse.

Les milliers de pièces des collections rassemblées y tiennent à l’aise, dans une muséographie remarquablement conçue. De son principal animateur, grand connaisseur des langues anciennes et de l’histoire des signes, le musée tient une approche humaniste qui fait son originalité.

Embrassant l’histoire sur la longue durée, une fresque chronologique (time line) commence par  les origines de l’écriture et du calcul dans les premières civilisations du Proche-Orient. Elle évoque ensuite les différentes techniques de traitement ou de production de l’information – instruments de calcul, horlogerie, imprimerie, photographie et autres procédés aujourd’hui largement absorbés dans le « numérique ».

Le tableau chronologique est un exercice redoutable, car il met en relief la moindre erreur. Or ici l’historien le plus méticuleux (comprendre : le plus casse-pieds) ne décèle qu’une ou deux approximations hasardeuses. La principale est d’avoir qualifié Colossus de « calculateur », alors que cette première grande machine électronique digitale, installée à Blechtley Park fin 1943, était conçue pour comparer des chaînes de caractères et n’a sans doute jamais rien calculé. On peut aussi contester le cliché de « première programmeuse de l’histoire » souvent accolé à Lady Ada Lovelace : la comtesse a fait beaucoup mieux, elle a analysé un problème pour élaborer un algorithme adapté à la machine de Babbage ; celle-ci n’étant pas encore construite et n’ayant pas encore de « code » défini, on ne pouvait écrire un programme. Mais ces deux confusions étant omniprésentes dans la saga de l’informatique, on ne saurait les reprocher aux rédacteurs, au regard de l’énorme besogne qu’ils ont menée à bien.

bureau-annee90
Ph : P. Mounier Kuhn. Poste de travail des chercheurs en langues anciennes du Proche-Orient, nécessitant matériels et logiciels spéciaux (années 1990).

Je ne vais pas dresser ici un catalogue complet du musée, mais seulement partager avec les lecteurs de Binaire quelques impressions de visite. Je prévoyais de traverser rapidement la collection Burroughs de machines comptables, mais j’ai été accroché par la qualité de leur présentation, qui évoque bien un atelier de traitement bancaire des années 1930, et par l’intérêt des machines elles-mêmes, aux points de vue de la technique comme de l’esthétique industrielle. À la fin du XIXe siècle, Burroughs était si fier de ses machines qu’il les packageait sous un capot vitré afin qu’on admire la perfection de leurs mécanismes !

Voir un atelier mécanographique des années 1950 remis à neuf et en parfait état de fonctionnement, avec traitement de fichiers sur cartes perforées avalées à grande vitesse et à grand bruit par la tabulatrice : voilà un voyage dans le temps, que nous devons au travail de restauration mené par les anciens de Bull Belgique, qui se relaient pour en présenter la « démo » aux visiteurs stupéfaits.

Plus loin, relique exhumée du monastère de Maredsous, une grosse machine IBM accompagnée de sa véritable « base de données » biblique sur cartes perforées, imprime un listing de versets de la Genèse en hébreu.

Une bonne place est accordée aux technologies plus récentes – en fait il y a tant de micro-ordinateurs que le parti pris muséographique a consisté à en faire un mur crénelé qui entoure les dernières salles, complétant une astucieuse architecture à base de conteneurs.

Photos et videos ajoutent de la vie à ce patrimoine machinique.

 

hollerith-container
Ph : J.-J. Quisquater

Une cinquième collection est attendue, celle des anciennes machines IBM léguées par la multinationale américaine à la Maison de la Métallurgie et de l’Industrie de Liège. Elle a déjà apporté à Namur un véritable monument historique : l’une des premières machines statistiques d’Hollerith, construite pour traiter les recensements dans les années 1890, désormais classée « patrimoine exceptionnel » de la Fédération Wallonie-Bruxelles.

Inauguration doublée d’un petit colloque sur l’histoire de l’informatique en Belgique. 

Organisée par Marie d’Udekem-Gevers (informaticienne et anthropologue) sous le titre « Namur : pionnière du numérique », cette manifestation réunissait une soixantaine de personnes. Les exposés portaient sur l’histoire de l’informatique dans l’enseignement supérieur (universitaire ou non) en Belgique, montrant le caractère innovant en la matière de la capitale de la Wallonie, sur l’évolution de la programmation et sur l’informatique musicale. Ainsi que sur des sujets d’actualité, comme les smart cities (sic) dont Namur veut faire l’expérience. Les smart cities sont-elles moins bêtes que les villes d’autrefois ? Ça se discute, mais incontestablement Namur a fait preuve d’intelligence en accueillant ce nouveau musée.

Qui sait… si la France s’obstine à ne pas avoir de musée équivalent, les ordinateurs fossiles des très riches collections existant dans l’Hexagone (de Grenoble à La Villette en passant par Bordeaux, Belfort, Angers, Paris et Lillers) pourraient prendre le chemin de Namur pour être plus visibles…

 Pierre Mounier-Kuhn, CNRS & Université Paris-Sorbonne

Pour aller plus loin :

  • Numerical Artefacts Museum – Informatique Pionnière (NAM-IP)
  • Marie d’Udekem-Gevers et Jean-Marie Jacquet (dir.), Programmer : un passé pour l’avenir ?, Recueil une partie des exposés d’un colloque précédent, organisé pour les 40 ans de la Faculté d’informatique de l’Université Notre-Dame de la Paix.

Remue-méninge pour informathématicien

Un nouvel « Entretien autour de l’informatique  ». Serge Abiteboul  et Claire Mathieu interviewent Olivier Faugeras, un informaticien et mathématicien français, membre de l’Académie des sciences et de l’Académie des technologies. Olivier Faugeras est Directeur de recherche (émérite) à Inria, Sophia Antipolis. Il a apporté des contributions fondamentales à de nombreux sujets comme l’analyse d’images, la vision par ordinateur, la robotique, ou les neurosciences computationnelles et mathématiques. Ses recherches l’ont conduit aux frontières de l’informatique.

Cet article est publié en collaboration avec TheConversation.

Olivier Faugeras, © Inria
Olivier Faugeras, © Inria

B : Olivier, tes sujets de recherche ont beaucoup évolué pendant ta carrière.
OF : Oui. J’ai commencé par le traitement des images. Nous cherchions par exemple à éliminer les distortions dans des images. J’ai passé quelques années aux USA. Quand je suis rentré, j’ai démarré un groupe de recherche à l’INRIA. Nous avons travaillé sur des applications comme la vision par ordinateur. Il s’agissait, par exemple, de permettre à un robot de modéliser ce qu’il voyait pour réaliser une tâche particulière. Je suis passé ensuite tout naturellement à l’analyse des images du cerveau, ce qui m’a conduit à m’intéresser aux neurones. Aujourd’hui, je cherche à modéliser les ensembles de neurones pour contribuer à la construction de ce que j’appelle la neuroscience mathématique, un écho biologique à la physique mathématique.

cajal13B : Que sait-on dans ce domaine ?
OF : On sait finalement peu de choses. C’est tout sauf simple. Un neurone isolé, c’est déjà un monde très complexe en soi. Alors les connections d’un grand nombre de neurones… Avec les synapses et les dendrites… C’est un travail très pluridisciplinaire avec des biologistes, des chimistes, des physiciens, des informaticiens, des mathématiciens …

B : Que peut-on espérer obtenir de cette modélisation ?
OF : Bien sûr, nous espérons des avancées en « sciences fondamentales », comprendre les mécanismes de base, construire des modèles mathématiques ou informatiques du cerveau, lever le mystère de son fonctionnement. Et puis nous pouvons espérer des résultats en science clinique, par exemple, découvrir des traitements de maladies neuro-dégénératives comme Alzheimer ou Parkinson. On peut aussi imaginer de réduire la part d’expérimentation humaine de médicaments avec des simulations d’ensembles de neurones. Enfin, nous nous inspirons du fonctionnement du cerveau pour imaginer de nouvelles architectures d’ordinateurs, de nouveaux algorithmes.

B : Imaginer de nouvelles architectures d’ordinateurs, de nouveaux algorithmes ?
OF : Le cerveau n’est pas un ordinateur dans le sens d’une « machine de von Neumann », une machine purement numérique, avec d’un coté une mémoire et de l’autre un processeur. Dans le cerveau, mémoire et calcul sont mélangés ; des traitements analogiques et numériques se combinent ; c’est mystérieux mais ça fonctionne ! Peut-être moins bien qu’un ordinateur classique pour calculer ou faire des raisonnements mathématiques, mais mieux pour de nombreuses choses comme la mémoire associative par exemple, ou pour reconnaître des objets dans une image.

B : On parle beaucoup du « Human Brain Project ». Est-ce que tu pourrais nous en dire quelques mots ?
OF : C’est beaucoup d’argent : un milliard d’euros sur 10 ans, réparti entre plusieurs centaines d’équipes : donc finalement, ce n’est pas énorme rapporté au nombre de chercheurs. Henry Markram est l’homme à l’origine de ce projet, un expérimentateur de grand talent, un neuro-physiologiste qui a effectué des expériences fondamentales pour mesurer l’activité des neurones. Le but est, en dix ans, de construire un simulateur du cerveau humain. Pour y arriver, il faut mieux comprendre comment les choses se passent à plusieurs échelles de temps et d’espace et utiliser les ordinateurs les plus puissants disponibles, voire construire des ordinateurs spécialisés. Il faut aussi développer de nouveaux outils mathématiques qui font défaut.

Pour ce qui est de la modélisation de l’ensemble du cerveau de manière précise, c’est, à mon avis, hors de portée pour longtemps. On peut néanmoins arriver à modéliser de manière très détaillée le fonctionnement d’une zone du cerveau, une aire corticale par exemple, à laquelle appartiennent plusieurs millions de neurones. Pour modéliser l’audition, on peut ainsi modéliser l’aire auditive de façon très détaillée, et modéliser les aires périphériques à un niveau macroscopique, plus grossier, en s’appuyant par exemple sur les équations obtenues en prenant la limite thermodynamique c’est-à-dire en supposant que le nombre de neurones est très grand. Modéliser le tout de manière très détaillée, pas encore ; peut-être que cela sera en fait inutile.

La complexité des neurones, HBP
La complexité d’un réseau de neurones, image obtenue dans le « Humain Brain Project », Le Temps

B : Est-ce que le Humain Brain Project a déjà produit des résultats ?
OF : Le projet a un peu plus de deux ans. Pour l’instant, les gens se focalisent sur le développement de plateformes informatiques ouvertes. Certaines de ces plateformes proposent des architectures hautement parallèles, parfois neuro-inspirées. Le but est que des expérimentateurs puissent tester les modèles qu’ils proposent. D’autres visent à construire de grandes bases de données, avec des mesures diverses de neurones auxquelles les chercheurs ont accès pour comparer avec leurs modèles, entrainer ces modèles. Dans d’autres plateformes enfin, on peut piloter des robots avec des ordinateurs conçus autour d’architectures bio-inspirées. La partie du projet dans laquelle je travaille poursuit des buts moins appliqués et plus lointains, il s’agit d’un bloc scientifique intitulé « Théorie ».

B : Dans tes exposés, tu insistes sur l’importance des modèles mathématiques ?
OF : Oui. Les aspects théoriques de ces recherches sont adossés à deux piliers fondamentaux : le concept mathématique de bifurcation issu de la théorie des systèmes dynamiques et la théorie des probabilités.

Localement, un ensemble de neurones est un système dynamique qui se débrouille pour régler ses paramètres de façon à se rapprocher de ce qu’en mathématiques on appelle une bifurcation. Quand on regarde un système d’équations différentielles qui dépendent de paramètres, certains choix de valeurs des paramètres induisent un changement brutal des solutions. Proche d’une bifurcation, la réponse du système peut être plus rapide et le système plus réactif. Ça se passe comme cela dans les réseaux de neurones. Le système “s’installe” localement près d’une bifurcation et c’est cela qui lui donne sa réactivité dynamique.

L’autre pilier, ce sont les probabilités. Le cerveau est un système extrêmement «  bruité » avec de l’aléatoire partout. Il y a une sensibilité aux variations thermiques, chimiques, électriques… On pourrait croire que tout cet aléa va détériorer les informations, perturber leur transmission. Pas du tout. Le cerveau arrive à s’en sortir malgré tout. Comment ? D’au moins deux façons. D’abord avec la redondance ! Les informations sont dupliquées, des neurones voisins véhiculent souvent des informations similaires. C’est cela qui induit la robustesse. Ensuite en utilisant l’aléa pour enrichir la dynamique dont nous parlions plus haut. C’est cela qui permet de construire des « comportements » neuronaux plus sophistiqués. Et puis il y a à côté de tout cela des mécanismes très sophistiqués de décodage pour reconstruire et utiliser l’information.

B : Ça paraît très complexe le mécanisme de stockage de l’information dans la mémoire.
OF : Très. Des neurones sont connectés les uns aux autres par des synapses auxquels sont attachés des poids : ces poids définissent l’importance de chaque connexion. Localement, celle-ci évolue aléatoirement dans le temps en fonction de l’état du neurone auquel elle appartient. Localement, il n’y a pas, ou très peu, de mémoire. Mais ce qui est génial, quand on considère un ensemble de plusieurs neurones, c’est qu’il apparaît au niveau collectif des phénomènes de mémoire. C’est un peu comme dans les verres de spins en physique.

B : C’est très joli comme terme les « verres de spin » mais nous n’avons pas la moindre idée de ce que c’est.
OF : C’est un phénomène physique. Les verres de spin sont des systèmes magnétiques dans lesquels les interactions entre les atomes sont aléatoirement de signe ferro- ou anti-ferromagnétique. On les appelle verres car ils possèdent, comme les verres, beaucoup d’états métastables aux basses énergies. En première approximation, les interactions entre ces atomes les font passer aléatoirement dans deux états distincts. Les physiciens avaient eu l’intuition qu’il existait une sorte de mémoire globale des états antérieurs même s’il n’y avait pas de mémoire locale. Cela a été démontré rigoureusement, notamment par les mathématiciens Gérard Ben Arous, Alice Guionnet et Michel Talagrand. On retrouve ce curieux phénomène dans les réseaux de neurones. Ce sont les corrélations globales qui contiennent une trace de l’histoire de l’ensemble du système, donc sa mémoire, même si au niveau du neurone individuel il n’y a aucune trace. C’est une des nombreuses correspondances surprenantes que l’on peut découvrir entre la physique statistique et les systèmes neuronaux.

B : Nous sommes là dans le domaine des neurosciences, plus précisément de la « neuroscience mathématique » et de la « neuroscience computationnelle ». Tu nous expliques ?
OF : Dans les neurosciences computationnelles, on part d’un réseau de neurones, on écrit des équations, et on les « résout » avec de la simulation numérique. Pour modéliser un réseau de quelques millions de neurones, on doit modéliser l’activité de chacun des neurones au cours du temps. Il y a des millions d’équations et c’est très difficile, voire impossible, à analyser, à comprendre. Pour y arriver, il faut adopter une approche mathématique. Cela nous conduit aux neurosciences mathématiques. L’approche mathématique, en extrayant la substantifique moelle de ces gigantesques systèmes d’équations, aboutit à des modèles beaucoup plus concis qui capturent les propriétés fondamentales du système initial et permettent donc de mieux le comprendre. L’apport des mathématiques est essentiel.

B : Comment fonctionne la communauté des neurosciences computationnelles ?
OF : La communauté fonctionne bien. Les logiciels sont en général des logiciels ouverts, et l’esprit est au partage des connaissances. Tous les ans, à l’EPFL en Suisse, il y a un concours du meilleur modèle pour un neurone. On fournit des observations des neurones basées, par exemple, sur l’activité de sa membrane. On compare les logiciels pour voir lesquels s’approchent le mieux des observations. Les logiciels sont ouverts. On peut progresser en s’appuyant sur le travail des autres. La recherche scientifique avance bien ainsi. C’est, je trouve, un bel exemple à suivre de collaboration scientifique.

B : Qu’est-ce que les jeunes chercheurs dans ce domaine devraient avoir comme formation ?
OF : Il faut qu’ils aient des connaissances en neurosciences, en informatique, en mathématiques, en physique. Parmi des jeunes qui nous rejoignent, les lacunes sont parfois flagrantes. C’est parfois en informatique alors que les connaissances dans cette discipline sont indispensables. Nous avons, par exemple, à résoudre des problèmes de tri, et sans notions des bases de l’algorithmique… L’Allemagne a conçu, grâce au financement des réseaux Bernstein, des cursus adaptés recrutant des scientifiques venant d’horizons divers à l’entrée en Master et en leur donnant une formation complémentaire.

B : Tu as complètement passé sous silence certains domaines de l’informatique, comme la logique et la représentation des connaissances, qui pourtant semblent proches ?
OF : Nos connaissances en neurosciences restent modestes. Nous commençons à comprendre certains mécanismes de base comme le stockage et la transmission d’information par exemple. Pour ce qui est des mécanismes cognitifs de plus haut niveau, il faudra attendre. C’est totalement inaccessible actuellement, si ce n’est à des niveaux d’observations très grossiers qui limitent les tentatives de modélisation.

B : Tu es passionné par cette recherche. Qu’est-ce qui te passionne tant ?
OF : Ses aspects mathématiques. Développer une théorie qui capture le fonctionnement de ces ensembles de neurones. Quel défi ! C’est une étape pour comprendre un jour le raisonnement ou la conscience. C’est ça qui me fascine !

Serge Abiteboul Inria, Claire Mathieu, ENS Paris

Pour aller plus loin :

La crypto quantique débarque

La tâche est plus vieille que Le Monde : A (comme Angela) souhaite communiquer un message à B (comme Barack) tout en empêchant E (comme Edward) de l’intercepter. Nous savons faire avec des techniques sophistiquées de cryptographie comme RSA. Mais il parait que la mécanique quantique va ouvrir de nouvelles possibilités. Binaire a demandé à un ami, Alexei Grinbaum, ce qu’il en est. Serge Abiteboul, Thierry Viéville.

Cet article est publié en collaboration avec TheConversation.

Partager un secret avec une clé secrète. Le lecteur de Binaire n’aura guère de difficulté à imaginer que le message soit une suite de 0 et 1. La méthode imbattable consiste à utiliser une « clé de chiffrement jetable ». C’est une séquence de 0 et de 1, aléatoire et au moins aussi longue que le message à transmettre. Supposons qu’Angela souhaite transmettre le message « 11111 » à Barack et que la clé aléatoire, tenue secrète, soit « 10110 ». Alors Angela intervertit le premier, le troisième et le quatrième bits du message (comme l’indiquent les 1 dans la clé) et publie en clair « 01001 ». Barack, qui connaît la clé secrète, intervertit les mêmes trois bits et reconstruit le message « 11111 ». Edward n’a aucune chance de rétablir ce message en ayant accès à la seule transmission chiffrée.

Alexei Grinbaum, CEA
Alexei Grinbaum, CEA

Mais une clé qui se renouvelle sans cesse ! Un problème est que la clé est « jetable ». Si par aventure Angela l’utilisait plusieurs fois, Edward  finirait par la découvrir en faisant des analyses statistiques.

Ce que l’on aimerait, c’est un monde idéal où Angela et Barack disposeraient d’une source illimitée de clés. Imaginons qu’ils possèdent deux pièces de monnaies, A et B, qui, lorsqu’on les lance, tombent sur pile, qu’on comprendra comme « 0 », ou sur face, le « 1 », de façon aléatoire, mais, par un coup de magie, à chaque fois les deux tombent du même coté. S’ils pouvaient disposer de telles pièces, Angela et Barack pourraient jouer à pile ou face autant de fois qu’ils le souhaitent et se fabriquer sans limite des clés secrètes. Un détail : dans notre monde, à notre échelle, de telles pièces magiques n’existent pas. Alors ? Patience.

Mieux encore une clé qu’il serait inutile de voler ! Nous devons aussi garantir qu’Edward ne puisse intercepter le message en se procurant un troisième clone de la même pièce. Attaquons nous à cette dernière condition. Pour y trouver une solution, nous allons tirer profit d’une valeur que l’on ne rencontre pas souvent dans un problème de sciences : la liberté !

Supposons qu’Angela et Barack possèdent deux pièces de monnaie magiques, A1 et A2 pour la première, B1 et B2 pour le second. Pour obtenir un bit, Angela choisit librement entre A1 et A2 et lance la pièce. Barack fait de même avec B1 et B2. Ils vont recommencer autant de fois qu’ils le souhaitent. Les quatre pièces sont magiques : à chaque coup, si Angela choisit A1 et Barack B1, les deux pièces disent la même chose ; idem dans les cas (A1, B2) et (A2, B1) ; mais dans le cas (A2, B2), les pièces disent le contraire l’une de l’autre. Bref, le résultat individuel ne dépend que du choix local d’Angela ou Barack, mais la relation entre ces choix dépend de ce que font A et B conjointement.

Maintenant Angela et Barack peuvent construire une clé secrète. Pour Angela, c’est juste la séquence de bits que lui indiquent les pièces. Pour Barack, il garde le bit que lui donne sa pièce dans trois cas, et il l’intervertit dans le cas (A2,B2). Ce mécanisme garantit que le message ne sera pas intercepté par Edward. Car, même s’il est capable de cloner une pièce d’Angela, il ne connaît pas le choix de Barack. S’il lance un clone de A1 au moment où Angela choisit — toujours librement ! — de jouer A2, alors ce lancement simultané, et de A1 (cloné) et de A2 entrave le libre arbitre de Barack, puisque aucune valeur ne peut être attribuée à ses pièces (rappelons que A1=B2, mais A2≠B2, d’où la possibilité de contradiction).

Oui mais si tout cela n’existe pas ? À notre échelle, de telles pièces magiques n’existent pas. Des corrélations aussi parfaites entre elles sont en réalité inatteignables. Et puis la liberté des agents elle aussi est douteuse. Mais à l’échelle de l’infiniment petit, la cryptographie quantique pallie d’une manière spectaculaire à ces défauts.

Un exemple de dispositif qui permet d’implémenter un tel protocole de distribution quantique de clé, basé sur l’utilisation de photons transmis à travers une fibre optique. ©National Institute of Standards and Technology, via commons.wikimedia.org. Au moment où sort ce billet, un nouveau record de distance* (plus de 400km entre les points A et B) vient d’être publié.

À la place des pièces, la cryptographie quantique utilise des paires de particules quantiques  intriquées, souvent des photons. Grâce à un phénomène, l’intrication quantique, on arrive à des corrélations imparfaites, certes, mais proches de plus de 80% de celles qu’ont les pièces de monnaie dans le monde idéal. En se servant alors de la propriété de non-localité quantique, c’est-à-dire d’un lien simultané entre deux phénomènes distants, séparés dans l’espace, Angela et Barack arrivent à partager des bits avec une corrélation suffisamment forte pour que la communication reste protégée contre les intrusions. En plus, Edward ne peut s’immiscer entre Angela et Barack et intercepter leurs communications à cause d’une propriété de l’intrication quantique dont le nom fort à propos est « monogamie » : à chaque particule, pas plus d’un partenaire intriqué à la fois !

Plus de 80%, ce n’est pas idéal. Pourtant on prouve que c’est suffisant pour que les protocoles quantiques de distribution des clés secrètes puissent assurer la protection parfaite de la communication entre Angela et Barack.

Un enjeu de recherche colossal. Où en sommes-nous dans la réalisation pratique de ces procédés ? Depuis peu, la sécurité absolue qu’offre la cryptographie quantique est vraiment devenue atteignable. Nous entrons dans une ère où les expériences scientifiques, mais aussi des produits technologiques et industriels, se développent de plus en plus rapidement. L’Europe se prépare à lancer un nouveau financement gigantesque de ce secteur à la hauteur de 1 milliard d’euros. Bientôt, la cryptographie quantique prendra le relai des techniques conventionnelles de cryptage.

Alexei Grinbaum, CEA.

En savoir plus:
La mécanique des étreintes, Alexei Grinbaum, 2014.
– L’intrication quantique : https://en.wikipedia.org/wiki/Quantum_entanglement.
– Distribution quantique de clés : https://en.wikipedia.org/wiki/Quantum_key_distribution
– Le 9 novembre à 19h30, un bar des sciences sur la cryptographie quantique, http://bardessciences.net/
– Et pour les spécialistes 16-18 novembre, un colloque scientifique sur les technologiques quantiques https://iqfacolloq2016.sciencesconf.org/

(*) http://journals.aps.org/prl/abstract/10.1103/PhysRevLett.117.190501

Une nouvelle salle dédiée à l’informatique au Science Museum de Londres

logo_sciencemusem Nous sommes le  24 Octobre 2014, Sa majesté la Reine Elizabeth II envoie son 1er tweet : « It is a pleasure to open the Information Age exhibition today at the ‪@ScienceMuseum and I hope people will enjoy visiting ». Pierre est allé visiter cette galerie permanente dans le Musée de la Science de Londres et il en est ressorti tout à fait heureux. Récit. Thierry Viéville.

« C’est un plaisir d’ouvrir l’exposition sur l’ère de l’information aujourd’hui à @ScienceMuseum. J’espère que cette visite sera appréciée. » Par ces mots la Reine d’Angleterre elle même, inaugure le dernier grand musée/exposition dédié à l’informatique en date. Cette exposition permanente a pris comme thème –comme son intitulé l’indique- de se concentrer sur l’information.

On y retrace les 200 dernières années de la place de l’information dans notre société. Le parti pris est de regarder cette transformation et ces évolutions à travers 6 périodes de la transmission de l’information.

Les 6 périodes correspondent à six zones consacrées aux différentes époques et « réseaux » de communication. On y retrouve donc le Câble, le Téléphone, la Télévision (Broadcast), les Satellites (The Constellation), les réseaux cellulaires (The Cell) et le Web.

L’exposition est très « moderne » avec de très nombreux écrans interactifs ou pas, et à plusieurs endroits des montages et des objets avec lesquels on peut interagir. De même, des parcours avec des objets connectés en liens avec des applications mobiles sont disponibles. Cette dernière ayant donné lieu à un travail artistique.

Photo : P. Paradinas
information-age-1
Photo : P. Paradinas

Rompant avec l’approche muséale classique qui conduit à imposer un parcours –comme dans certains magasins d’ameublement d’origine scandinave- l’exposition se tient dans une très grande pièce rectangulaire avec un « parcours » lisible ovale autour de la pièce qui passe à travers les 6 périodes ou types de réseau. La vision et le parcours, sont complétés par un autre parcours en mezzanine qui au travers de ce chemin aérien suspendu permet de voir l’exposition sous un autre angle et/ou de découvrir d’autres objets.

information-age-2
Plan de l’exposition

Le cheminement global est historique. Pour chaque période, la technologie est présentée et explicitée. Au delà de la technique, les usages sont détaillés et illustrés. Par exemple, le sauvetage de rescapés du Titanic suite à un câble ou les numéros de téléphone du type SOS-Amitié. Plus récemment, l’impact de la téléphonie mobile (The Cell) et aussi démontré au travers d’une boutique de distribution vente et d’un centre de réparation/hacking de téléphone au Cameroun.

img_4968 img_4967
L’informatique utilisée comme moyen est aussi présente et occupe une belle place. L’informatique anglaise y trouve bien sûr une juste place, avec les premières machines issues des travaux du Bletchley Park, du National Physical Laboratory (NPL) pour les réseaux, mais aussi les projets BBC-Community ou la création de la société Advanced RISC Machine, plus connue sous le nom de ARM dont les processeurs sont au cœur de la majorité de tout les téléphones mobiles du monde.

Une belle vidéo de l’inventeur du Web Tim Berners Lee pour expliquer cette dernière période de l’exposition : The Web.

http://collectionsonline.nmsi.ac.uk/detail.php?t=objects&type=related&kv=8059486
Photo : P. Paradinas

On ne peut pas ne pas être impressionné par l’immense émetteur de la station radio de Rugby en bois.

bd-information-age-5
Apple Newton Ph : P. Paraddinas

 

Et puis, pour les nostalgiques, les amateurs du touché des choses, un grand stand au milieu de l’exposition permet d’utiliser de vieux téléphones fixes, les premiers portables (enfin transportables car de la taille d’une boite de chaussures) et un Newton-Message Pad d’Apple en état de marche.

 

D’un point de vue plus technique, l’exposition permanente « Information Age » occupe de 2.500 m². Elle contient plus de 800 objets et a été réalisée avec un budget de 15,6 M £ (plus de 17 M€). Les principaux sponsors par ordre d’importance sont la Fondation de la Loterie, British Telecom, ARM, Bloomberg Philanthropies, Google et de nombreuses autres fondations (Motorola, Qualcomm,…) ou entreprises (Accenture,..).

img_4970

Et puis, juste avant de partir une autre exposition dans le musée sur les données qui sont nos vies (« Our Lives in Data »)… avec de très nombreuses explications sur les données des différentes applications et ce que celles-ci révèlent.

 

 

Pierre Paradinas, Envoyé spécial de Binaire (Cnam)

  • Pour aller plus loin ou avant d’y aller : visitez le site web de l’expo
  • L’exposition sur les données