Seguritat de tipos

En informàtica i ,ciberseguridad, la seguritat de tipos és la mida en que un llenguage de programació disminuïx o prevé els errors de tipo . Un error de tipo és un comportament de programa erròneu o indesijable causat per una discrepància entre diferents tipos de senyes per a les constants, variables i métodos (funcions) del programa, per eixemple, tractar un sancer ( int ) com un número de punt flotant ( float ). La seguritat de tipos a voltes es considera alternativament com una propietat d'un programa d'ordenador en lloc d'una propietat del llenguage en el que està escrit eixe programa; és dir, alguns llenguages tenen funcions de seguritat de tipos que poden ser evitades per programadors que utilisen pràctiques que presenten una seguritat de tipos deficient. La definició formal de la teoria de tipos de seguritat de tipos és considerablement més sòlida de lo que entenen la majoria dels programadors.

L'eixecució de tipos pot ser estàtica, detectant possibles errors en temps de compilació, o dinàmica, associant l'informació de tipos en valors en temps d'eixecució i consultant-los segons siga necessari per a detectar errors immediats, o una combinació d'abdós.

Els comportaments classificats com a errors de tipo per un llenguage de programació donat són generalment els que resulten de realisar intents d'operacions en valors que no són del tipo de senyes apropiat. Esta classificació es basa en part en opinions; pot implicar que qualsevol operació que no done lloc a fallos del programa, falles de seguritat o unes atres falles òbvies és llegítima i no necessita ser considerada un error, o pot implicar que qualsevol incompliment de l'intenció explícita del programador (com es comunica a través d'anotacions mecanografiadas) siga errònea i no "a prova de tipos".

En el context dels sistemes de tipos estàtics (en temps de compilació), la seguritat de tipos generalment implica (entre atres coses) una garantia de que el valor final de qualsevol expressió serà un membre llegítim del tipo estàtic d'eixa expressió. El requisit precís és més sotil que açò: consulte subtipado i polimorfisme.

La seguritat de tipos està estretament relacionada en la seguritat de memòria, una restricció en la capacitat de copiar patrons de bits arbitraris d'una localisació de memòria a una atra. Per eixemple, en una implementació d'un llenguage que té un tipo $t$, de modo que alguna seqüència de bits (de la llongitut apropiada) no representa un membre llegítim de $t$, si eixe llenguage permet que les senyes es copien en una variable de tipo $t$, llavors no té seguritat de tipos perque l'operació podria assignar un valor que no siga de $t$ a eixa variable.

La majoria dels llenguages tipados estáticamente proporcionen un grau de seguritat de tipos que és estrictament més fort que la seguritat de la memòria, perque els seus sistemes de tipos imponen l'us adequat dels tipos de senyes abstractes definits pels programadors, inclús quan açò no és estrictament necessari per a la seguritat de la memòria o per a la prevenció de qualsevol tipo d'error catastròfic.

Definicions

El còdic en seguritat de tipos accedix solament a les ubicacions de memòria a les que està autorisat a accedir. (Per a esta discussió, la seguritat de tipos es referix específicament a la seguritat de tipos de memòria i no deu confondre's en la seguritat de tipos en un sentit més ampli. ) Per eixemple, el còdic de seguritat de tipos no pot llegir valors dels camps privats d'un atre objecte.

Robin Milner va proporcionar el següent eslògan per a descriure la seguritat de tipos:

Els programes ben escrits no poden "eixir mal".

La formalisació adequada d'este eslògan depén de l'estil de semàntica formal que s'utilise per a un llenguage en particular. En el context de la semàntica denotacional, seguritat de tipos significa que el valor d'una expressió que està ben tipada, digam en el tipo $t$, és un membre genuí del conjunt corresponent a $t$.

En 1994, Andrew Wright i Matthias Felleisen varen formular lo que ara és la definició estàndar i la tècnica de prova per a la seguritat de tipos en llenguages definits per la semàntica operativa . Baixe este enfocament, la seguritat de tipos està determinada per dos propietats de la semàntica del llenguage de programació:

(Tipo-) preservació o reducció de subjectes

La "bona tipificación" dels programes permaneix invariable segons les regles de transició (és dir, regles d'evaluació o regles de reducció) del llenguage.

Progrés

Un programa ben tipado mai es "atolla", lo que significa que les expressions en el programa seran evaluades a un valor, o hi ha una regla de transició per a això; en atres paraules, el programa mai entra en un estat indefinit a on no són possibles més transicions.

Estes propietats no existixen en el buit; estan vinculades a la semàntica del llenguage de programació que descriuen, i existix un gran espai de llenguages variats que poden ajustar-se a estos criteris, ya que la noció de programa "be tipado" és part de la semàntica estàtica del llenguage de programació i de la noció de "quedar-se atollat" (o "eixir mal") és una propietat de la seua semàntica dinàmica..

Vijay Saraswat proporciona la següent definició:

"Un llenguage és de tipo segur si les úniques operacions que es poden realisar en les senyes en el llenguage són les autorisades pel tipo de senyes".

Relació en atres formes de seguritat

La seguritat de tipos té com a objectiu en última instància excloure atres problemes, per eixemple: -

• Prevenció d'operacions illegals. Per eixemple, podem identificar una expressió 3 / "Hello, World" com inválida, perque les regles de l'aritmètica no especifiquen cóm dividir un número entero per una cadena de caràcters .
• Seguritat de la memòria
  • Els busques salvages poden sorgir quan una busca apunta a un objecte de tipo un tipo i es tracta com una busca que apunta a un atre tipo. Per eixemple, el tamany d'un objecte depén del tipo, per lo que si una busca s'incrementa en les credencials incorrectes, terminarà apuntant a un àrea aleatòria de la memòria.
  • Desbordament del búfer : les escritures fòra del llímit poden danyar el contingut dels objectes que ya estan presents en el heap. Açò pot ocórrer quan un objecte més gran d'un tipo es copia de manera brusca en un objecte més chicotet d'un atre tipo.
• Errors llògics originats en la semàntica de diferents tipos. Per eixemple, les polzades i els milímetros poden almagasenar-se com a número entero, pero no deuen substituir-se ni agregar-se. Un sistema de tipos pot impondre dos tipos diferents de sancers per a ells.

Vore també

• Teoria de tipos

Referències

• Pierce (2002). Types and Programming Languages, MIT Press. ISBN 978-0-262-16209-8.
• «Type Safe». Portland Pattern Repository Wiki.
• (1994).Information and Computation.115(1)

38–94.doi:10.1006/inco.1994.1093.

• ACM SIGSOFT Software Engineering Notes.7(2)

25–26.doi:10.1145/1005937.1005941.