Les informaticiens peuvent prouver qu'il n'y a pas d'erreurs dans le programme avec la même certitude que les mathématiciens peuvent prouver les théorèmes. Ces avancées sont utilisées pour renforcer la sécurité dans divers domaines, des drones à Internet.



Au printemps 2015, une équipe de hackers a tenté de s'introduire dans un hélicoptère militaire sans pilote appelé Little Bird ("Bird"). L'hélicoptère, similaire à la version habitée de l'avion préféré des forces spéciales américaines, était situé à Boeing en Arizona. Les hackers avaient une longueur d'avance: au début de leur travail, ils avaient accès à l'un des sous-systèmes de l'ordinateur de contrôle. Ils ne pouvaient que pirater l'ordinateur de bord principal et prendre le contrôle de l'UAV.

Au tout début du projet, l'équipe de hackers de la Red Team pouvait casser un système d'hélicoptère presque aussi facilement que le WiFi de votre domicile. Au cours des mois suivants, les ingénieurs de la DARPA ont mis en place un nouveau mécanisme de sécurité, un système logiciel non soumis à une expropriation forcée. Les paramètres clés du système Little Bird ne peuvent pas être déchiffrés à l'aide des technologies existantes, et son code peut être considéré comme une preuve mathématique. Et bien que l’équipe ait eu six semaines d’accès à l’UAV et que l’accès au système informatique ait dépassé les capacités d’accès d’une véritable équipe de hackers, elle n’a pas réussi à casser la défense de l’oiseau.

«Ils ne pouvaient pas casser ou perturber l'opération», explique Kathleen Fisher, professeur d'informatique à l'Université Tufts et chef de projet pour les systèmes cyber-militaires à haute assurance (HACMS). "En conséquence, les représentants de la DARPA se sont levés et ont dit, oh mon Dieu, vous pouvez réellement utiliser cette technologie dans des systèmes importants."

La technologie opposée aux pirates est un style de programmation appelé confirmation formelle . Contrairement au code ordinaire écrit de manière informelle et généralement évalué uniquement par ses performances, le logiciel officiellement vérifié ressemble à une preuve mathématique: chaque déclaration découle logiquement de la précédente. L'ensemble du programme peut être vérifié avec la même certitude qu'un théorème mathématique.

«Vous écrivez une formule mathématique qui décrit le comportement d'un programme et utilisez un outil de validation de principe qui teste la validité de cette déclaration», explique Brian Parno , chercheur en recherche formelle et sécurité chez Microsoft Research.

Le désir de créer des programmes officiellement confirmés a existé presque aussi longtemps que le domaine de l'informatique lui-même. Et pendant très longtemps, cela est resté impossible, mais les réalisations des dix dernières années dans le domaine des «méthodes formelles» ont rapproché cette approche de la pratique conventionnelle. Aujourd'hui, la confirmation formelle du logiciel est à l'étude dans des groupes universitaires financés, dans des projets militaires américains et dans des sociétés technologiques telles que Microsoft et Amazon.

L'intérêt grandit avec une augmentation du nombre de tâches vitales en ligne. Lorsque les ordinateurs existaient isolément dans les maisons et les bureaux, les erreurs de programmation n'étaient qu'une nuisance. Désormais, ils ouvrent des failles de sécurité sur les machines du réseau, permettant à toute personne avertie de pénétrer dans les systèmes informatiques.

«Au 20e siècle, lorsqu'un programme avait une erreur, c'était grave, il pouvait tomber, eh bien, Dieu la bénisse», a déclaré Andrew Appel , professeur d'informatique à l'Université de Princeton et chef de file en validation de programme. Mais au 21e siècle, une erreur peut ouvrir un moyen pour les pirates de prendre le contrôle du programme et de voler vos données. D'une erreur tolérable, c'est devenu une vulnérabilité qui est bien pire », dit-il.


Kathleen Fisher

Rêves de programmes parfaits

1973 . , , , . , « 2:30 , ». 1976 « », ( , ), .

Mais l'informatique n'a pas suivi cette idée, principalement parce que pendant de nombreuses années, il a semblé impossible, voire impossible, de déterminer la fonction d'un programme en utilisant les règles de la logique formelle.

