Tipo de seguridad - Type safety

Sistemas de tipos
Conceptos generales
Categorías mayores
Categorías menores

En informática , la seguridad de los tipos es la medida en que un lenguaje de programación desalienta o evita los errores de tipos . Un error de tipo es un comportamiento de programa erróneo causado por una discrepancia entre diferentes tipos de datos para las constantes, variables y métodos (funciones) del programa, por ejemplo, tratar un entero ( int ) como un número de punto flotante ( float ) Se necesita un mejor ejemplo . La seguridad de tipos a veces se considera alternativamente como una propiedad de un programa de computadora en lugar del lenguaje en el que está escrito ese programa; es decir, algunos lenguajes tienen funciones de seguridad de tipos que los programadores pueden eludir que utilizan otras funciones de seguridad de tipos en el mismo idioma. La definición formal de la teoría de tipos de seguridad de tipos es considerablemente más sólida de lo que entienden la mayoría de los programadores.

La imposición de tipos puede ser estática, detectando posibles errores en tiempo de compilación , o dinámica, asociando información de tipos con valores en tiempo de ejecución y consultándolos según sea necesario para detectar errores inminentes, o una combinación de ambos. La aplicación de tipo dinámico esencialmente permite que se ejecute un programa no válido.

Los comportamientos clasificados como errores de tipo por un lenguaje de programación dado son generalmente los que resultan de los intentos de realizar operaciones en valores que no son del tipo de datos apropiado . Esta clasificación se basa en parte en opiniones.

En el contexto de los sistemas de tipos estáticos (en tiempo de compilación), la seguridad de tipos generalmente implica (entre otras cosas) una garantía de que el valor final de cualquier expresión será un miembro legítimo del tipo estático de esa expresión. El requisito preciso es más sutil que esto; consulte, por ejemplo, Subtipado y polimorfismo (informática) para conocer las complicaciones.

La seguridad de tipos está estrechamente relacionada con la seguridad de la memoria , una restricción en la capacidad de copiar patrones de bits arbitrarios de una ubicación de memoria a otra. Por ejemplo, en una implementación de un lenguaje que tiene algún tipo , tal que alguna secuencia de bits (de la longitud apropiada) no representa un miembro legítimo de , si ese lenguaje permite que los datos se copien en una variable de tipo , entonces no es seguro para los tipos porque una operación de este tipo podría asignar un valor sin valor a esa variable. Por el contrario, si el lenguaje no es seguro para los tipos hasta el punto de permitir que se utilice un entero arbitrario como puntero , entonces no es seguro para la memoria.

La mayoría de los lenguajes tipados estáticamente proporcionan un grado de seguridad de tipos que es estrictamente más fuerte que la seguridad de la memoria, porque sus sistemas de tipos imponen el uso adecuado de los tipos de datos abstractos definidos por los programadores, incluso cuando esto no es estrictamente necesario para la seguridad de la memoria o para la prevención de ningún tipo. de falla catastrófica.

Definiciones

El código de tipo seguro accede solo a las ubicaciones de memoria a las que está autorizado a acceder. (Para esta discusión, la seguridad de tipos se refiere específicamente a la seguridad de tipos de memoria y no debe confundirse con la seguridad de tipos en un aspecto más amplio). Por ejemplo, el código de seguridad de tipos no puede leer valores de los campos privados de otro objeto.

Robin Milner proporcionó el siguiente eslogan para describir la seguridad de tipos:

Los programas bien escritos no pueden "salir mal".

La formalización adecuada de este lema depende del estilo de semántica formal que se utilice para un idioma en particular. En el contexto de la semántica denotacional , seguridad de tipos significa que el valor de una expresión que está bien tipada, digamos con el tipo τ, es un miembro genuino del conjunto correspondiente a τ.

En 1994, Andrew Wright y Matthias Felleisen formularon lo que ahora es la definición estándar y la técnica de prueba para la seguridad de tipos en lenguajes definidos por la semántica operativa . Bajo este enfoque, la seguridad de tipos está determinada por dos propiedades de la semántica del lenguaje de programación:

