Quels sont les avantages d'un système de types en termes de sécurité?

47

Dans JavaScript: The Good Parts de Douglas Crockford, il mentionne dans son chapitre sur l'héritage,

L’autre avantage de l’héritage classique est qu’il inclut la spécification d’un système de types. Cela libère généralement le programmeur de la nécessité d’écrire des opérations de transtypage explicites, ce qui est une très bonne chose, car lors de la transposition, les avantages en matière de sécurité d’un système de types sont perdus.

Alors tout d’abord, c’est quoi la sécurité? protection contre la corruption des données, les pirates, les dysfonctionnements du système, etc.?

Quels sont les avantages d'un système de types en termes de sécurité? Qu'est-ce qui différencie un système de types lui permettant d'offrir ces avantages en matière de sécurité?

Les erreurs ont été faites
la source
Je ne suis pas certain que les systèmes de types offrent des avantages pour les langages non compilés, mais en tant qu'utilisateur à long terme des langages compilés, je trouve que les langages compilés avec une vérification de type attentive sont efficaces pour empêcher de nombreux types de code ambigu, non défini ou incomplet passer le stade "compiler". J'imagine que vous pourriez dire que les conseils de frappe et un système Lint sont précieux pour les scripts Web (JavaScript) et, dans l'affirmative, nous en verrons assez. Dart quelqu'un? Les langages dynamiques comme Python ne semblent pas pires faute de système de type statique.
Warren P
1
Aujourd'hui, nous comprenons que la frappe doit être comportementale et non structurelle. Malheureusement, la plupart des langages de programmation modernes n'ont aucun moyen d'affirmer le comportement d'un type ( voir cette question pour une bonne lecture). Cela rend le système de types assez inutile dans la plupart des cas, en particulier parce que les erreurs de type simples que les réponses mentionnent ici peuvent être interceptées par un linter intelligent qui vérifie les problèmes courants.
Benjamin Gruenbaum
4
@BenjaminGruenbaum Ce que vous décrivez existe déjà dans des langages comme OCaml de manière statique. C'est ce qu'on appelle le typage structural, il est en fait assez ancien, le typage nominal est plus récent.
Jozefg
2
@BenjaminGruenbaum: ... Quoi !? Ce n'est évidemment pas indécidable dans les langages à typage statique, sinon écrire un compilateur pour ces langages serait impossible.
BlueRaja - Danny Pflughoeft
6
@BenjaminGruenbaum: Vos commentaires sont précieux, et ce papier est intéressant, mais cela ne corrobore pas votre affirmation selon laquelle "c'est généralement indécidable dans les langages statiques comme Java aussi", car il montre qu'il est décidable en C # et laisse ouverte la question. de savoir si c'est indécidable en Java. (Et de toute façon, IME, quand un compilateur pour un langage statiquement typé ne peut pas décider que quelque chose est bien typé, il le rejette (ou ne parvient pas à le compiler), donc l'indécidabilité est un ennui plutôt qu'un trou dans le type- sécurité.)
ruakh

Réponses:

82

Les systèmes de types préviennent les erreurs

Les systèmes de types éliminent les programmes illégaux. Considérez le code Python suivant.

 a = 'foo'
 b = True
 c = a / b

En Python, ce programme échoue. il jette une exception. Dans un langage comme Java, C #, Haskell , peu importe, ce n'est même pas un programme légal. Vous évitez entièrement ces erreurs car elles ne sont tout simplement pas possibles dans l'ensemble des programmes d'entrée.

De même, un meilleur système de types exclut plus d'erreurs. Si nous sautons aux systèmes de types super avancés, nous pouvons dire des choses comme celle-ci:

 Definition divide x (y : {x : integer | x /= 0}) = x / y

Maintenant, le système de types garantit qu’il n’ya pas d’erreur de division par 0.

Quel genre d'erreurs