Une définition formelle est un moyen de déterminer ce qu'un programme fait spécifiquement. La confirmation formelle est un moyen de prouver sans aucun doute que le code du programme correspond parfaitement à cette définition. Imaginez que vous écrivez un programme pour un robot motorisé vous emmenant dans une épicerie. Au niveau des opérations, vous déterminez les mouvements que le robot doit atteindre pour atteindre l'objectif - il peut tourner, ralentir ou accélérer, s'allumer ou s'éteindre au début et à la fin du chemin. Votre programme se composera de ces opérations de base, organisées dans le bon ordre afin qu'à la fin vous arriviez au magasin, et non à l'aéroport.

La manière traditionnelle de tester la santé d'un programme consiste à tester. Les programmeurs donnent au programme beaucoup de données d'entrée (tests unitaires) pour s'assurer qu'il se comporte comme il se doit. Si votre programme définit un algorithme pour le mouvement d'un robot, vous pouvez tester ses déplacements entre de nombreux points différents. Ces tests garantissent le bon fonctionnement des programmes dans la plupart des cas, ce qui est suffisant pour la plupart des applications. Mais les tests unitaires ne garantissent pas que le logiciel fonctionnera toujours correctement - vous ne pouvez pas comparer le programme avec toutes les données d'entrée possibles. Même si l'algorithme fonctionne pour toutes les destinations, il est toujours possible qu'il se comporte différemment dans des conditions rares - ou, comme on dit, dans des «conditions aux limites» - et ouvre une faille de sécurité. Dans les programmes réels, ces erreurs peuvent être simples, par exemple, des dépassements de tampon,dans lequel le programme copie un peu plus de données que nécessaire et écrase une partie de la mémoire de l'ordinateur. Cette erreur apparemment inoffensive est difficile à éliminer, et elle fournit un trou pour une attaque de pirate - une charnière de porte faible qui ouvre la voie au château.

«Un trou quelque part dans le logiciel, et c'est une vulnérabilité. Il est très difficile de vérifier tous les chemins pour toutes les entrées possibles », explique Parno.

Ces spécifications sont plus compliquées qu'un voyage au magasin. Les programmeurs, par exemple, peuvent avoir besoin d'un programme notarié et apposant la date de réception des documents dans l'ordre où ils ont été reçus. Dans ce cas, la spécification doit indiquer que le compteur augmente toujours et que le programme ne doit jamais permettre à la clé utilisée de signer de fuir.

En langage humain, c'est facile à décrire. Transformer une spécification en un langage formel qu'un ordinateur comprend est beaucoup plus difficile - ce qui explique le principal problème de l'écriture de programmes.

«Construire une spécification formelle compréhensible pour un ordinateur est par essence difficile», explique Parno. "Il est facile au niveau supérieur de dire" ne laissez pas le mot de passe couler ", mais vous devez réfléchir à la façon de transformer cela en une définition mathématique."

Un autre exemple est un programme qui trie une liste de nombres. Un programmeur qui essaie de formaliser une spécification pour elle peut trouver ceci:

Pour chaque élément j de la liste, assurez-vous que j ≤ j + 1

Mais même dans cette spécification formelle - pour vous assurer que chaque élément de la liste est inférieur ou égal au suivant - il y a une erreur. Le programmeur suppose que la sortie contiendra l'entrée modifiée. Si la liste est [7, 3, 5], il s'attend à ce que le programme renvoie [3, 5, 7]. Mais la sortie du programme [1, 2] satisfera aux spécifications - car «c'est aussi une liste triée, mais pas la liste que vous attendiez probablement», explique Parno.

En d'autres termes, il est difficile de transformer l'idée de ce qu'un programme devrait faire en une spécification formelle qui exclut toute interprétation incorrecte de ce que vous voulez du programme. Et l'exemple donné décrit le programme de tri le plus simple. Imaginez maintenant une description de quelque chose de beaucoup plus abstrait, comme la protection par mot de passe. «Qu'est-ce que cela signifie mathématiquement? Pour une telle définition, il peut être nécessaire d'écrire une description mathématique de ce que signifie «garder un secret», ou ce que cela signifie pour que l'algorithme de chiffrement soit sûr », explique Parno. «Nous avons examiné tous ces problèmes et avancé dans leur étude, mais ils peuvent être extrêmement difficiles à mettre en œuvre.»

