En informática y ,ciberseguridad, la seguridad de tipos es la medida en que un lenguaje de programación disminuye o previene los errores de tipo . Un error de tipo es un comportamiento de programa erróneo o indeseable 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 ). La seguridad de tipos a veces se considera alternativamente como una propiedad de un programa de ordenador en vez de una propiedad del lenguaje con el que está escrito ese programa; es decir, algunos lenguajes tienen funciones de seguridad de tipos que pueden ser evitadas por programadores que utilizan prácticas que presentan una seguridad de tipos deficiente. 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 ejecución de tipos puede ser estática, detectando posibles errores en tiempo de compilación, o dinámica, asociando la información de tipos con valores en tiempo de ejecución y consultándolos según sea necesario para detectar errores inmediatos, o una combinación de ambos.
Los comportamientos clasificados como errores de tipo por un lenguaje de programación dado son generalmente los que resultan de realizar intentos de operaciones con valores que no son del tipo de datos apropiado. Esta clasificación se basa en parte en opiniones; puede implicar que cualquier operación que no dé lugar a fallos del programa, fallas de seguridad u otras fallas obvias es legítima y no necesita ser considerada un error, o puede implicar que cualquier incumplimiento de la intención explícita del programador (como se comunica a través de anotaciones mecanografiadas) sea errónea y no "a prueba de tipos".
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 subtipado y polimorfismo.
La seguridad de tipos está estrechamente relacionada con la seguridad de memoria, una restricción en la capacidad de copiar patrones de bits arbitrarios de una localización de memoria a otra. Por ejemplo, en una implementación de un lenguaje que tiene un tipo , de modo 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 tiene seguridad de tipos porque la operación podría asignar un valor que no sea de a esa variable.
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 cualquier tipo de error catastrófico.
Definiciones El código con seguridad de tipos 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 sentido 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 eslogan depende del estilo de semántica formal que se utilice para un lenguaje 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" de los programas permanece invariable según las reglas de transición (es decir, reglas de evaluación o reglas de reducción) del lenguaje. Progreso Un programa bien tipado nunca se "atasca", lo que significa que las expresiones en el programa serán evaluadas a un valor, o hay una regla de transición para ello; en otras palabras, el programa nunca entra en un estado indefinido donde no son posibles más transiciones.
Estas propiedades no existen en el vacío; están vinculadas 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 de 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 lenguaje es de tipo seguro si las únicas operaciones que se pueden realizar con los datos en el lenguaje son las autorizadas por el tipo de datos".
Relación con otras formas de seguridad La seguridad de tipos 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 de caracteres . Seguridad de la memoria Los punteros salvajes pueden surgir cuando un puntero apunta a un objeto de tipo un tipo y se trata como un puntero que apunta 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 heap. Esto puede ocurrir cuando un objeto más grande de un tipo se copia de manera brusca 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 agregarse. 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.Standard ML. Smlnj.org. Retrieved on 2013-11-02. Se cree que algunos otros lenguajes como Haskell cumplen con alguna definición de seguridad de tipos, siempre que no se utilicen ciertas características de "escape" (por ejemplo, unsafePerformIO de Haskell, que se usa para "escapar" del entorno restringido habitual en el que se posible, evita el sistema de tipos y, por lo tanto, se puede utilizar para romper la seguridad del tipo. ). 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; dichos errores podrían hacer que un tipo de implementación determinado no sea seguro en determinadas circunstancias. Una de las primeras versiones de la máquina virtual Java de Sun´s era vulnerable a este tipo de problema.
Tipado 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 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 conserve la integridad del objeto.La seguridad de tipos también es una cuestión de una buena definición de clase: los métodos públicos que modifican el estado interno de un objeto deben preservar 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.
Problemas de seguridad de tipos en lenguajes específicos
Ada Ada fue diseñado para ser utilizado en sistemas integrados, controladores de dispositivos y otras formas de programación de sistemas, 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_ . 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 los punteros colgantes al no permitir la asignación en tiempo de ejecución por completo.
Ada2012 agrega contratos verificados estáticamente al propio lenguaje (en forma de condiciones previas y posteriores, así como invariantes de tipo).
C