La seguridad de tipos es una propiedad de un lenguaje de programación que caracteriza la seguridad y confiabilidad en la aplicación de su sistema de tipos .
Un sistema de tipo se denomina seguro ( ing. seguro ) o confiable ( ing. sonido ) si los programas que han pasado las comprobaciones de consistencia de tipo ( ing. programas bien tipificados o programas bien formados ) excluyen la posibilidad de errores de consistencia de tipo en ejecución hora [1 ] [2] [3] [4] [5] [6] .
Error de coincidencia de tipo o error de tipeo ( error de tipo en inglés ) - inconsistencia en los tipos de componentes de expresión en el programa, por ejemplo, un intento de usar un número entero como una función [7] . Los errores de coincidencia de tipos en tiempo de ejecución que faltan pueden generar errores e incluso bloqueos . La seguridad de un lenguaje no es sinónimo de ausencia total de errores, pero al menos estos se vuelven explorables dentro de la semántica del lenguaje (formal o informal) [8] .
Los sistemas de tipos confiables también se denominan fuertes ( eng. strong ) [1] [2] , pero la interpretación de este término a menudo se suaviza, además, a menudo se aplica a lenguajes que realizan comprobaciones dinámicas de consistencia de tipos ( fuerte y débil escribiendo ).
A veces, la seguridad se considera una propiedad de un programa en particular en lugar del lenguaje en el que está escrito, por la razón de que algunos lenguajes con seguridad de tipos permiten eludir o violar el sistema de tipos si el programador practica una seguridad de tipos deficiente. Se cree ampliamente que tales oportunidades en la práctica resultan ser una necesidad, pero esto es ficción [9] . El concepto de "seguridad del programa" es importante en el sentido de que una implementación de un lenguaje seguro puede ser en sí misma insegura. La puesta en marcha del compilador resuelve este problema, haciendo que el lenguaje sea seguro no solo en teoría sino también en la práctica.
Robin Milner acuñó la frase "Los programas que pasan la verificación de tipos no pueden 'desviarse'" [10] . En otras palabras, un sistema de tipo seguro evita operaciones deliberadamente erróneas que involucran tipos no válidos. Por ejemplo, la expresión 3 / "Hello, World"es obviamente errónea, ya que la aritmética no define la operación de dividir un número por una cadena. Técnicamente, la seguridad significa garantizar que el valor de cualquier expresión de tipo con verificación de tipo τsea un verdadero miembro del conjunto de valores τ, es decir, estará dentro del rango de valores permitido por el tipo estático de esa expresión. De hecho, hay matices en este requisito: consulte subtipos y polimorfismo para casos complejos.
Además, con el uso intensivo de mecanismos para definir nuevos tipos , se evitan errores lógicos resultantes de la semántica de varios tipos [5] . Por ejemplo, tanto los milímetros como las pulgadas son unidades de longitud y se pueden representar como números enteros, pero sería un error restar pulgadas a los milímetros, y el sistema de tipos desarrollado no lo permitirá (por supuesto, siempre que el programador use diferentes tipos). para valores expresados en diferentes unidades).datos, en lugar de describir ambas como variables de tipo entero). En otras palabras, la seguridad del lenguaje significa que el lenguaje protege al programador de sus propios posibles errores [9] .
Muchos lenguajes de programación de sistemas (p. ej. , Ada , C , C++ ) prevén operaciones no seguras ( poco sólidas ) o inseguras ( no seguras ) diseñadas para poder violar ( ing . violar ) el sistema de tipos; consulte conversión de tipos y escritura de juegos de palabras . En algunos casos, esto se permite solo en partes limitadas del programa, en otros no se distingue de las operaciones bien tipificadas [11] .
en la corriente principal[ clarificar ] No es raro ver que la seguridad de tipo se reduce a " seguridad de tipo de memoria ", lo que significa que los componentes de los objetos de un tipo agregado no pueden acceder a las ubicaciones de memoria asignadas para objetos de otro tipo . La seguridad de acceso a la memoria significa no poder copiar una cadena arbitraria de bits de un área de la memoria a otra. Por ejemplo, si un idioma proporciona un tipo que tiene un rango limitado de valores válidos y brinda la capacidad de copiar datos sin tipo en una variable de ese tipo, entonces esto no es seguro para el tipo porque potencialmente permite que una variable de tipo tenga un valor. eso no es válido para el tipo . Y, en particular, si un lenguaje tan inseguro permite escribir un valor entero arbitrario en una variable de tipo " puntero ", entonces la inseguridad del acceso a la memoria es obvia (ver puntero colgante ). Ejemplos de lenguajes inseguros son C y C++ [4] . En las comunidades de estos idiomas, cualquier operación que no provoque directamente que el programa se cuelgue se suele denominar "segura" . La seguridad de acceso a la memoria también significa evitar la posibilidad de desbordamientos del búfer , como intentar escribir objetos grandes en celdas asignadas para objetos de otro tipo de tamaño más pequeño. ttt
Los sistemas confiables de tipo estático son conservadores (redundantes) en el sentido de que rechazan incluso los programas que se ejecutarían correctamente. La razón de esto es que, para cualquier lenguaje completo de Turing , el conjunto de programas que pueden generar errores de coincidencia de tipos en tiempo de ejecución es algorítmicamente indecidible (ver el problema de detención ) [12] [13] . Como consecuencia, este tipo de sistemas proporcionan un grado de protección sustancialmente superior al necesario para garantizar la seguridad del acceso a la memoria. Por otro lado, la seguridad de algunas acciones no puede probarse estáticamente y debe controlarse dinámicamente, por ejemplo, indexar una matriz de acceso aleatorio. Dicho control puede ser llevado a cabo por el propio sistema de tiempo de ejecución del lenguaje o directamente por funciones que implementan tales operaciones potencialmente inseguras.
Los lenguajes fuertemente tipados dinámicamente (por ejemplo, Lisp , Smalltalk ) no permiten la corrupción de datos debido al hecho de que un programa que intenta convertir un valor a un tipo incompatible genera una excepción. Las ventajas de la escritura dinámica fuerte sobre la seguridad de tipos incluyen la falta de conservadurismo y, como resultado, la expansión de la gama de tareas de programación a resolver. El precio de esto es la inevitable disminución de la velocidad de los programas, así como la necesidad de un número significativamente mayor de ejecuciones de prueba para identificar posibles errores. Por lo tanto, muchos lenguajes combinan las capacidades de control de consistencia de tipo estático y dinámico de una forma u otra. [14] [12] [1]
Ada (el lenguaje con mayor seguridad de tipos en la familia Pascal ) se centra en el desarrollo de sistemas integrados confiables , controladores y otras tareas de programación del sistema . Para implementar secciones críticas, Ada proporciona una serie de construcciones inseguras cuyos nombres generalmente comienzan con Unchecked_.
El lenguaje SPARK es un subconjunto de Ada. Eliminó características inseguras pero agregó características de diseño por contrato . SPARK elimina la posibilidad de punteros colgantes al eliminar la posibilidad misma de asignación de memoria dinámica. Los contratos verificados estáticamente se han agregado a Ada2012.
Hoare , en una conferencia de Turing, argumentó que las comprobaciones estáticas no son suficientes para garantizar la confiabilidad: la confiabilidad es principalmente una consecuencia de la simplicidad [15] . Luego predijo que la complejidad de Ada provocaría catástrofes.
BitC es un lenguaje híbrido que combina las características de bajo nivel de C con la seguridad de Standard ML y la concisión de Scheme . BitC se centra en el desarrollo de sistemas integrados robustos , controladores y otras tareas de programación de sistemas .
El lenguaje exploratorio Cyclone es un dialecto seguro de C que toma prestadas muchas ideas de ML (incluido el polimorfismo paramétrico de tipo seguro ). Cyclone está diseñado para las mismas tareas que C, y después de hacer todas las comprobaciones, el compilador genera código en ANSI C. Cyclone no requiere una máquina virtual o recolección de elementos no utilizados para la seguridad dinámica; en cambio, se basa en la administración de memoria a través de regiones . Cyclone establece un listón más alto para la seguridad del código fuente y, debido a la naturaleza insegura de C, transferir incluso programas simples de C a Cyclone puede requerir algo de trabajo, aunque mucho se puede hacer dentro de C antes de cambiar los compiladores. Por lo tanto, Cyclone a menudo se define no como un dialecto de C, sino como " un lenguaje sintáctica y semánticamente similar a C ".
Muchas de las ideas de Cyclone han llegado al lenguaje Rust . Además de un fuerte tipado estático, se ha agregado al lenguaje un análisis estático de la vida útil de los punteros basado en el concepto de "propiedad". Restricciones estáticas implementadas que bloquean el acceso a la memoria potencialmente incorrecto: no se permiten punteros nulos, no pueden aparecer variables no inicializadas y desinicializadas, se prohíbe compartir variables mutables entre varias tareas. Se requiere verificar la matriz fuera de los límites.
Haskell (un descendiente de ML ) se diseñó originalmente como un lenguaje puro lleno de tipos , que se suponía que haría que el comportamiento de los programas en él fuera aún más predecible que en los dialectos anteriores de ML . Sin embargo, más adelante en el lenguaje estándar , se proporcionaron operaciones inseguras [16] [17] , que son necesarias en la práctica diaria, aunque están marcadas con los identificadores apropiados (empezando por ) [18] . unsafe
Haskell también proporciona funciones de tipeo dinámico débil , y la implementación del mecanismo de manejo de excepciones a través de estas funciones se incluyó en el estándar del lenguaje . Su uso puede hacer que los programas se cuelguen, por lo que Robert Harper llamó a Haskell " extremadamente inseguro " [18] . Considera inaceptable que las excepciones tengan un tipo definido por el usuario en el contexto de una clase de tipos , dado que las excepciones son lanzadas por código seguro (fuera de la mónada ); y clasifica el mensaje de error interno del compilador como inapropiado para el eslogan de Milner . En la discusión que siguió, se mostró cómo se pueden implementar en Haskell las excepciones estáticamente seguras de tipos de estilo ML estándar . Typeable IO
Lisp "puro" (mínimo) es un lenguaje de un solo tipo (es decir, cualquier construcción pertenece al tipo " S-expression ") [19] , aunque incluso las primeras implementaciones comerciales de Lisp proporcionaron al menos un cierto número de átomos . . La familia de descendientes del lenguaje Lisp está representada en su mayoría por lenguajes de tipado fuertemente dinámico , pero hay lenguajes de tipado estático que combinan ambas formas de tipeo.
Common Lisp es un lenguaje fuertemente tipado dinámicamente, pero brinda la capacidad de ( manifestar ) asignar tipos explícitamente (y el compilador SBCL puede inferirlos por sí mismo ) , sin embargo, esta capacidad se usa para optimizar y hacer cumplir controles dinámicos y no implica seguridad de tipo estático. El programador puede establecer un nivel más bajo de controles dinámicos para el compilador con el fin de mejorar el rendimiento, y el programa compilado de esta manera ya no puede considerarse seguro [20] [21] .
El lenguaje Scheme también es un lenguaje fuertemente tipado dinámicamente, pero el de Stalin infiere tipos estáticamente , usándolos para optimizar programas agresivamente. Los lenguajes "Typed Racket" (una extensión de Racket Scheme ) y Shen son de tipo seguro. Clojure combina una fuerte escritura dinámica y estática.
El lenguaje ML se desarrolló originalmente como un sistema interactivo de prueba de teoremas y solo más tarde se convirtió en un lenguaje compilado independiente de propósito general. Se ha dedicado mucho esfuerzo a probar la confiabilidad del sistema de tipo Hindley-Milner paramétricamente polimórfico subyacente al ML . La prueba de seguridad se construye para un subconjunto puramente funcional ( "ML funcional" ), una extensión por tipos de referencia ( "ML de referencia" ), una extensión por excepciones ( "ML de excepción" ), un lenguaje que combina todas estas extensiones ( " ML funcional"). Core ML" ), y finalmente, sus extensiones con continuaciones de primera clase ( "Control ML" ), primero monomórficas, luego polimórficas [2] .
La consecuencia de esto es que los descendientes de ML a menudo se consideran a priori como de tipo seguro, aunque algunos de ellos difieren las comprobaciones significativas al tiempo de ejecución ( OCaml ), o se desvían de la semántica para la que se construye la prueba de seguridad, y explícitamente contienen inseguro características ( Haskell ). Los lenguajes de la familia ML se caracterizan por un soporte desarrollado para tipos de datos algebraicos , cuyo uso contribuye significativamente a la prevención de errores lógicos , lo que también respalda la impresión de seguridad de tipos.
Algunos descendientes de ML también son herramientas de prueba interactivas ( Idris , Mercury , Agda ). Muchos de ellos, aunque podrían usarse para el desarrollo directo de programas con confiabilidad comprobada, se usan con mayor frecuencia para verificar programas en otros idiomas, debido a razones tales como alta intensidad de uso, baja velocidad, falta de FFI y así sucesivamente. Entre los descendientes de ML con confiabilidad comprobada, Standard ML y el prototipo de su sucesor de desarrollo posterior ML [22] (anteriormente conocido como "ML2000") se destacan como lenguajes orientados a la industria .
El lenguaje ML estándar (el más antiguo de la familia de lenguajes ML ) se centra en el desarrollo de programas de velocidad industrial a gran escala 23] . El lenguaje tiene una definición formal estricta y su seguridad estática y dinámica ha sido probada [24] . Después de una verificación estática de la consistencia de las interfaces de los componentes del programa (incluidos los generados , consulte Functors ML ), el sistema de tiempo de ejecución admite un control de seguridad adicional . Como consecuencia, incluso un programa de ML estándar con un error siempre se comporta como un programa de ML: puede entrar en cálculos para siempre o dar al usuario un mensaje de error, pero no puede bloquearse [9] .
Sin embargo, algunas implementaciones ( SML/NJ , Mythryl , MLton ) incluyen bibliotecas no estándar que proporcionan ciertas operaciones no seguras (sus identificadores comienzan con Unsafe). Estas capacidades son necesarias para la interfaz de lenguaje externo de estas implementaciones, que proporciona interacción con código que no es de ML (por lo general , código C que implementa componentes de programa críticos para la velocidad), lo que puede requerir una representación de bits peculiar de los datos. Además, muchas implementaciones de Standard ML , aunque escritas en sí mismas , utilizan un sistema de tiempo de ejecución escrito en C. Otro ejemplo es el modo REPL del compilador SML/NJ , que utiliza operaciones no seguras para ejecutar el código ingresado de manera interactiva por el programador.
El lenguaje Alice es una extensión de Standard ML , que brinda sólidas capacidades de escritura dinámica .