Intervention de Gilles Dowek

Les systèmes informatiques sont partout, pour le mieux en général. Ils permettent par exemple d'améliorer la qualité des soins médicaux, via notamment l'imagerie médicale ou la robotique chirurgicale ; ils facilitent l'accès à la connaissance, appelé à connaître une transformation radicale avec la mise en place d'e-universités. Ils ont bouleversé les modes de communications interpersonnelles. On ne peut pas, bien entendu, passer sous silence l'accroissement considérable de la productivité qu'on leur doit. C'est précisément parce que l'informatique nous apporte tous ces bénéfices que leur dysfonctionnement peut provoquer des dommages, tant matériels qu'humains, à la mesure de cette omniprésence.

On appelle domaines critiques ceux dans lesquels le dysfonctionnement d'un système informatique provoque des conséquences graves. On en compte au moins quatre : les transports, la santé, l'énergie – on a évoqué la sûreté des centrales nucléaires –, la banque et plus largement les services.

Définir les menaces pesant sur un système informatique suppose de faire la distinction traditionnelle entre sûreté et sécurité : c'est la différence entre défaillance involontaire et action malveillante. Un crash aérien, par exemple, peut être consécutif à une panne de son moteur : c'est là un problème de sûreté. Mais s'il est dû au déclenchement d'une bombe placée dans l'avion, il s'agit d'une faille de la sécurité.

Fabriquer des objets qui fonctionnent n'est certes pas un objectif propre à l'informatique. Cependant, les objets informatiques présentent la spécificité d'être les plus complexes de toute l'histoire de l'industrie humaine. Un programme compte plusieurs dizaines de millions de lignes, contre quelques dizaines de milliers dans un roman. C'est encore plus vrai s'agissant des matériels : il y a plusieurs milliards de transistors dans un processeur, contre cinq ou dix dans un poste de radio. Il est humainement impossible de construire un système aussi complexe sans se tromper. De plus, l'interconnexion des systèmes produit des bugs généralisés ou en cascade.

Étant donné le caractère faillible des êtres humains, le développement de logiciels ne peut pas être une activité exclusivement humaine. C'est la raison pour laquelle on utilise des outils informatiques pour concevoir des systèmes sans bugs. Ces outils s'appellent l'analyse statique, la vérification dans un modèle, la preuve, etc. Ils sont le fruit de recherches fondamentales en théorie de la démonstration, en théorie des langages de programmation et en combinatoire, ainsi que dans d'autres domaines à la frontière de l'informatique et des mathématiques. Ils ne sont pas plus interchangeables que ne le sont un marteau, un tournevis et une clé à molette : ils traitent des problèmes différents et doivent souvent être combinés. Ensemble, ils constituent une boite à outils qu'on appelle les méthodes formelles.

Ainsi, les algorithmes et les programmes de contrôle aérien peuvent être très complexes, mais la tâche qu'ils doivent réaliser est très simple : maintenir une distance de séparation minimale entre les avions à tout instant.

Lorsqu'on a cette spécification et ce programme, il est possible, en utilisant des outils appropriés, de démontrer, au sens mathématique du terme, que tel programme vérifie telle spécification.

La preuve de programme a été appliquée à de nombreux cas, notamment aux trains de la ligne 14 du métro parisien ou à certains compilateurs utilisés par Airbus.

En conclusion, la France fait partie des pays leaders en matière de recherche dans les méthodes formelles. Il y a, dans notre pays, un véritable potentiel de développement pour une industrie dans ce domaine.

Une manière de soutenir ce développement et d'améliorer la sûreté et la sécurité des logiciels que nous utilisons tous les jours est d'imposer, lors de la commande publique de systèmes critiques, l'utilisation de méthodes formelles, par exemple en utilisant le vocabulaire des critères communs, qui mesure la qualité d'un projet sur une échelle allant de EAL-1 à EAL-7. C'est déjà le cas, mais ce pourrait être systématique.