Les dysfonctionnements informatiques font régulièrement la une des journaux, que ce soit des attaques malveillantes ou des erreurs de conception et de programmation (les célèbres bugs). Par exemple, au printemps dernier, des rançongiciels[i] ont paralysé des hôpitaux en France et en Irlande, ainsi que l’oléoduc Colonial qui alimente en essence la côte Est des États-Unis. Une cyber-attaque sur une station de traitement des eaux en Floride a permis au pirate d’augmenter dangereusement la quantité d’hydroxyde de sodium (NDLR : soude caustique) dans l’eau. Une porte dérobée a été découverte dans le logiciel SolarWinds Orion de surveillance de réseaux informatiques, permettant à la grande puissance qui a introduit cette porte de collecter beaucoup d’informations confidentielles dans les agences gouvernementales et les grandes entreprises utilisant ce logiciel. Et cetera.

Comment expliquer cette fragilité de l’informatique ? C’est le revers de son extraordinaire flexibilité, celle-là même qui l’a fait sortir des centres de calcul, envahir notre quotidien, et gérer nos infrastructures économiques et sociales. La facilité avec laquelle on écrit et modifie le logiciel débouche sur des systèmes informatiques excessivement complexes, que plus personne ne maîtrise dans leur intégralité, et riches en failles de sécurité. La rigueur avec laquelle le matériel exécute le logiciel, sans jamais dévier de ce qui est écrit, sans s’user avec le temps, a pour effet pervers qu’une faille de sécurité est facilement reproductible et exploitable à distance sur des millions d’ordinateurs, de téléphones, ou d’objets connectés à Internet. Par exemple, en 2016, l’opérateur français OVH a subi une dévastatrice attaque par déni de service provenant de centaine de milliers de caméras de sécurité, toutes piratées à distance non pour recueillir leurs images mais seulement pour leur faire amplifier l’attaque.

Comment faire face à cette vulnérabilité des systèmes informatiques ? Revenir à un monde moins informatisé, moins connecté, moins centralisé, semble peu probable. En revanche, beaucoup de progrès restent à faire pour améliorer les logiciels, en éradiquer les bugs, et les rendre résistants aux attaques. Les traits du logiciel – flexibilité, rigueur, reproductibilité – dont les attaques tirent parti sont aussi un puissant moyen de contrer ces attaques ! L’objet des sciences du logiciel est précisément de concevoir et d’étudier les principes, les approches et les outils nécessaires à la construction de logiciels fiables et sécurisés.

Dans le cadre de la chaire Sciences du logiciel, j’explore des approches scientifiquement rigoureuses et fondées sur les mathématiques et la logique. Une fois donnée une sémantique formelle aux langages de programmation utilisés, tout programme est aussi une définition mathématique : on peut raisonner sur le comportement du programme en démontrant des théorèmes sur cette définition ou en calculant certaines de ses propriétés ; on peut aussi synthétiser un programme « correct par construction » à partir des propriétés qu’il doit vérifier.

Voilà qui peut surprendre tant ces approches, connues sous le nom de « méthodes formelles », diffèrent des méthodes expérimentales utilisées par tous : on écrit d’abord le programme puis on le teste longuement pour le valider. Bien qu’efficace pour assurer le bon fonctionnement du logiciel non critique en conditions normales, le test devient très coûteux aux plus hauts niveaux d’exigence de qualité et se révèle peu efficace pour détecter les failles de sécurité, tant les attaquants savent sortir des conditions dans lesquelles le logiciel a été testé.

Les méthodes formelles souffrent moins de ces limitations et dessinent un chemin vers le logiciel zéro défaut. Cependant, elles sont longtemps restées à l’état de curiosités académiques, tant les objets mathématiques correspondant à un programme réaliste sont énormes et difficiles à manier. Il a fallu développer des outils de vérification formelle qui automatisent une grande partie des raisonnements pour permettre les premières utilisations systématiques de méthodes formelles pour des logiciels critiques, dans le ferroviaire, l’avionique, et le nucléaire. Citons comme exemples de telles utilisations le pilotage automatique de la ligne 14 du métro parisien, les commandes électroniques de vol des avions Airbus A380 et A350, et les fonctions cryptographiques au cœur de la sécurité du navigateur Web Firefox. Ma principale contribution à cet effort est d’étendre la vérification formelle du logiciel critique lui-même aux outils informatiques (compilateurs, générateurs de code, analyseurs statiques) qui participent à sa production et sa vérification.

L’émergence des outils de vérification formelle est un des résultats majeurs de la science informatique des vingt dernières années. Cependant, beaucoup reste à faire pour étendre et faciliter l’utilisation de ces méthodes formelles. Il faut mieux prendre en compte les nouveaux impératifs de sécurité, notamment le respect de la vie privée ; les attaques comme Spectre, qui exploitent les fuites d’information provenant des processeurs multicœurs modernes ; les algorithmes distribués comme dans les applications Web et les blockchains[ii]; et les réseaux de neurones et autres systèmes pour l’intelligence artificielle qui ne sont plus complètement écrits, mais en grande partie appris à partir d’exemples. Beaucoup de travaux de recherche en perspective, mais toujours l’espoir, grâce à la rigueur des mathématiques et à la puissance des outils informatiques, de maîtriser entièrement le logiciel dans toute sa complexité.

Pr Xavier Leroy
Chaire Sciences du logiciel

 

[i]  Technique d’attaque courante de la cybercriminalité, le rançongiciel ou ransomware consiste en l’envoi à la victime d’un logiciel malveillant qui chiffre l’ensemble de ses données et lui demande une rançon en échange du mot de passe de déchiffrement (source : Agence nationale de la sécurité des systèmes d’information – ANSSI).

[ii] Mode de stockage et de transmission de données sous forme de blocs liés les uns aux autres et protégés contre toute modification.