(Tipo-) preservación o reducción de sujetos
La "buena tipificación" ("tipificabilidad") de los programas permanece invariable bajo las reglas de transición (es decir, reglas de evaluación o reglas de reducción) del lenguaje.
Progreso
Un programa bien escrito (que se puede escribir) nunca se "atasca", lo que significa que las expresiones del programa se evaluarán a un valor o hay una regla de transición para ello; en otras palabras, el programa nunca entra en un estado indefinido en el que no son posibles más transiciones.

Estas propiedades no existen en el vacío; están vinculados a la semántica del lenguaje de programación que describen, y existe un gran espacio de lenguajes variados que pueden ajustarse a estos criterios, ya que la noción de programa "bien tipado" es parte de la semántica estática del lenguaje de programación y la noción de "quedarse atascado" (o "salir mal") es una propiedad de su semántica dinámica .

Vijay Saraswat proporciona la siguiente definición:

"Un idioma es de tipo seguro si las únicas operaciones que se pueden realizar con los datos en el idioma son las sancionadas por el tipo de datos".

Relación con otras formas de seguridad

La seguridad de tipo tiene como objetivo en última instancia excluir otros problemas, por ejemplo: -

  • Prevención de operaciones ilegales. Por ejemplo, podemos identificar una expresión 3 / "Hello, World"como inválida, porque las reglas de la aritmética no especifican cómo dividir un número entero por una cadena .
  • Seguridad de la memoria
    • Los punteros salvajes pueden surgir cuando un puntero a un objeto de tipo se trata como un puntero a otro tipo. Por ejemplo, el tamaño de un objeto depende del tipo, por lo que si un puntero se incrementa con las credenciales incorrectas, terminará apuntando a un área aleatoria de la memoria.
    • Desbordamiento del búfer : las escrituras fuera del límite pueden dañar el contenido de los objetos que ya están presentes en el montón. Esto puede ocurrir cuando un objeto más grande de un tipo se copia toscamente en un objeto más pequeño de otro tipo.
  • Errores lógicos originados en la semántica de diferentes tipos. Por ejemplo, las pulgadas y los milímetros pueden almacenarse como números enteros, pero no deben sustituirse ni sumarse. Un sistema de tipos puede imponer dos tipos diferentes de enteros para ellos.

Idiomas de tipo seguro y de tipo inseguro

La seguridad de tipos suele ser un requisito para cualquier lenguaje de juguete propuesto en la investigación de lenguajes de programación académicos. Muchos lenguajes, por otro lado, son demasiado grandes para las pruebas de seguridad de tipo generado por humanos, ya que a menudo requieren la verificación de miles de casos. Sin embargo, se ha demostrado que algunos lenguajes como Standard ML , que ha definido rigurosamente la semántica, cumplen una definición de seguridad de tipos. Algunos otros lenguajes como Haskell se cree que para cumplir con alguna definición de seguridad de tipos, siempre cierta "escapar" no se utilizan características (por ejemplo de Haskell unsafePerformIO , usado para "escape" del entorno restringido usual en la que / O es posible I, elude el sistema de tipos y, por lo tanto, se puede utilizar para romper la seguridad de tipos). El juego de palabras con tipos es otro ejemplo de esta característica de "escape". Independientemente de las propiedades de la definición del lenguaje, pueden ocurrir ciertos errores en tiempo de ejecución debido a errores en la implementación, o en bibliotecas vinculadas escritas en otros lenguajes; tales errores podrían hacer que un tipo de implementación dado sea inseguro en determinadas circunstancias. Una de las primeras versiones de la máquina virtual Java de Sun era vulnerable a este tipo de problema.

Escritura fuerte y débil

Artículo principal: mecanografía fuerte y débil

Los lenguajes de programación a menudo se clasifican coloquialmente como fuertemente tipados o débilmente tipados (también escritos libremente) para referirse a ciertos aspectos de la seguridad de tipos. En 1974, Liskov y Zilles definieron un lenguaje fuertemente tipado como aquel en el que "siempre que un objeto se pasa de una función que llama a una función llamada, su tipo debe ser compatible con el tipo declarado en la función llamada". En 1977, Jackson escribió: "En un lenguaje fuertemente tipado, cada área de datos tendrá un tipo distinto y cada proceso establecerá sus requisitos de comunicación en términos de estos tipos". Por el contrario, un lenguaje de tipo débil puede producir resultados impredecibles o puede realizar una conversión de tipo implícita.