Voici une brève liste de ce que les systèmes de types d'erreur peuvent éviter

  1. Erreurs hors de portée
  2. Injection SQL
  3. En généralisant 2, de nombreux problèmes de sécurité (à quoi sert la vérification des altérations dans Perl )
  4. Erreurs hors séquence (oubli d'appeler init)
  5. Forcer l'utilisation d'un sous-ensemble de valeurs (par exemple, seuls les entiers supérieurs à 0)
  6. Chatons néfastes (Oui, c'était une blague)
  7. Erreurs de perte de précision
  8. Erreurs de mémoire logicielle transactionnelle (STM) (cela nécessite de la pureté, ce qui nécessite également des types)
  9. Généraliser 8, contrôler les effets secondaires
  10. Invariants sur des structures de données (un arbre binaire est-il équilibré?)
  11. Oublier une exception ou jeter la mauvaise

Et rappelez-vous, ceci est également au moment de la compilation . Nul besoin d'écrire des tests avec une couverture de code à 100% pour simplement vérifier les erreurs de type, le compilateur le fait pour vous :)

Étude de cas: lambda calcul typé

Très bien, examinons le plus simple de tous les systèmes de types, simplement le lambda calcul .

Fondamentalement, il existe deux types,

Type = Unit | Type -> Type

Et tous les termes sont soit des variables, des lambdas ou des applications. Sur cette base, nous pouvons prouver que tout programme bien typé se termine. Il n'y a jamais une situation où le programme va rester bloqué ou en boucle pour toujours. Ce n'est pas prouvable dans le calcul lambda normal parce que, bien, ce n'est pas vrai.

Pensez-y, nous pouvons utiliser des systèmes de types pour garantir que notre programme ne fonctionne pas en boucle pour toujours, plutôt cool, non?

Détournez dans les types dynamiques

Les systèmes de types dynamiques peuvent offrir des garanties identiques aux systèmes de types statiques, mais au moment de l'exécution plutôt que lors de la compilation. En fait, puisque c'est le temps d'exécution, vous pouvez réellement offrir plus d'informations. Vous perdez cependant certaines garanties, en particulier concernant les propriétés statiques telles que la terminaison.

Ainsi, les types dynamiques n'excluent pas certains programmes, mais orientent plutôt les programmes mal formés vers des actions bien définies, telles que le lancement d'exceptions.

TLDR

En résumé, les systèmes de types excluent certains programmes. Beaucoup de programmes sont cassés d'une certaine manière, par conséquent, avec les systèmes de types, nous évitons ces programmes cassés.

Jozefg
la source
25
+1 pour la compilation, ce qui équivaut à écrire beaucoup de tests.
Dan Neely
3
@DanNeely C'est simplement pour illustrer que dans un langage dynamique, vous devez utiliser toutes les parties du code pour détecter les erreurs qu'un système de types contrôle gratuitement. Et dans un langage typé de manière dépendante, vous pouvez en réalité entièrement remplacer les tests par des types. Bien souvent, vous devez prouver des théorèmes supplémentaires de la correction
Jozefg
3
Si votre système de typage a prouvé que votre programme doit se terminer, il le fait (probablement) en prouvant qu'il calcule une fonction primitive-récursive. Ce qui est cool je suppose, mais une classe de complexité nettement moins intéressante que celle qu'une vraie machine de Turing peut résoudre. (Cela ne veut pas dire que les valeurs intermédiaires ne sont pas grandes; la fonction Ackermann est primitive-récursive…)
Donal Fellows
5
@DonalFellows La fonction Ackermann n'est pas récursive primitive, bien qu'il s'agisse d'une fonction totalement calculable.
Taymon
4
@sacundim Exactement, des langages comme agda autorisent la vérification de totalité optionnelle et, dans les rares cas où vous souhaitez une récursion arbitraire, vous pouvez poser des questions judicieusement. C'est un système assez complexe.
Jozefg
17

La réalité elle-même est dactylographiée. Vous ne pouvez pas ajouter de longueurs aux poids. Et bien que vous puissiez ajouter des pieds aux mètres (les deux sont des unités de longueur), vous devez redimensionner au moins l'une des deux. Faute de quoi, votre mission sur Mars pourrait s'écraser, littéralement.

Dans un système typé, ajouter deux longueurs exprimées dans des unités différentes aurait été une erreur ou aurait provoqué une conversion automatique.

MSalters
la source
15

Un système de types vous aide à éviter les erreurs de codage simples, ou permet plutôt au compilateur d'attraper ces erreurs pour vous.

Par exemple, en JavaScript et en Python, le problème suivant ne sera souvent détecté qu'à l'exécution - et en fonction des tests, la qualité / rareté de la condition peut en réalité être mise en production:

if (someRareCondition)
     a = 1
else
     a = {1, 2, 3}

// 10 lines below
k = a.length

Tandis qu'un langage fortement typé vous obligera à déclarer explicitement qu'il as'agit d'un tableau et ne vous laissera pas attribuer un entier. De cette façon, il n'y a aucune chance que acela ne se produise length- même dans les cas les plus rares.

Eugene
la source
5
Et un linter intelligent dans un IDE tel que WebStorm JavaScript peut dire "Référence indéfinie possible à a.length pour number a". Cela ne nous est pas donné en ayant un système de type explicite.
Benjamin Gruenbaum
4
1. Statiquement, pas très fort 2. @BenjaminGruenbaum Oui, mais cela se fait en recherchant un graphique d'affectations en arrière-plan. Imaginez-le comme un mini-interprète essayant de déterminer où vont les choses. Beaucoup plus difficile que quand les types vous le donnent gratuitement
jozefg
6
@BenjaminGruenbaum: Ne confondez pas implicite / explicite avec fort / faible. Haskell, par exemple, a un système de caractères incroyablement puissant qui fait honte à la plupart des autres langages, mais en raison de décisions de conception de langage prises, il est également capable d'inférence de type presque entièrement universelle, ce qui en fait un langage fortement implicite prenant en charge le typage explicite. (C'est ce que vous devriez utiliser, parce que l'inférence de type ne peut déduire que de ce que vous avez écrit, pas ce que vous vouliez dire!)
Phoshi
6
"Un langage fortement typé vous obligera à déclarer explicitement que a est un tableau" C'est faux. Python est fortement typé et ne nécessite pas cela. Même les langues statiquement et fortement typées ne l'exigent pas si elles supportent l'inférence de type (et la plupart des langues traditionnelles le font, du moins en partie).
Konrad Rudolph
1
@ BenjaminGruenbaum: Ah, ça va. Même dans ce cas, il y aura des cas où aucun analyseur statique JS ne peut effectuer le même type de vérification de type qu'un langage fortement typé fournirait, résolution qui, dans le cas général, nécessite de résoudre le problème d'arrêt. Haskell n'a dû prendre que peu de décisions de conception pour obtenir une inférence de type proche de 100%, et C # / Scala ne peut pas tout déduire. Bien sûr, dans ces cas, peu importe, vous pouvez simplement spécifier explicitement des types - en Javascript, cela signifie que même le meilleur analyseur statique ne peut plus vérifier votre code.
Phoshi
5

Plus tôt dans le cycle de développement logiciel vous pouvez détecter une erreur, moins il est coûteux de la réparer. Considérez une erreur qui entraîne la perte de données de votre plus gros client ou de tous vos clients. Une telle erreur pourrait être la fin de votre entreprise si elle est capturée seulement après que de vrais clients ont perdu des données! Il est clairement moins coûteux de trouver et de corriger ce bogue avant de le mettre en production.

Même pour des erreurs moins coûteuses, les testeurs sont plus actifs que les programmeurs, mais les programmeurs peuvent le trouver et le corriger. C’est moins cher s’il n’est pas vérifié dans le contrôle de source où d’autres programmeurs peuvent créer un logiciel qui en dépend. La sécurité des types empêche la compilation même de certaines classes d’erreurs, éliminant ainsi presque tout le coût potentiel de ces erreurs.

Mais ce n'est pas toute l'histoire. Comme le diront tous ceux qui programment dans un langage dynamique, il est parfois agréable de compiler votre programme afin que vous puissiez en essayer une partie sans avoir à régler tous les détails. Il y a un compromis entre sécurité et commodité. Les tests unitaires peuvent limiter le risque d'utiliser un langage dynamique, mais écrire et maintenir de bons tests unitaires a un coût qui peut être plus élevé que celui d'un langage sûr pour le type.

Si vous faites des essais, si votre code ne sera utilisé qu'une seule fois (comme un rapport ponctuel), ou si vous êtes dans une situation où vous n'auriez pas la peine d'écrire un test unitaire de toute façon, un langage dynamique est probablement parfait pour vous. Si vous avez une application volumineuse et souhaitez modifier une partie sans casser le reste, le type sécurité sauve des vies. Les types d’erreurs de type «captures de sécurité» correspondent exactement au type d’erreurs que les humains ont tendance à négliger ou à se tromper lors de la refactorisation.

GlenPeterson
la source
Cela rend le typage dynamique bref, sans mentionner ses principaux avantages (ceux mentionnés sont pratiques par relativement peu importants). Cela semble également impliquer quelque chose d'étrange à propos des tests unitaires - oui, ils sont difficiles à réaliser et ont un coût, et cela s'applique également aux langages à typage statique. Qu'est-ce que cela essaie de dire? Il omet également de mentionner les limitations (de par leur conception) des systèmes de types actuels, à la fois dans ce qu'ils peuvent exprimer et dans quelles erreurs ils peuvent intercepter.
@ MattFenwick, quels sont selon vous les principaux avantages du typage dynamique?
GlenPeterson 12/12
Les systèmes de types statiques classiques rejettent de nombreux programmes bien typés. ( Une alternative ) (BTW, mes critiques ne
4

introduction

La sécurité de type peut être obtenue avec des langages à type statique (compilé, vérification de type statique) et / ou à l'exécution (évalué, vérification de type dynamique). Selon Wikipedia, un système de type " fort" est décrit comme un système dans lequel aucune erreur de type d'exécution non vérifiée (ed Luca Cardelli) n'est possible. En d'autres termes, l'absence d'erreurs d'exécution non vérifiées est appelée sécurité ou type sécurité ... '

Sécurité - Vérification de type statique

Classiquement, la sécurité des types est synonyme de typage statique, dans des langages tels que C, C ++ et Haskell, conçus pour détecter les correspondances de types lors de leur compilation. Cela présente l'avantage d'éviter des conditions potentiellement indéfinies ou sujettes à erreur lors de l'exécution du programme. Cela peut être inestimable lorsqu'il existe un risque que les types de pointeurs soient mal adaptés, par exemple, une situation qui pourrait avoir des conséquences catastrophiques si elle n'est pas détectée. En ce sens, le typage statique est considéré comme synonyme de sécurité de la mémoire.

Le typage statique n'est pas complètement sûr mais améliore la sécurité , cependant. Même les systèmes statiques peuvent avoir des conséquences catastrophiques. De nombreux experts considèrent que le typage statique peut être utilisé pour écrire des systèmes (critiques) plus robustes et moins sujets aux erreurs.

Les langages à typage statique peuvent aider à réduire le risque de perte de données ou de précision dans le travail numérique, qui peut être dû à une mauvaise correspondance ou à une troncation des types double à float ou des types intégral et float.

L’utilisation de langages à typage statique présente un avantage en termes d’efficacité et de rapidité d’exécution. Le runtime bénéficie de l’absence de détermination des types lors de l’exécution.

Sécurité - Vérification du type d'exécution

Erlang, par exemple, est un type déclaratif, langage vérifié de type dynamique qui s'exécute sur une machine virtuelle. Le code Erlang peut être compilé octet. Erlang est considéré comme le plus important langage critique à la mission et tolérant aux pannes, et sa fiabilité est de neuf 9 (99,9999999%, soit au plus 31,5 ms par an).

Certaines langues, telles que Common Lisp, ne sont pas typées statiquement, mais des types peuvent être déclarés si nécessaire, ce qui peut contribuer à améliorer la vitesse et l'efficacité. Il convient également de noter que nombre des langages interprétés les plus largement utilisés, tels que Python, sont écrits sous la boucle d'évaluation dans des langages à typage statique tels que C ou C ++. Commom Lisp et Python sont tous deux considérés comme sûrs par la définition ci-dessus.

AsymLabs
la source
2
Je m'oppose à "fortement typé". Vous voulez dire statiquement tapé. Le type utilisé n’a quasiment aucune signification, c’est-à-dire "j’ai aimé ce type de système"
jozefg
@ jozefg Bon point. Je vais modifier le post.
AsymLabs
3
Il n'est également pas utile de dire langage interprété ... à propos d'une implémentation de langage oui, mais pas le langage lui-même. Toute langue peut être interprétée ou compilée. Et même après la modification, vous utilisez les termes frappe fort et frappe faible.
Esailija
3
@jozefg: J'ai toujours pensé que le caractère fortement typé signifiait que chaque valeur avait un type fixe (par exemple, un entier, une chaîne, etc.), alors qu'un type faiblement typé signifiait qu'une valeur pouvait être contrainte à une valeur d'un autre type, si cela était considéré comme pratique. alors. Par exemple, en Python (fortement typé), 1 + "1"lève une exception, alors qu'en PHP (faiblement typé), 1 + "1"product 2(la chaîne "1"est automatiquement convertie en entier 1).
Giorgio
1
@Giorgio avec une telle définition, par exemple, Java n'est pas fortement typé. Mais dans de nombreux cas, on le prétend. Il n'y a pas de sens à ces mots. Les définitions de type fort / faible ont une définition beaucoup plus précise, telle que jozefg: "j'aime / ne parle pas cette langue".
Esailija
1

les avantages d'un système de types en termes de sécurité sont perdus.

Alors tout d’abord, c’est quoi la sécurité? protection contre la corruption des données, les pirates, les dysfonctionnements du système, etc.?

Quels sont les avantages d'un système de types en termes de sécurité? Qu'est-ce qui différencie un système de types lui permettant d'offrir ces avantages en matière de sécurité?

J'ai l'impression que les systèmes de types ont une vue si négative. Un système de types consiste davantage à donner une garantie qu'à prouver l'absence d'absence d'erreur. Ce dernier est une conséquence du système de types. Un système de types pour un langage de programmation est un moyen de produire, au moment de la compilation, la preuve qu'un programme respecte une sorte de spécification.

Le type de spécification que l'on peut encoder en tant que type dépend de la langue, ou plus directement de la puissance du système de types de la langue.

Le type de spécification le plus fondamental est une garantie sur le comportement des fonctions en entrée / sortie et sur la validité de l'intérieur d'un corps de fonction. Considérons un en-tête de fonction

f : (Int,Int) -> String

Un bon système de types s'assurera que f n'est appliqué qu'aux objets produisant une paire de Int lors de l'évaluation et garantira que f produira toujours une chaîne.

Certaines instructions dans un langage, comme les blocs if-then, n'ont pas de comportement d'entrée / sortie; Ici, le système de types garantit la validité de chaque déclaration ou instruction du bloc; c’est-à-dire applique des opérations aux objets du type correct. Ces garanties sont composables.

En outre, cela donne une sorte de condition de sécurité de la mémoire. La citation dont vous parlez concerne le casting. Dans certains cas, la conversion est correcte, comme la conversion d’un int de 32 bits en un int de 64 bits. Cependant, généralement, cela plante le système de types.

Considérer

Foo x = new Foo(3,4,5,6);
f((Int)x,(Int)x);

À cause de la conversion, x est transformé en un Int, donc techniquement, le contrôle de type ci-dessus est vérifié; Cependant, cela va vraiment à l'encontre de l'objectif de vérification de type.

Une chose qui pourrait créer un système de types différent et meilleur est de disséminer les conversions (A) x où x avant le cas correspond au type B, sauf si B est un sous-type (ou sous-objet) de A. Les notions de théorie du sous-typage ont été utilisées en sécurité pour éliminer la possibilité d'attaques de débordement / débordement d'entier.

Sommaire

Un système de types est un moyen de prouver qu'un programme répond à une sorte de spécification. Les avantages qu'un système de types peut fournir dépendent de la force du système de types utilisé.

Jonathan Gallagher
la source
1

Un avantage qui n’a pas encore été mentionné pour un système de types réside dans le fait que de nombreux programmes sont lus plus qu’ils ne sont écrits, et dans de nombreux cas, un système de types peut permettre de spécifier un grand nombre d’informations de manière concise et facile à utiliser. digéré par quelqu'un qui lit le code. Bien que les types de paramètres ne remplacent pas les commentaires descriptifs, la plupart des gens trouveront plus rapidement ce qui suit: "int Distance;" ouDistance As Int32que lire "La distance doit être un nombre entier +/- 2147483647"; Des fractions de passage peuvent donner des résultats incohérents. "En outre, les types de paramètres peuvent aider à réduire l'écart entre ce qu'une implémentation particulière d'une API fait par rapport à ce que les appelants sont autorisés à utiliser. Par exemple, si une implémentation Javascript particulière d'une API utilise ses paramètres d'une manière qui forcerait toutes les chaînes à la forme numérique, il peut être difficile de savoir si les appelants sont autorisés à compter sur un tel comportement, ou si d' autres implémentations du dysfonctionnement pourrait API si les chaînes données. avoir une méthode dont le paramètre est spécifié comme DoubleWould indiquer clairement que toutes les valeurs de chaîne doivent être forcées par l'appelant avant d'être transmises; disposer d'une méthode avec une surcharge qui accepte Doubleet une autre qui accepteString serait un peu plus clair que les appelants détenteurs de chaînes seraient autorisés à les transmettre en tant que tels.

supercat
la source
0

Alors tout d’abord, c’est quoi la sécurité? Protection contre la corruption des données, les pirates, les dysfonctionnements du système, etc.?

Toutes les autres réponses et plus. En général, "sécurité du type" signifie simplement qu'aucun des programmes compilés avec succès par un compilateur ne contient d'erreur de type.

Maintenant, quelle est une erreur de type? En principe, vous pouvez spécifier toute propriété indésirable en tant qu'erreur de type, et certains systèmes de types seront en mesure de garantir de manière statique qu'aucun programme ne présente une telle erreur.

Par "propriété" ci-dessus, j'entends un type de proposition logique qui s'applique à votre programme, par exemple, "tous les index sont compris dans les limites d'un tableau". Parmi les autres types de propriétés, on peut citer "tous les pointeurs différés sont valables", "ce programme n'effectue aucune E / S" ou "ce programme n'effectue des E / S que sur / dev / null", etc. La propriété peut être spécifiée et le type vérifié de cette manière, en fonction de l’expression de votre système de typage.

Les systèmes de types dépendants font partie des systèmes de types les plus généraux, grâce auxquels vous pouvez appliquer à peu près n'importe quelle propriété de votre choix. Ce n'est pas forcément facile à faire, car les propriétés sophistiquées sont sujettes à l' incomplétude de la part de Gödel .

naasking
la source