Seguretat de tipus

En informàtica, la seguretat de tipus i la solidesa de tipus són el grau en què un llenguatge de programació desincentiva o evita els errors de tipus. La seguretat de tipus de vegades es considera alternativament una propietat de les eines d'un llenguatge informàtic; és a dir, algunes eines són segures pel que fa al tipus i el seu ús no donarà lloc a errors de tipus, mentre que altres eines del mateix llenguatge poden no ser segures pel que fa al tipus i un programa que les utilitza pot trobar errors de tipus. Els comportaments classificats com a errors de tipus per un llenguatge de programació determinat solen ser els que resulten dels intents de realitzar operacions sobre valors que no són del tipus de dades adequat, per exemple, afegir una cadena a un enter quan no hi ha cap definició de com gestionar aquest cas. Aquesta classificació es basa en part en l'opinió.

L'aplicació de tipus pot ser estàtica, detectant possibles errors en temps de compilació, o dinàmica, associant informació de tipus amb valors en temps d'execució i consultant-los segons calgui per detectar errors imminents, o una combinació d'ambdues opcions.^[1] L'aplicació de tipus dinàmica sovint permet executar programes que no serien vàlids amb l'aplicació estàtica.

En el context dels sistemes de tipus estàtics (en temps de compilació), la seguretat de tipus normalment implica (entre altres coses) una garantia que el valor final de qualsevol expressió serà un membre legítim del tipus estàtic d'aquesta expressió. El requisit precís és més subtil que això; vegeu, per exemple, subtipificació i polimorfisme per a complicacions.

Intuïtivament, la solidesa del tipus es captura amb l'afirmació concisa de Robin Milner que

Els programes ben tipificats no poden "sortir malament".

En altres paraules, si un sistema de tipus és correcte, les expressions acceptades per aquest sistema de tipus han d'avaluar-se com a valor del tipus adequat (en lloc de produir un valor d'un altre tipus no relacionat o fallar amb un error de tipus). Vijay Saraswat proporciona la següent definició relacionada:

Un llenguatge és segur pel que fa al tipus si les úniques operacions que es poden realitzar sobre les dades del llenguatge són les que permet el tipus de les dades.^[2]

Tanmateix, el que significa precisament que un programa estigui "ben tipificat" o que "es faci malament" són les propietats de la seva semàntica estàtica i dinàmica, que són específiques de cada llenguatge de programació. En conseqüència, una definició formal i precisa de la solidesa de tipus depèn de l'estil de semàntica formal utilitzada per especificar un llenguatge. El 1994, Andrew Wright i Matthias Felleisen van formular el que s'ha convertit en la definició estàndard i la tècnica de prova per a la seguretat de tipus en llenguatges definits per semàntica operativa,^[3] que és la més propera a la noció de seguretat de tipus tal com l'entenen la majoria dels programadors. Segons aquest enfocament, la semàntica d'un llenguatge ha de tenir les dues propietats següents per ser considerada sòlida de tipus:

Progrés

Un programa ben tipificat mai es "encalla": cada expressió o bé ja és un valor o bé es pot reduir a un valor d'alguna manera ben definida. En altres paraules, el programa mai entra en un estat indefinit on no siguin possibles més transicions.

Preservació (o reducció de subjectes)

Després de cada pas d'avaluació, el tipus de cada expressió roman igual (és a dir, es conserva el seu tipus).

També s'han publicat diversos altres tractaments formals de la solidesa dels tipus en termes de semàntica denotacional i semàntica operacional estructural.^[4]

Aïlladament, la solidesa del tipus és una propietat relativament feble, ja que essencialment només afirma que les regles d'un sistema de tipus són internament consistents i no es poden subvertir. Tanmateix, a la pràctica, els llenguatges de programació estan dissenyats de manera que una bona tipificació també implica altres propietats més fortes, algunes de les quals inclouen:

• Prevenció d'operacions il·legals. Per exemple, un sistema de tipus pot rebutjar l'expressió 3 / "Hello, World" com a invàlida, perquè l'operador de divisió no està definit per a un divisor de cadena.
• Seguretat de la memòria
  • Els sistemes de tipus poden evitar que els punters salvatges que d'altra manera podrien sorgir d'un punter a un tipus d'objecte siguin tractats com a punter a un altre tipus.
  • Els sistemes de tipus més sofisticats, com ara els que admeten tipus dependents, poden detectar i rebutjar accessos fora de límit, evitant possibles desbordaments de memòria intermèdia.^[5]
• Errors lògics originats en la semàntica de diferents tipus. Per exemple, les polzades i els mil·límetres es poden emmagatzemar com a nombres enters, però no s'han de substituir ni sumar. Un sistema de tipus pot imposar dos tipus diferents d'enters per a ells.

