C'est déjà assez grave de perdre une heure de travail lorsque votre ordinateur tombe en panne, mais dans des environnements comme les soins de santé et l'aviation, les problèmes logiciels peuvent avoir des conséquences bien plus graves. Dans un cas notoire, un bogue informatique a causé des surdoses mortelles à des patients atteints de cancer à partir d'un appareil de radiothérapie ; dans les titres plus récents, un logiciel défectueux a été blâmé pour les accidents d'avion en Éthiopie et en Indonésie.

Aujourd'hui chercheurs au Stevens Institute of Technology, en collaboration avec l'Université de Yale, développent des outils qui pourraient rendre les accidents informatiques catastrophiques beaucoup moins probables. Dirigé par Eric Koskinen, professeur assistant d'informatique à Stevens, le travail vise non seulement à s'assurer que les programmes fonctionnent correctement dans des situations spécifiques, mais utilise également des algorithmes pour déterminer si c'est logiquement possible, en quelque circonstance que ce soit, pour que le logiciel produise des résultats indésirables.

"Ce que nous visons, c'est une garantie à 100 % que vous ne rencontrerez jamais de bogue, " a déclaré Koskinen.

L'équipe de Koskinen, soutenu par plus de 2,5 millions de dollars du Bureau de la recherche navale, modélise les différences entre deux versions d'un programme. C'est utile parce que les programmeurs travaillent souvent en s'appuyant sur des logiciels existants, plutôt que d'écrire du code à partir de zéro, et des bugs peuvent être introduits d'une version à l'autre. Cette approche est particulièrement précieuse pour les militaires, étant donné que les agences de défense achètent fréquemment des logiciels à des entrepreneurs privés, puis apportez des modifications en interne avant de les déployer dans des situations critiques.

"Ils ont besoin d'un moyen de confirmer qu'ils ont correctement apporté les modifications en interne, et n'ont pas introduit de nouveaux problèmes, " a déclaré Koskinen.

Pour prouver mathématiquement qu'un programme informatique ne peut jamais avoir de bogue, quelles que soient les circonstances, prévu ou insoupçonné, L'équipe de Koskinen utilise une stratégie appelée logique temporelle. Plutôt que de scruter des lignes de code individuelles pour rechercher des différences syntaxiques, l'équipe, dont le professeur adjoint Jun Xu, un expert en analyse binaire chez Stevens, examine le comportement d'un programme au fil du temps. L'idée est de prouver que quelle que soit la durée d'exécution du programme, il n'y a aucun moyen logique pour qu'il renvoie jamais un résultat indésirable.

Modéliser la structure et le comportement d'un programme, plutôt que de se pencher sur des lignes de code individuelles, est important car exactement les mêmes lignes de code peuvent avoir des effets différents dans différents contextes, tout comme des lignes de code qui semblent très différentes peuvent accomplir la même chose. C'est comme étudier un document juridique, Koskinen explique :changer un seul mot peut sembler trivial, mais peut changer tout le sens du document. La logique temporelle permet de modéliser le potentiel d'un programme, obtenir des informations puissantes sur les capacités réelles du programme.

L'approche de l'équipe permet également d'éliminer les bogues dans les logiciels commerciaux standard pour lesquels le code source n'est pas disponible. Sans le code source, l'équipe doit comparer les programmes informatiques en utilisant la version binaire du code source. "Il est difficile de voir si la vulnérabilité a vraiment été éliminée si vous ne pouvez pas voir le code source, " a-t-il dit. " Les techniques que nous construisons feront cela :si vous avez une version du logiciel en laquelle vous avez confiance, nos techniques seront en mesure de vous aider à repérer les changements (vulnérabilités dans les mises à jour logicielles ou malwares insérés dans les programmes exécutables) et à décider s'il faut faire confiance à la nouvelle version."

L'équipe de Koskinen développe également une boîte à outils que d'autres chercheurs et membres du public pourront utiliser pour tester des logiciels - et ils étendent leur approche pour travailler avec des programmes plus importants et des problèmes plus complexes. "Ce sont de gros problèmes qui affligent les systèmes informatiques modernes, " a déclaré Koskinen. " Ces problèmes ne feront que s'aggraver, dans des domaines comme la santé, aviation, véhicules autonomes, et bien d'autres encore, il est donc essentiel que nous développions des techniques pratiques pour rendre les systèmes contrôlés par ordinateur sans bogues et sûrs à utiliser. »