¿Cuáles son los beneficios de seguridad de un sistema tipo?

Los sistemas de tipos evitan errores

Los sistemas de tipos eliminan los programas ilegales. Considera el siguiente código de Python.

 a = 'foo'
 b = True
 c = a / b

En Python, este programa falla; lanza una excepción. En un lenguaje como Java, C #, Haskell , como sea, este no es un programa legal. Evita por completo estos errores porque simplemente no son posibles en el conjunto de programas de entrada.

Del mismo modo, un mejor sistema de tipos descarta más errores. Si saltamos a sistemas de tipos súper avanzados, podemos decir cosas como esta:

 Definition divide x (y : {x : integer | x /= 0}) = x / y

Ahora el sistema de tipos garantiza que no hay errores de división por 0.

¿Qué tipo de errores

Aquí hay una breve lista de los errores que pueden evitar los sistemas de tipos

1. Errores fuera de rango
2. inyección SQL
3. Generalizar 2, muchos problemas de seguridad (para lo que comprobación de manchas es en Perl )
4. Errores fuera de secuencia (olvidando llamar a init)
5. Forzar el uso de un subconjunto de valores (por ejemplo, solo enteros mayores que 0)
6. Gatitos nefarios (Sí, era una broma)
7. Errores de pérdida de precisión
8. Errores de memoria transaccional del software (STM) (esto requiere pureza, que también requiere tipos)
9. Generalizar 8, controlar los efectos secundarios
10. Invariantes sobre estructuras de datos (¿está equilibrado un árbol binario?)
11. Olvidando una excepción o lanzando la incorrecta

Y recuerda, esto también está en compilar a la vez. No es necesario escribir pruebas con una cobertura de código del 100% para verificar simplemente los errores de tipo, el compilador simplemente lo hace por usted :)

Estudio de caso: cálculo lambda mecanografiado

Bien, examinemos el más simple de todos los sistemas de tipo, simplemente cálculo lambda escrito .

Básicamente hay dos tipos,

Type = Unit | Type -> Type

Y todos los términos son variables, lambdas o aplicación. En base a esto, podemos probar que cualquier programa bien escrito termina. Nunca hay una situación en la que el programa se atasque o se duplique para siempre. Esto no es demostrable en el cálculo lambda normal porque, bueno, no es cierto.

Piensa en esto, podemos usar sistemas de tipos para garantizar que nuestro programa no se ejecute nunca, más bien, ¿no?

desvío en tipos dinámicos

Los sistemas de tipo dinámico pueden ofrecer garantías idénticas a los sistemas de tipo estático, pero en tiempo de ejecución en lugar de tiempo de compilación. En realidad, dado que es tiempo de ejecución, puedes ofrecer más información. Sin embargo, se pierden algunas garantías, especialmente sobre propiedades estáticas como la terminación.

Por lo tanto, los tipos dinámicos no descartan ciertos programas, sino que enrutan programas mal formados a acciones bien definidas, como lanzar excepciones.

TLDR

Por lo tanto, a largo plazo, los sistemas de tipos descartan ciertos programas. Muchos de los programas están rotos de alguna manera, por lo tanto, con los sistemas de tipo evitamos estos programas rotos.

La realidad misma está escrita. No puedes agregar longitudes a pesos. Y mientras puede agregar pies a metros (ambos son unidades de longitud), debe escalar al menos uno de los dos. Si no lo haces, puedes estrellar tu misión a Marte, literalmente.

En un sistema de seguridad contra tipos, agregar dos longitudes expresadas en unidades diferentes habría sido un error o habría causado un lanzamiento automático.

Un sistema de tipos lo ayuda a evitar errores de codificación simples o, más bien, le permite al compilador capturar esos errores por usted.

Por ejemplo, en JavaScript y Python, el siguiente problema a menudo solo se detectará en tiempo de ejecución, y dependiendo de la calidad / rareza de la prueba de la condición puede llegar a producción:

if (someRareCondition)
     a = 1
else
     a = {1, 2, 3}

// 10 lines below
k = a.length

Mientras que un lenguaje de tipo fuerte lo obligará a declarar explícitamente que a es una matriz y no le permitirá asignar un número entero. De esta manera, no hay ninguna posibilidad de que a no tenga length , incluso en los casos más raros.

Cuanto antes en el ciclo de desarrollo de software pueda detectar un error, menos costoso es solucionarlo. Considere un error que haga que su cliente más grande, o todos sus clientes pierdan datos. ¡Un error de este tipo podría ser el final de su empresa si solo se detecta después de que los clientes reales hayan perdido datos! Es claramente menos costoso encontrar y corregir este error antes de moverlo a producción.