La seguretat de tipus sol ser un requisit per a qualsevol llenguatge de joguina (és a dir, llenguatge esotèric) proposat en la investigació acadèmica de llenguatges de programació. Molts llenguatges, en canvi, són massa grans per a proves de seguretat de tipus generades per humans, ja que sovint requereixen la comprovació de milers de casos. No obstant això, s'ha demostrat que alguns llenguatges com ara Standard ML, que té una semàntica rigorosament definida, compleixen una definició de seguretat de tipus. Es creu que alguns altres llenguatges com ara Haskell compleixen alguna definició de seguretat de tipus, sempre que no s'utilitzin certes característiques "d'escapada" (per exemple, Haskell's , utilitzat per "escapar" de l'entorn restringit habitual en què és possible l'E/S, eludeix el sistema de tipus i, per tant, es pot utilitzar per trencar la seguretat de tipus.^[6]) El joc de paraules de tipus és un altre exemple d'aquesta característica "d'escapada". Independentment de les propietats de la definició del llenguatge, es poden produir certs errors en temps d'execució a causa d'errors en la implementació o en biblioteques enllaçades escrites en altres llenguatges; aquests errors podrien fer que un tipus d'implementació determinat no fos segur en determinades circumstàncies. Una versió anterior de la màquina virtual Java de Sun era vulnerable a aquest tipus de problema.^[7]

Els llenguatges de programació sovint es classifiquen col·loquialment com a fortament tipats o feblement tipats (també amb tipatge lliure) per referir-se a certs aspectes de la seguretat de tipus. El 1974, Liskov i Zilles van definir un llenguatge fortament tipat com aquell en què "sempre que un objecte es passa d'una funció que fa la crida a una funció que fa la crida, el seu tipus ha de ser compatible amb el tipus declarat a la funció que fa la crida".^[8] El 1977, Jackson va escriure: "En un llenguatge fortament tipat, cada àrea de dades tindrà un tipus diferent i cada procés indicarà els seus requisits de comunicació en termes d'aquests tipus".^[9] En canvi, un llenguatge feblement tipat pot produir resultats imprevisibles o pot realitzar una conversió de tipus implícita.^[10]

La seguretat de tipus està estretament relacionada amb la seguretat de memòria. Per exemple, en una implementació d'un llenguatge que té algun tipus ${\displaystyle t}$ que permet alguns patrons de bits però no d'altres, un error de memòria de punter penjant permet escriure un patró de bits que no representa un membre legítim de ${\displaystyle t}$ en una variable morta de tipus ${\displaystyle t}$, causant un error de tipus quan es llegeix la variable. Per contra, si el llenguatge és segur per a la memòria, no pot permetre que un enter arbitrari s'utilitzi com a punter, per tant, hi ha d'haver un punter o tipus de referència separat.

Com a condició mínima, un llenguatge de tipus segur no ha de permetre punters penjants entre assignacions de diferents tipus. Però la majoria de llenguatges imposen l'ús correcte dels tipus de dades abstractes definits pels programadors, fins i tot quan això no és estrictament necessari per a la seguretat de la memòria o per a la prevenció de qualsevol tipus d'error catastròfic. A les assignacions se'ls assigna un tipus que descriu el seu contingut, i aquest tipus es fixa durant la durada de l'assignació. Això permet que l'anàlisi d'àlies basada en tipus infereixi que les assignacions de diferents tipus són diferents.

La majoria de llenguatges de tipus segurs utilitzen la recollida de brossa. Pierce diu que "és extremadament difícil aconseguir la seguretat de tipus en presència d'una operació de desassignació explícita", a causa del problema del punter penjant.^[11] Tanmateix, Rust generalment es considera segur de tipus i utilitza un verificador de préstecs per aconseguir la seguretat de memòria, en lloc de la recollida de brossa.

En els llenguatges orientats a objectes, la seguretat de tipus sol ser intrínseca al fet que hi hagi un sistema de tipus. Això s'expressa en termes de definicions de classe.

Una classe defineix essencialment l'estructura dels objectes derivats d'ella i una API com un contracte per gestionar aquests objectes. Cada vegada que es crea un objecte nou, complirà amb aquest contracte.

Cada funció que intercanvia objectes derivats d'una classe específica, o que implementa una interfície específica, s'adherirà a aquest contracte: per tant, en aquesta funció, les operacions permeses sobre aquest objecte només seran les definides pels mètodes de la classe que l'objecte implementa. Això garantirà que es preservi la integritat de l'objecte.

Les excepcions a això són els llenguatges orientats a objectes que permeten la modificació dinàmica de l'estructura de l'objecte o l'ús de la reflexió per modificar el contingut d'un objecte per superar les restriccions imposades per les definicions dels mètodes de la classe.