Seguridad de tipos en lenguajes orientados a objetos

En los lenguajes orientados a objetos, la seguridad de los tipos suele ser intrínseca al hecho de que existe un sistema de tipos . Esto se expresa en términos de definiciones de clases.

Una clase esencialmente define la estructura de los objetos derivados de ella y una API como un contrato para manejar estos objetos. Cada vez que se crea un nuevo objeto, cumplirá con ese contrato.

Cada función que intercambia objetos derivados de una clase específica, o que implementa una interfaz específica , se adherirá a ese contrato: por lo tanto, en esa función, las operaciones permitidas en ese objeto serán solo aquellas definidas por los métodos de la clase que el objeto implementa. Esto garantizará que se conservará la integridad del objeto.

Las excepciones a esto son los lenguajes orientados a objetos que permiten la modificación dinámica de la estructura del objeto, o el uso de la reflexión para modificar el contenido de un objeto para superar las restricciones impuestas por las definiciones de métodos de clase.

Escriba problemas de seguridad en idiomas específicos

Ada

Ada fue diseñado para ser adecuado para sistemas integrados , controladores de dispositivos y otras formas de programación del sistema , pero también para fomentar la programación con seguridad de tipos. Para resolver estos objetivos en conflicto, Ada limita la inseguridad de tipos a un cierto conjunto de construcciones especiales cuyos nombres generalmente comienzan con la cadena Unchecked_ . Unchecked_Deallocation se puede prohibir efectivamente en una unidad de texto Ada aplicando pragma Pure a esta unidad. Se espera que los programadores utilicen las construcciones Unchecked_ con mucho cuidado y solo cuando sea necesario; los programas que no los utilizan son seguros para los tipos.

El lenguaje de programación SPARK es un subconjunto de Ada que elimina todas sus posibles ambigüedades e inseguridades y, al mismo tiempo, agrega contratos verificados estáticamente a las características del lenguaje disponibles. SPARK evita los problemas con punteros colgantes al no permitir la asignación en tiempo de ejecución por completo.

Ada2012 agrega contratos verificados estáticamente al lenguaje en sí (en forma de condiciones previas y posteriores, así como invariantes de tipo).

C

El lenguaje de programación C es de tipo seguro en contextos limitados; por ejemplo, se genera un error en tiempo de compilación cuando se intenta convertir un puntero a un tipo de estructura en un puntero a otro tipo de estructura, a menos que se utilice una conversión explícita. Sin embargo, una serie de operaciones muy comunes no son seguras de tipos; por ejemplo, la forma habitual de imprimir un número entero es algo así como printf("%d", 12), donde el %dindica printfen tiempo de ejecución esperar un argumento entero. (Algo como printf("%s", 12), que le dice a la función que espere un puntero a una cadena de caracteres y, sin embargo, proporciona un argumento entero, puede ser aceptado por los compiladores, pero producirá resultados indefinidos). Esto se mitiga parcialmente mediante la comprobación de algunos compiladores (como gcc) correspondencias de tipos entre argumentos de printf y cadenas de formato.

Además, C, como Ada, proporciona conversiones explícitas no especificadas o indefinidas; ya diferencia de Ada, los modismos que usan estas conversiones son muy comunes y han ayudado a darle a C una reputación de tipo inseguro. Por ejemplo, la forma estándar de asignar memoria en el montón es invocar una función de asignación de memoria, como malloc, con un argumento que indique cuántos bytes se requieren. La función devuelve un puntero sin tipo (tipo void *), que el código de llamada debe emitir explícita o implícitamente al tipo de puntero apropiado. Las implementaciones pre-estandarizadas de C requerían un elenco explícito para hacerlo, por lo tanto, el código se convirtió en la práctica aceptada. (struct foo *) malloc(sizeof(struct foo))

C ++

Algunas características de C ++ que promueven un código más seguro de tipos:

C#

