Intervention de Dominique Bolignano

Je vais vous parler de l'état actuel de l'utilisation des méthodes formelles dans l'industrie et du potentiel de celles-ci.

Pour ce faire, je répartirai les trois catégories de méthodes formelles dont a parlé Gilles Dowek en deux groupes.

Celles du premier groupe – analyse statique et vérification dans un modèle – sont les plus simples d'utilisation. Elles permettent de répondre à des questions précises, mais plus limitées, et d'éviter certains types d'erreurs informatiques ou sur certaines catégories de logiciels. Gérard Berry a donné plusieurs exemples de leur application dans les transports, notamment dans l'aéronautique. Ce sont, de loin, les plus utilisées dans l'industrie.

Une dizaine de sociétés – françaises ou contrôlées par de grands groupes français – commercialisent ces technologies. Malgré un grand potentiel de croissance, ces sociétés restent de taille modeste – entre 10 et 200 personnes. Elles n'en ont pas moins une grande importance pour la sûreté et la sécurité numériques.

Le deuxième groupe de méthodes formelles concerne la preuve de programme : il faut l'appliquer là où les techniques du premier groupe ne réussissent pas, car elle est beaucoup plus coûteuse et demande plus de temps. En revanche, son domaine d'application est beaucoup plus vaste. Elle couvre à peu près tous les secteurs qu'on a cités et permet de répondre à un nombre de questions beaucoup plus important.

Il en est ainsi pour la téléphonie mobile. La plupart des informations importantes, autant pour les entreprises que pour les particuliers, passent par les téléphones, et celles qui n'y passent pas sont accessibles à distance grâce à eux. C'est donc un point de vulnérabilité très important.

Actuellement, à chaque nouvelle version, quelques semaines suffisent pour que les téléphones de dernière génération – comme ceux d'Apple ou d'Android – soient crackés, c'est-à-dire attaqués et cassés dans leur sécurité. Les pirates ou les attaquants exploitent des vulnérabilités, qui sont des erreurs logicielles. Ce sont les bogues – ou bugs dont parlait Gérard Berry. Les bogues en matière de sûreté ont moins de répercussions, mais en matière de sécurité, quelques-uns suffisent pour mener une attaque de grande envergure. Voilà pourquoi on essaie de s'approcher le plus possible du « zéro faute ».

Ces erreurs sont exploitées pour des besoins relativement modestes, mais elles pourraient l'être pour lancer des attaques beaucoup plus graves. Cela nous renvoie aux propos qu'a tenus ce matin le représentant du ministère de la défense.

Je citerai deux exemples liés à la téléphonie mobile.

Le premier concerne les entreprises. La plupart des cadres utilisent leur téléphone à des fins aussi bien professionnelles que personnelles : ils consultent des mails et peuvent charger des applications à la fiabilité douteuse. Or les erreurs logicielles peuvent être utilisées pour corrompre et faire du cyberespionnage à relativement grande échelle, ce qui peut avoir des répercussions dramatiques sur l'entreprise.

Ces erreurs pourraient être évitées par une bonne application des méthodes formelles, en particulier de la preuve de programme. Certes, cela coûte cher et est difficile à faire, mais c'est faisable.

Deuxième axe : le paiement par téléphone. S'il y a eu beaucoup d'avancées grâce à la carte à puce, le téléphone reste un élément vulnérable dans la mesure où l'on a remplacé des terminaux de paiement relativement sécurisés par des objets qui le sont beaucoup moins.

Quant à la banque à domicile, qui n'est pas considérée comme un moyen de paiement mais permet de faire des virements, elle est encore plus vulnérable.

Il ne s'agit pas d'appliquer ces techniques sur tout le logiciel. En effet, les téléphones peuvent comporter jusqu'à plusieurs dizaines de millions de lignes de codes. Les architectures modernes permettent de se focaliser sur une « base de confiance », qui ne fait que quelques dizaines de milliers de lignes de codes : en s'attaquant à celles-ci, on peut vraiment s'approcher du « zéro défaut » s'agissant des parties critiques et éviter ces erreurs.

On a dit ce matin que cette problématique connaissait une croissance exponentielle. Je le confirme : nous n'en sommes qu'au début.

L'utilisation des méthodes formelles reste très modeste, essentiellement pour des problèmes liés à leur mise en oeuvre et au manque de disponibilité d'experts dans ces domaines. Cela étant, la nouvelle société que j'ai créée a pour objet de les appliquer à grande échelle : des raisons objectives m'amènent à penser que c'est possible.

Nous nous trouvons aujourd'hui dans une situation très proche de celle d'il y a trente ans, au moment de la conception en 3D. Des sociétés comme Dassault Systèmes, qui est devenu le numéro un mondial dans son domaine, ont transformé la manière dont le développement était fait. Aujourd'hui, l'enjeu est encore plus grand, car le potentiel est probablement beaucoup plus important.

Pour terminer, je rejoindrai Gilles Dowek en disant que c'est le moment de se lancer. Je le montre moi-même en investissant beaucoup. Les pouvoirs publics pourraient de leur côté favoriser l'utilisation de ces méthodes formelles, afin d'enclencher un cercle vertueux.