Sommaire-
Garanties de sûreté : le minimum exigible
Dans le numéro de décembre 2011 des Communications of the ACM [1] Xavier Leroy introduit un article de Jean Yang et Chris Hawblitzel, Safe to the Last Instruction : Automated Verification of a Type-Safe Operating System [2].
Ce texte bref donne à Xavier Leroy l'occasion de formuler avec concision les qualités qu'en 2011 on devrait être en droit d'attendre d'un environnement de développement de logiciels afin d'assurer aux programmes y-écrits robustesse, sûreté de fonctionnement et sécurité des usages. Atteindre la qualité souhaitée demande que soit vérifiée la sûreté du typage et de la mémoire, c'est-à-dire que soient appliqués strictement un petit nombre de principes fondamentaux : une chaîne de caractères n'est pas un pointeur sur une fonction ; l'accès à un tableau n'est possible qu'entre les bornes de ses index ; une zone de mémoire dé-allouée n'est plus accessible ; on ne peut pas fabriquer un pointeur (ou toute autre référence) à partir d'un entier ; etc. Ces principes de bon sens sont violés avec allégresse par des langages comme C et C++, dont les adeptes considèrent même que l'art de pratiquer ces violations prouve leur compétence. À l'inverse, Java, OCaml, Scheme ou Ada, langages plus modernes, garantissent le respect de ces principes.
La mise en œuvre de ces principes repose sur la combinaison d'un contrôle de type statique (à la compilation) et dynamique (par exemple, vérification des bornes de tableau à l'exécution), et d'une gestion automatique de la mémoire.
Au cours de la dernière décennie, nous dit Xavier Leroy, ces méthodes pour garantir la sûreté du logiciel ont fait des progrès considérables, sous l'impulsion notamment des communautés Java et .NET, qui les ont mises en œuvre jusque dans leurs machines virtuelles, ce qui prouve que la sûreté peut être garantie y compris dans les couches basses du système d'exploitation. Dans le même ordre d'idées, des chercheurs ont créé un Typed Assembly Language (TAL), ce qui délivre les compilateurs de la charge de la preuve et permet la sûreté des logiciels écrits en plusieurs langages (polyglottes ?).
Le système d'exploitation sûr décrit par Yang et Hawblitzel, Verve, représente une avancée significative sur ce chemin vers la sûreté, obtenue grâce à TAL. Cependant, il reste des parties du système d'exploitation dont la preuve de sûreté de la mémoire est plus difficile à obtenir : c'est le cas notamment... de la gestion de la mémoire (allocation, glaneur de cellules), ainsi que de la commutation de contexte et du traitement des interruptions, dont la sûreté doit être prouvée « à la main ».
Vers de meilleures architectures du matériel et du logiciel
Ce n'est pas d'hier que les défauts et les lacunes des langages de programmation, des systèmes d'exploitation et des architectures matérielles (ISA : Instruction Set Architecture) les plus répandus ont été relevés. Dès le tournant des années 1970, date de leur apparition, des solutions alternatives existaient.
Les auteurs de Multics (1964), Fernando Corbató en tête, avaient déjà compris que la notion de fichier était une aporie conceptuelle, source de difficultés inextricables, et qu'il était incomparablement plus efficace et élégant d'avoir un concept unique de mémoire, dont certains segments pourraient se voir dotés de l'attribut de persistance. L'électronique de l'époque ne permettait pas de produire à des coûts raisonnables des ordinateurs capables de supporter un système aussi puissant, et nous avons hérité de Unix, système pour lequel tout est fichier.
À l'époque où Dennis Ritchie et Ken Thompson ont conçu le langage C (1972), un « assembleur portable » dérivé de l'assembleur du PDP, il était sans doute un véhicule commode pour l'écriture de pilotes de périphériques, de commutateurs de tâches et d'allocateurs de mémoire, mais sûrement pas pour les innombrables logiciels d'application qui sont grâce à lui truffés de vulnérabilités de type débordement de tampon, et encore moins comme langage d'apprentissage initial pour des armées d'étudiants qui croiront toute leur vie que le fin du fin de l'art de la programmation consiste à bricoler astucieusement des entiers pour en faire des pointeurs de fonction, et à ne pas trop se mélanger les pinceaux dans les malloc et les struct. Il existait déjà (ou peu après) des langages de programmation qui offraient de bien meilleures possibilités d'abstraction et de rigueur. Quant aux qualités d'expressivité et d'intelligibilité, dont C est totalement dépourvu, il n'était pas difficile de faire mieux. L'hégémonie de C a procédé de sa disponibilité à peu près gratuite et générale, elle a plongé l'art de la programmation dans l'obscurantisme et le bricolage.
La déplorable architecture x86, que nous devons encore supporter, naquit en 1978 : à cette époque plusieurs projets d'architectures RISC (Reduced instruction set computing, par opposition à CISC, Complex instruction set computing, comme x86) étaient déjà assez avancés, notamment l'IBM 801/ROMP, qui sortit de fonderie en 1981, bientôt suivi par les processeurs MIPS (1985), PA-RISC (HP, 1986), SPARC (Sun, 1987), Alpha (DEC, 1992). Ces processeurs RISC se révélèrent d'emblée considérablement plus rapides et plus efficaces que leurs rivaux CISC, et de surcroît plus simples à concevoir et à fabriquer. Ce sont les gros volumes de production (et de profit) du PC, avec leur corollaire en parc de logiciels disponibles, qui assurèrent la suprématie totale de l'architecture x86 et d'Intel, son concepteur. En fait, hommage du vice à la vertu, tous les processeurs modernes comportent un cœur RISC entouré de circuits qui procurent un décor différent, x86 par exemple, mais au prix de performances moindres (un processeur x86 à 3 GHz comporte un cœur RISC à 10 GHz [3]), sans parler de la consommation électrique et de la dissipation thermique, qui sont les principaux obstacles que les ingénieurs hardware doivent affronter aujourd'hui.
Les technologies en vigueur atteignent leurs limites, cependant que la puissance des processeurs actuels autorise des traitements d'une complexité hors d'atteinte il y a quelques années. En effet, avoir un système d'exploitation qui exhibe des abstractions simples impose d'enfouir sa complexité intrinsèque dans le système afin que l'utilisateur ne la voie pas, et il en va de même pour les langages de programmation. La voie semble enfin ouverte pour des systèmes plus sûrs et plus intelligibles : pour les langages, depuis Java la cause est entendue (sauf dans les IUT français, récemment convertis à C++, sans doute pour freiner la formation d'informaticiens, dont nous serions trop bien pourvus) ; pour les systèmes Verve et seL4 montrent sans doute la voie ; quant aux processeurs, le salut viendra peut-être de l'architecture ARM.
[1] Communications of the Association for Computing Machinery, vol. 54, n° 12, p. 122.
[2] Communications of the Association for Computing Machinery, vol. 54, n° 12, pp. 123-131.
[3] François Anceau, communication personnelle.