Incluso para errores menos costosos, se gasta más tiempo y energía si se involucran los evaluadores que si los programadores pueden encontrarlo y solucionarlo. Es más barato si no se comprueba en el control de código fuente donde otros programadores pueden crear software que se basa en él. La seguridad de tipos evita que se compilen ciertas clases de errores, eliminando así casi todo el costo potencial de esos errores.

Pero esa no es toda la historia. Como cualquier persona que programe en un lenguaje dinámico le dirá, algunas veces es bueno que su programa se compile para que pueda probar una parte de ella sin que cada pequeño detalle se resuelva. Hay una compensación entre la seguridad y la comodidad. Las pruebas unitarias pueden mitigar algunos de los riesgos de usar un lenguaje dinámico, pero escribir y mantener buenas pruebas unitarias tiene su propio costo, que puede ser mayor que el de usar un lenguaje seguro para el tipo.

Si está experimentando, si su código solo se usará una vez (como un informe de una sola vez), o si se encuentra en una situación en la que no se molestaría en escribir una prueba de unidad de todos modos, entonces un lenguaje dinámico es probablemente perfecto para ti Si tiene una aplicación grande y desea cambiar una parte sin romper el resto, entonces escriba seguridad es un salvavidas. Los tipos de errores de captura de seguridad son exactamente el tipo de errores que los humanos tienden a pasar por alto o se equivocan al refactorizar.

Introducción

La seguridad de tipo se puede lograr con los lenguajes de tipo estático (compilado, control de tipo estático) y / o en tiempo de ejecución (evaluado, control de tipo dinámico). Según Wikipedia un '... sistema de tipos fuertes se describe como uno en el que no hay posibilidad de un error de tipo de tiempo de ejecución no verificado (ed Luca Cardelli). En otros escritos, la ausencia de errores de tiempo de ejecución no controlados se conoce como seguridad o tipo seguridad ... '

Seguridad: verificación de tipo estático

Clásicamente, la seguridad de tipos ha sido sinónimo de escritura estática, en lenguajes como C, C ++ y Haskell, que están diseñados para detectar desajustes de tipos cuando se compilan. Esto tiene la ventaja de evitar condiciones potencialmente indefinidas o propensas a errores cuando se ejecuta el programa. Esto puede ser invaluable cuando existe el riesgo de que los tipos de punteros no coincidan, por ejemplo, una situación que podría llevar a consecuencias catastróficas si no se detecta. En este sentido, la escritura estática se considera sinónimo de seguridad de memoria.

La escritura estática no es completamente segura, pero mejora la seguridad , sin embargo. Incluso los sistemas tipificados estáticamente pueden tener consecuencias catastróficas. Muchos expertos consideran que la tipificación estática se puede usar para escribir sistemas más robustos y menos propensos a errores (de misión crítica).

Los lenguajes de tipo estático pueden ayudar a reducir el riesgo de pérdida de datos o pérdida de precisión en el trabajo numérico, que puede ocurrir debido a una falta de coincidencia o truncamiento del doble al flotante o integral de la integral y los tipos de flotadores.

Hay una ventaja en el uso de lenguajes de tipo estático para la eficiencia y la velocidad de ejecución. El tiempo de ejecución se beneficia de no tener que determinar los tipos durante la ejecución.

Seguridad - Comprobación de tipo de tiempo de ejecución

Erlang, por ejemplo, es un tipo declarativo, escribe dinámicamente el idioma verificado que se ejecuta en una máquina virtual. El código de Erlang se puede compilar en bytes. Erlang es considerado como el lenguaje de tolerancia a fallas más importante y de misión crítica disponible, y se informa que Erlang tiene una confiabilidad de nueve 9's (99.9999999% o no más de 31.5 msegs por año).

Ciertos idiomas, como Common Lisp, no están tipificados de forma estática, pero se pueden declarar los tipos que se deseen, lo que puede ayudar a mejorar la velocidad y la eficiencia. También se debe tener en cuenta que muchos de los lenguajes interpretados más utilizados, como Python, están, debajo del ciclo de evaluación, escritos en lenguajes de tipo estático como C o C ++. Tanto Commom Lisp como Python se consideran seguros de tipo según la definición anterior.

  

Se pierden los beneficios de seguridad de un sistema de tipo.

     

En primer lugar, ¿qué es realmente la seguridad? ¿Protección contra la corrupción de datos, hackers, mal funcionamiento del sistema, etc.?

     

¿Cuáles son los beneficios de seguridad de un sistema tipo? ¿En qué se diferencia un sistema de tipo que le permite brindar estos beneficios de seguridad?

Siento que los sistemas de tipos tienen una visión tan negativa. Un sistema de tipo es más una garantía que la prueba de la ausencia de errores. Este último es una consecuencia del sistema de tipos. Un sistema de tipo para un lenguaje de programación es una forma de producir, en tiempo de compilación, una prueba de que un programa cumple algún tipo de especificación.