C # es seguro para los tipos (pero no estáticamente seguro para los tipos). Tiene soporte para punteros sin tipo, pero se debe acceder a esto usando la palabra clave "inseguro" que puede prohibirse en el nivel del compilador. Tiene soporte inherente para la validación de conversión en tiempo de ejecución. Los elencos se pueden validar usando la palabra clave "as" que devolverá una referencia nula si el elenco no es válido, o usando un elenco de estilo C que arrojará una excepción si el elenco no es válido. Consulte Operadores de conversión de C Sharp .

La confianza indebida en el tipo de objeto (del que se derivan todos los demás tipos) corre el riesgo de frustrar el propósito del sistema de tipos C #. Por lo general, es una mejor práctica abandonar las referencias a objetos en favor de genéricos , similares a las plantillas en C ++ y genéricos en Java .

Java

El lenguaje Java está diseñado para reforzar la seguridad de los tipos. Cualquier cosa en Java sucede dentro de un objeto y cada objeto es una instancia de una clase .

Para implementar la aplicación de seguridad de tipo , es necesario asignar cada objeto, antes de su uso . Java permite el uso de tipos primitivos, pero solo dentro de los objetos asignados correctamente.

A veces, una parte del tipo de seguridad se implementa indirectamente: por ejemplo, la clase BigDecimal representa un número de punto flotante de precisión arbitraria, pero maneja solo números que pueden expresarse con una representación finita. La operación BigDecimal.divide () calcula un nuevo objeto como la división de dos números expresados ​​como BigDecimal.

En este caso, si la división no tiene representación finita, como cuando se calcula, por ejemplo, 1/3 = 0.33333 ..., el método divide () puede generar una excepción si no se define ningún modo de redondeo para la operación. Por tanto, la biblioteca, más que el lenguaje, garantiza que el objeto respeta el contrato implícito en la definición de clase.

ML estándar

El ML estándar tiene una semántica rigurosamente definida y se sabe que es seguro para los tipos. Sin embargo, algunas implementaciones, incluido el estándar ML de Nueva Jersey (SML / NJ), su variante sintáctica Mythryl y MLton , proporcionan bibliotecas que ofrecen operaciones inseguras. Estas instalaciones se utilizan a menudo junto con las interfaces de funciones externas de esas implementaciones para interactuar con código que no es ML (como bibliotecas C) que pueden requerir datos dispuestos de formas específicas. Otro ejemplo es el nivel superior interactivo SML / NJ en sí mismo, que debe usar operaciones inseguras para ejecutar el código ML ingresado por el usuario.

Modula-2

Modula-2 es un lenguaje fuertemente tipado con una filosofía de diseño que requiere que cualquier instalación insegura se marque explícitamente como insegura. Esto se logra "moviendo" dichas instalaciones a una pseudobiblioteca incorporada llamada SYSTEM desde donde deben importarse antes de que puedan usarse. La importación, por lo tanto, lo hace visible cuando se utilizan tales instalaciones. Lamentablemente, esto no se implementó en consecuencia en el informe en el idioma original y su implementación. Todavía quedaban instalaciones inseguras como la sintaxis de conversión de tipos y los registros de variantes (heredados de Pascal) que podrían usarse sin una importación previa. La dificultad de trasladar estas instalaciones al pseudo-módulo SYSTEM fue la falta de un identificador para la instalación que luego pudiera importarse, ya que solo se pueden importar identificadores, pero no la sintaxis. 

IMPORT SYSTEM; (* allows the use of certain unsafe facilities: *)
VAR word : SYSTEM.WORD; addr : SYSTEM.ADDRESS;
addr := SYSTEM.ADR(word);

(* but type cast syntax can be used without such import *)
VAR i : INTEGER; n : CARDINAL;
n := CARDINAL(i); (* or *) i := INTEGER(n);

El estándar ISO Modula-2 corrigió esto para la facilidad de conversión de tipos cambiando la sintaxis de conversión de tipos a una función llamada CAST que tiene que ser importada desde el pseudo-módulo SYSTEM. Sin embargo, otras instalaciones inseguras, como registros variantes, permanecieron disponibles sin ninguna importación desde el pseudo-módulo SYSTEM. 

IMPORT SYSTEM;
VAR i : INTEGER; n : CARDINAL;
i := SYSTEM.CAST(INTEGER, n); (* Type cast in ISO Modula-2 *)