Sécurité des blocs

En fait, il est nécessaire d'écrire à la fois les spécifications et les commentaires supplémentaires nécessaires pour que le logiciel puisse tirer des conclusions sur le code. Un programme, y compris sa confirmation officielle, peut représenter cinq fois la taille d'un programme régulier rédigé dans le même but.

Ce fardeau peut être allégé un peu avec des outils appropriés - des langages de programmation et des programmes auxiliaires qui aident les programmeurs à créer des programmes pare-balles. Mais dans les années 1970, ils n'existaient pas. «De nombreux aspects de la science et de la technologie n'ont pas connu une croissance suffisante à ce moment-là, alors dans les années 1980, de nombreux domaines de l'informatique s'étaient désintéressés de cela», explique Appel, chercheur principal chez DeepSpec, un groupe de systèmes informatiques officiellement validé.

Malgré l'amélioration des outils, un autre obstacle est apparu dans la confirmation des programmes: il n'y avait aucune certitude que cela était nécessaire. Bien que les amateurs de la méthode aient déclaré que de petites erreurs peuvent entraîner de gros problèmes, les autres ont attiré l'attention sur le fait que les programmes informatiques fonctionnent plutôt bien. Parfois, ils se bloquent, oui - mais perdre un peu de données non enregistrées, ou parfois redémarrer le système semble être un petit prix à payer pour ne pas avoir à traduire minutieusement chaque élément du programme dans le langage de la logique formelle. Au fil du temps, même ceux qui étaient à l'origine de la confirmation du programme ont commencé à douter de ses avantages. Dans les années 1990, même Hoar a reconnu que les spécifications pouvaient être une solution longue à un problème inexistant. En 1995, il a écrit:

( ) , … , , .

Puis est venu Internet, qui a fait la même chose pour les erreurs dans le code que les voyages en avion pour les infections: lorsque tous les ordinateurs sont connectés les uns aux autres, des erreurs inconfortables mais tolérantes peuvent entraîner des problèmes de sécurité croissants.

"Nous n'avons pas bien compris", explique Appel. "Il existe des programmes ouverts à tous les pirates Internet, et s'il y a une erreur dans un tel programme, cela peut devenir une vulnérabilité."

Au moment où les chercheurs ont commencé à comprendre la gravité des menaces à la sécurité posées par Internet, la confirmation du programme était sur le point de revenir. Pour commencer, les chercheurs ont fait des progrès dans les parties fondamentales des méthodes formelles. Il s'agit d'une amélioration des programmes auxiliaires tels que Coq et Isabelle; développement de systèmes logiques ( théorie des types dépendants) fournir une plateforme de développement qui aide les ordinateurs à évaluer le code; La «sémantique opérationnelle» est un langage qui a les bons mots pour exprimer ce qui est requis du programme.

«En commençant par la spécification en langage humain, vous avez rencontré des ambiguïtés», explique Janette Wing , vice-présidente de Microsoft Research. - Toute langue naturelle contient des ambiguïtés. Dans la spécification formelle, vous écrivez une description exacte basée sur les mathématiques pour expliquer ce que vous attendez du programme. »


Janette Wing de Microsoft Research

De plus, les chercheurs en méthodes formelles ont redéfini leurs objectifs. Dans les années 1970 et 1980, ils voulaient créer des systèmes informatiques entièrement testés, des circuits électroniques aux programmes. Aujourd'hui, la plupart des chercheurs travaillent sur des parties de systèmes petites, mais les plus critiques ou vulnérables - par exemple, les systèmes d'exploitation ou les protocoles cryptographiques.

«Nous ne disons pas que nous prouverons que l'ensemble du système est 100% correct, jusque dans les circuits électroniques», explique Wing. - De telles déclarations sont ridicules. Nous sommes précis dans ce que nous pouvons ou ne pouvons pas faire. »