El tipo de especificación que se puede codificar como un tipo depende del idioma, o más directamente, de la fuerza del sistema de tipos del idioma.

El tipo más básico de especificación es una garantía sobre el comportamiento de entrada / salida de las funciones y de la validez del interior de un cuerpo de función. Considere el encabezado de una función

f : (Int,Int) -> String

Un buen sistema de tipos se asegurará de que f solo se aplique a los objetos que producirán un par de Int cuando se evalúe, y garantiza que f siempre producirá una cadena.

Algunas declaraciones en un idioma, como los bloques if-then, no tienen un comportamiento de entrada / salida; aquí el sistema de tipos garantiza que cada declaración o declaración en el bloque es válida; es decir, aplica operaciones a objetos del tipo correcto. Estas garantías son compostables.

Además, esto da una especie de condición de seguridad de memoria. La cita con la que estás tratando es sobre el casting. En algunos casos, la conversión está bien, como la conversión de un Int de 32 bits a un Int de 64 bits. Sin embargo, en general, se bloquea el sistema de tipos.

Considera

Foo x = new Foo(3,4,5,6);
f((Int)x,(Int)x);

Debido a la conversión, x se convierte en un Int, por lo que técnicamente lo anterior hace una comprobación de tipo; sin embargo, realmente anula el propósito de la comprobación de tipos.

Una cosa que podría hacer un sistema de tipos diferente y mejor es desautorizar los conversos (A) x donde x antes del caso es del tipo B, a menos que B sea un subtipo (o subobjeto) de A. Las ideas de la teoría de subtipos se han realizado Se usa en seguridad para eliminar la posibilidad de ataques de desbordamiento / subdesbordamiento de enteros.

Summary

Un sistema de tipo es una forma de probar que un programa cumple con algún tipo de especificación. Los beneficios que puede proporcionar un sistema de tipos dependen de la solidez del sistema de tipos utilizado.

Una ventaja no mencionada todavía para un sistema de tipos se centra en el hecho de que muchos programas se leen más de lo que se escriben, y en muchos casos un sistema de tipos puede permitir que se especifique una gran cantidad de información de una manera que sea concisa y precisa. Puede ser fácilmente digerido por alguien que lee el código. Si bien los tipos de parámetros no reemplazan a los comentarios descriptivos, la mayoría de las personas encontrarán que es más rápido leer: "int Distancia"; o Distance As Int32 que leer "La distancia debe ser un número entero +/- 2147483647"; pasar las fracciones puede producir resultados inconsistentes ". Además, los tipos de parámetros pueden ayudar a reducir la brecha entre lo que hace una implementación particular de una API, en comparación con lo que las personas que llaman tienen derecho a confiar. Por ejemplo, si una implementación particular de JavaScript de una API usa sus parámetros de una manera que obligarían a cualquier cadena a ser numérica, puede ser poco claro si los llamadores pueden confiar en dicho comportamiento, o si otras implementaciones de la API pueden funcionar incorrectamente si se les dan cadenas. Tener un método cuyo parámetro se especifique como Double dejaría en claro que cualquier valor de cadena debe ser forzado por el llamante antes de ser pasado; tener un método con una sobrecarga que acepte Double y otro que acepte String dejaría algo más claro que los llamadores que tienen cadenas para pasarlos como tales.

  

En primer lugar, ¿qué es realmente la seguridad? ¿Protección contra la corrupción de datos, hackers, mal funcionamiento del sistema, etc.?

Todas las otras respuestas y más. En general, "seguridad de tipos" simplemente significa que ninguno de los programas que compila un compilador contendrá errores de tipo.

Ahora, ¿qué es un error de tipo? En principio, puede especificar cualquier propiedad no deseada como error de tipo, y algunos sistemas de tipo podrán garantizar de forma estática que ningún programa tenga tal error.

Por "propiedad" arriba, me refiero a algún tipo de proposición lógica que se aplique a su programa, por ejemplo, "todos los índices están dentro de los límites de la matriz". Otros tipos de propiedades incluyen, "todos los punteros diferidos son válidos", "este programa no realiza ninguna E / S", o "este programa realiza E / S solo para / dev / null", etc. Casi cualquier tipo de la propiedad se puede especificar y el tipo se puede verificar de esta manera, dependiendo de la expresividad de su sistema de tipos.

Los sistemas de tipo dependientes se encuentran entre los sistemas de tipo más generales, a través de los cuales puede hacer cumplir prácticamente cualquier propiedad que desee. Sin embargo, no es necesariamente fácil hacerlo, ya que las propiedades sofisticadas están sujetas a carácter incompleto cortesía de Gödel .