A recent revision of the language applied the original design philosophy rigorously. First, pseudo-module SYSTEM was renamed to UNSAFE to make the unsafe nature of facilities imported from there more explicit. Then all remaining unsafe facilities where either removed altogether (for example variant records) or moved to pseudo-module UNSAFE. For facilities where there is no identifier that could be imported, enabling identifiers were introduced. In order to enable such a facility, its corresponding enabling identifier must be imported from pseudo-module UNSAFE. No unsafe facilities remain in the language that do not require import from UNSAFE. 

IMPORT UNSAFE;
VAR i : INTEGER; n : CARDINAL;
i := UNSAFE.CAST(INTEGER, n); (* Type cast in Modula-2 Revision 2010 *)

FROM UNSAFE IMPORT FFI; (* enabling identifier for foreign function interface facility *)
<*FFI="C"*> (* pragma for foreign function interface to C *)

Pascal

Pascal ha tenido una serie de requisitos de seguridad de tipos, algunos de los cuales se guardan en algunos compiladores. Cuando un compilador de Pascal dicta "tipificación estricta", no se pueden asignar dos variables entre sí a menos que sean compatibles (como la conversión de entero a real) o asignadas al subtipo idéntico. Por ejemplo, si tiene el siguiente fragmento de código: 

type
  TwoTypes = record
     I: Integer;
     Q: Real;
  end;

  DualTypes = record
    I: Integer;
    Q: Real;
  end;

var
  T1, T2:  TwoTypes;
  D1, D2:  DualTypes;

Bajo escritura estricta, una variable definida como TwoTypes no es compatible con DualTypes (porque no son idénticos, aunque los componentes de ese tipo definido por el usuario son idénticos) y una asignación de {{{1}}} es ilegal. Una asignación de {{{1}}} sería legal porque los subtipos para los que están definidos son idénticos. Sin embargo, una asignación como {{{1}}} sería legal.

Lisp común

En general, Common Lisp es un lenguaje de tipo seguro. Un compilador Common Lisp es responsable de insertar comprobaciones dinámicas para operaciones cuya seguridad de tipo no se puede probar estáticamente. Sin embargo, un programador puede indicar que un programa debe compilarse con un nivel más bajo de verificación dinámica de tipos. Un programa compilado en tal modo no se puede considerar con seguridad de tipos.

Ejemplos de C ++

Los siguientes ejemplos ilustran cómo los operadores de conversión de C ++ pueden romper la seguridad de tipos cuando se usan incorrectamente. El primer ejemplo muestra cómo los tipos de datos básicos se pueden convertir incorrectamente: 

#include <iostream>
using namespace std;

int main () {
    int   ival = 5;                              // integer value
    float fval = reinterpret_cast<float&>(ival); // reinterpret bit pattern
    cout << fval << endl;                        // output integer as float
    return 0;
}

En este ejemplo, reinterpret_castevita explícitamente que el compilador realice una conversión segura de un valor entero a un valor de punto flotante. Cuando el programa se ejecuta, generará un valor de coma flotante de basura. El problema podría haberse evitado escribiendo en su lugarfloat fval = ival;

El siguiente ejemplo muestra cómo las referencias a objetos se pueden abatir incorrectamente: 

#include <iostream>
using namespace std;

class Parent {
public:
    virtual ~Parent() {} // virtual destructor for RTTI
};

class Child1 : public Parent {
public:
    int a;
};

class Child2 : public Parent {
public:
    float b;
};

int main () {
    Child1 c1;
    c1.a = 5;
    Parent & p = c1;                     // upcast always safe
    Child2 & c2 = static_cast<Child2&>(p); // invalid downcast
    cout << c2.b << endl;          // will output garbage data
    return 0;
}

Las dos clases secundarias tienen miembros de diferentes tipos. Al reducir un puntero de clase padre a un puntero de clase secundaria, es posible que el puntero resultante no apunte a un objeto válido del tipo correcto. En el ejemplo, esto lleva a que se imprima el valor de basura. El problema podría haberse evitado reemplazando static_castcon dynamic_casteso arroja una excepción en conversiones no válidas.

Ver también

Notas

Referencias