Le projet HACMS montre comment vous pouvez obtenir de grandes garanties de sécurité en décrivant une petite partie d'un système informatique. Le premier objectif du projet était de créer un quadricoptère incassable pour le divertissement. Le logiciel fourni avec le quadric était monolithique - c'est-à-dire qu'en accédant à une partie de celui-ci, le pirate avait accès à toutes les autres. Depuis deux ans, l'équipe HACMS divise le code de l'ordinateur de contrôle en plusieurs parties.

L'équipe a réécrit l'architecture logicielle en utilisant ce que Fisher appelle des «blocs de construction de haute confiance» - des outils qui permettent à un programmeur de prouver la pureté du code. L'un d'eux apporte la preuve que, ayant accédé à l'une des unités, il n'est pas possible d'élever les privilèges pour atteindre les autres.

Plus tard, les programmeurs ont installé un tel logiciel sur le «Bird». Lors du test avec l'équipe rouge, elle a eu accès à l'une des parties du système qui contrôlait une partie de l'hélicoptère, par exemple, la caméra - mais pas les fonctions principales. L'échec des pirates était mathématiquement garanti. «Ils ont prouvé de manière vérifiable par machine que les pirates ne pourront pas aller au-delà de la partition système, ce n'est donc pas surprenant», explique Fisher. "Ceci est cohérent avec le théorème, mais il est toujours utile de vérifier."

Au cours de l'année qui a suivi l'audit, la DARPA a appliqué les outils et technologies du projet à d'autres domaines de la technologie militaire, par exemple les satellites et les camions automatiques. De nouvelles initiatives coïncident avec la façon dont la confirmation officielle s'est répandue au cours des dix dernières années: chaque projet réussi encourage le suivant. «Les excuses concernant la complexité de ce principe ne fonctionnent plus», explique Fisher.

Vérifiez internet

La sécurité et la fiabilité sont deux des principaux objectifs qui inspirent les méthodes formelles. Chaque jour, le besoin d'améliorations devient de plus en plus évident. En 2014, une petite erreur logicielle, qu'une description formelle aurait détectée, a ouvert la voie à une erreur Heartbleed qui menaçait de casser Internet. Un an plus tard, quelques pirates «légaux» ont confirmé les pires craintes concernant les voitures connectées à Internet, obtenant le contrôle à distance de la Jeep Cherokee .

Avec des taux plus élevés, les chercheurs en méthodes formelles se sont fixés des objectifs de plus en plus ambitieux. L'équipe DeepSpec, dirigée par Appel (travaillant également sur HACMS), essaie de construire un système aussi complexe et entièrement testé qu'un serveur Web. En cas de succès, le projet, qui a reçu une subvention de la State Science Foundation de 10 millions de dollars, réunira de nombreux petits projets réussis de la dernière décennie. Les chercheurs ont créé plusieurs composants sécurisés éprouvés comme le noyau du système d'exploitation. «Ce qui n'a pas été fait jusqu'à présent, c'est l'intégration de ces composants dans des interfaces spécifiques aux spécifications», explique Appel.

Chez Microsoft Research, les programmeurs ont deux projets ambitieux. Le premier, Everest, vise à créer une version validée de HTTPS, un protocole de sécurisation des navigateurs Web que Wing appelle le «talon d'Achille d'Internet».

La seconde est la création de spécifications confirmées pour les systèmes cyber-physiques complexes, tels que les drones. Le projet rencontre des difficultés importantes. Alors que les programmes conventionnels fonctionnent avec des étapes distinctes et non ambiguës, les programmes de contrôle des drones utilisent l'apprentissage automatique pour prendre des décisions probabilistes basées sur un flux continu de données environnementales. Il est loin d'être évident de savoir comment des décisions logiques peuvent être prises avec un tel degré d'inexactitude ou décrites comme une spécification formelle. Mais ce n'est qu'au cours des dix dernières années que les méthodes formelles ont avancé assez loin et Wing, qui gère le projet, pense avec optimisme que les chercheurs seront en mesure de résoudre tous ces problèmes.