sécurité de type

Intuitivement, la validité typographique est résumée par la formule concise de Robin Milner :

Les programmes bien typés ne peuvent pas « mal tourner ».

Autrement dit, si un système de types est correct , les expressions acceptées par ce système doivent s'évaluer à une valeur du type approprié (plutôt que de produire une valeur d'un autre type ou de provoquer une erreur de type). Vijay Saraswat propose la définition suivante :

Un langage est sûr en termes de types si les seules opérations qui peuvent être effectuées sur les données du langage sont celles autorisées par le type des données.

Cependant, la signification précise des termes « bien typé » et « erroné » pour un programme dépend des propriétés de sa sémantique statique et dynamique , spécifiques à chaque langage de programmation. Par conséquent, une définition formelle et précise de la validité des types dépend du style de sémantique formelle utilisé pour spécifier un langage. En 1994, Andrew Wright et Matthias Felleisen ont formulé ce qui est devenu la définition et la technique de preuve standard pour la sûreté des types dans les langages définis par sémantique opérationnelle , qui correspond le mieux à la notion de sûreté des types telle que la plupart des programmeurs la comprennent. Selon cette approche, la sémantique d'un langage doit posséder les deux propriétés suivantes pour être considérée comme valide :

Progrès

Un programme bien typé ne se bloque jamais : toute expression est soit déjà une valeur , soit peut être réduite à une valeur selon une méthode bien définie. Autrement dit, le programme n’atteint jamais un état indéfini où aucune transition supplémentaire n’est possible.

Préservation (ou réduction du sujet )

Après chaque étape d'évaluation, le type de chaque expression reste le même (c'est-à-dire que son type est préservé ).

Un certain nombre d'autres traitements formels de la validité des types ont également été publiés en termes de sémantique dénotationnelle et de sémantique opérationnelle structurelle .

Prise isolément, la validité des types est une propriété relativement faible, puisqu'elle stipule essentiellement que les règles d'un système de types sont cohérentes et ne peuvent être contournées. Cependant, en pratique, les langages de programmation sont conçus de sorte qu'un bon typage implique également d'autres propriétés plus fortes, dont voici quelques exemples :

• Prévention des opérations illégales. Par exemple, un système de types peut rejeter l'expression 3 / "Hello, World"comme invalide, car l' opérateur de division n'est pas défini pour un diviseur de chaîne .
• Sécurité de la mémoire
  • Les systèmes de typage peuvent empêcher les pointeurs non standard qui pourraient autrement apparaître lorsqu'un pointeur vers un type d'objet est traité comme un pointeur vers un autre type.
  • Les systèmes de types plus sophistiqués, tels que ceux prenant en charge les types dépendants , peuvent détecter et rejeter les accès hors limites, empêchant ainsi les débordements de tampon potentiels .
• Les erreurs logiques proviennent de la sémantique des différents types. Par exemple, les pouces et les millimètres peuvent tous deux être stockés comme des entiers, mais ne doivent pas être intervertis ni additionnés. Un système de types peut imposer deux types entiers différents pour ces unités.

La sûreté de type est généralement une exigence pour tout langage jouet (c.-à-d. un langage ésotérique ) proposé dans la recherche académique sur les langages de programmation. Cependant, de nombreux langages sont trop volumineux pour que des preuves de sûreté de type générées manuellement soient possibles, car elles nécessitent souvent la vérification de milliers de cas. Néanmoins, certains langages, comme Standard ML , dont la sémantique est rigoureusement définie, ont été prouvés conformes à une définition de la sûreté de type. D'autres langages, comme Haskell, sont considérés comme conformes à une certaine définition de la sûreté de type, à condition que certaines fonctionnalités d'« échappement » ne soient pas utilisées (par exemple, ` unsafePerformIO` de Haskell , utilisé pour « échapper » à l'environnement restreint habituel dans lequel les entrées/sorties (E/S) sont possibles, contourne le système de types et peut donc être utilisé pour compromettre la sûreté de type. ). Le « type punning » est un autre exemple de telle fonctionnalité d'« échappement ». Indépendamment des propriétés de la définition du langage, certaines erreurs peuvent survenir à l'exécution en raison de bogues dans l'implémentation ou dans les bibliothèques liées écrites dans d'autres langages ; de telles erreurs pourraient rendre un type d'implémentation donné non sûr dans certaines circonstances. Une version antérieure de la machine virtuelle Java de Sun était vulnérable à ce type de problème.

Les langages de programmation sont souvent classés, de manière informelle, en langages fortement typés ou faiblement typés (ou à typage lâche) en fonction de certains aspects de la sécurité des types. En 1974, Liskov et Zilles ont défini un langage fortement typé comme un langage dans lequel « lorsqu'un objet est passé d'une fonction appelante à une fonction appelée, son type doit être compatible avec le type déclaré dans la fonction appelée » . En 1977, Jackson écrivait : « Dans un langage fortement typé, chaque zone de données possède un type distinct et chaque processus exprime ses exigences de communication en fonction de ces types » . À l'inverse, un langage faiblement typé peut produire des résultats imprévisibles ou effectuer des conversions de type implicites

La sécurité des types est étroitement liée à la sécurité de la mémoire . Par exemple, dans une implémentation d'un langage qui possède certains types

Par définition, un langage à typage statique ne doit pas autoriser les pointeurs non initialisés entre des allocations de types différents. Cependant, la plupart des langages imposent l'utilisation correcte des types de données abstraits définis par les programmeurs, même lorsque cela n'est pas strictement nécessaire pour la sécurité de la mémoire ou la prévention de toute défaillance critique. Chaque allocation se voit attribuer un type décrivant son contenu, et ce type reste fixe pendant toute la durée de l'allocation. Cela permet à l'analyse d'alias basée sur les types de déduire que les allocations de types différents sont distinctes.

La plupart des langages à typage statique utilisent le ramasse-miettes . Pierce affirme qu'« il est extrêmement difficile d'assurer la sécurité des types en présence d'une opération de désallocation explicite », en raison du problème des pointeurs non initialisés. Cependant, Rust est généralement considéré comme sûr au niveau des types et utilise un vérificateur d'emprunt pour garantir la sécurité de la mémoire, au lieu du ramasse-miettes.

Dans les langages orientés objet, la sécurité des types est généralement intrinsèque à la présence d'un système de types . Ceci s'exprime par des définitions de classes.

Une classe définit essentiellement la structure des objets qui en héritent, et une API sert de contrat pour la manipulation de ces objets. Chaque nouvel objet créé devra respecter ce contrat.

Chaque fonction qui échange des objets dérivés d'une classe spécifique ou implémentant une interface spécifique respectera ce contrat : par conséquent, dans cette fonction, les opérations autorisées sur cet objet seront uniquement celles définies par les méthodes de la classe que l'objet implémente. Ceci garantira la préservation de l'intégrité de l'objet.

Font exception à cette règle les langages orientés objet qui permettent la modification dynamique de la structure de l'objet, ou l'utilisation de la réflexion pour modifier le contenu d'un objet afin de surmonter les contraintes imposées par les définitions des méthodes de classe.