¿Es posible evaluar mediante programación la seguridad de código arbitrario?

Últimamente he estado pensando mucho en el código seguro. A salvo de amenazas. Seguro para la memoria. No va a explotar en su cara con una caja fuerte segura. Pero en aras de la claridad en la pregunta, usemos el modelo de seguridad de Rust como nuestra definición actual.

A menudo, garantizar la seguridad es un problema de cuán grande es la red, porque, como lo demuestra la necesidad de Rust unsafe, hay algunas ideas de programación muy razonables, como la concurrencia, que no se pueden implementar en Rust sin usar la unsafepalabra clave . Aunque la concurrencia se puede hacer perfectamente segura con bloqueos, mutexes, canales y aislamiento de memoria o lo que sea, esto requiere trabajar fuera del modelo de seguridad de Rust unsafey luego asegurar manualmente al compilador que, "Sí, sé lo que estoy haciendo . Esto parece inseguro, pero he demostrado matemáticamente que es perfectamente seguro ".

Pero generalmente, esto se reduce a hacer modelos manualmente de estas cosas y demostrar que están a salvo con los probadores de teoremas . Desde una perspectiva de la informática (es posible) y una perspectiva práctica (va a tomar la vida del universo), ¿es razonable imaginar un programa que toma código arbitrario en un lenguaje arbitrario y evalúa si es o no " A prueba de herrumbre "?

Advertencias :

• Es fácil señalar que el programa podría ser inofensivo y, por lo tanto, el problema de detención nos falla. Digamos que cualquier programa alimentado al lector está garantizado para detener
• Si bien el objetivo es "código arbitrario en un idioma arbitrario", por supuesto, soy consciente de que esto depende de la familiaridad del programa con el idioma elegido, que tomaremos como un hecho

Lo que finalmente estamos hablando aquí es el tiempo de compilación vs tiempo de ejecución.

Los errores de tiempo de compilación, si lo piensa, en última instancia equivalen a que el compilador pueda determinar qué problemas tiene en su programa incluso antes de que se ejecute. Obviamente no es un compilador de "lenguaje arbitrario", pero volveré sobre eso en breve. Sin embargo, el compilador, en toda su sabiduría infinita, no enumera todos los problemas que puede determinar el compilador. Esto depende en parte de qué tan bien esté escrito el compilador, pero la razón principal de esto es que muchas cosas se determinan en tiempo de ejecución .

Los errores de tiempo de ejecución, como ya conoce, estoy seguro, como yo, es cualquier tipo de error que ocurre durante la ejecución del programa en sí. Esto incluye dividir por cero, excepciones de puntero nulo, problemas de hardware y muchos otros factores.

La naturaleza de los errores de tiempo de ejecución significa que no puede anticipar dichos errores en tiempo de compilación. Si pudieras, casi seguramente se comprobarían en tiempo de compilación. Si pudiera garantizar que un número es cero en el momento de la compilación, podría realizar ciertas conclusiones lógicas, como dividir cualquier número por ese número dará como resultado un error aritmético causado por la división por cero.

Como tal, de una manera muy real, el enemigo de garantizar programáticamente el funcionamiento adecuado de un programa está realizando verificaciones de tiempo de ejecución en lugar de verificaciones de tiempo de compilación. Un ejemplo de esto podría ser realizar una conversión dinámica a otro tipo. Si esto está permitido, usted, el programador, esencialmente anula la capacidad del compilador de saber si es algo seguro. Algunos lenguajes de programación han decidido que esto es aceptable, mientras que otros al menos le avisarán en el momento de la compilación.

Otro buen ejemplo podría ser permitir que los nulos formen parte del lenguaje, ya que pueden producirse excepciones de puntero nulo si se permiten nulos. Algunos lenguajes han eliminado este problema por completo al evitar que las variables que no se declaran explícitamente puedan contener valores nulos para ser declarados sin que se les asigne inmediatamente un valor (tome Kotlin por ejemplo). Si bien no puede eliminar un error de tiempo de ejecución de excepción de puntero nulo, puede evitar que suceda eliminando la naturaleza dinámica del lenguaje. En Kotlin, puede forzar la posibilidad de mantener valores nulos, por supuesto, pero no hace falta decir que este es un "comprador cuidado" metafórico, ya que debe declararlo explícitamente como tal.

¿Podría conceptualmente tener un compilador que pueda verificar errores en todos los idiomas? Sí, pero probablemente sería un compilador torpe y altamente inestable en el que tendría que proporcionar necesariamente el idioma que se está compilando de antemano. Tampoco podía saber muchas cosas sobre su programa, más de lo que los compiladores para idiomas específicos saben ciertas cosas sobre él, como el problema de interrupción como mencionó. Resulta que es imposible obtener una gran cantidad de información que pueda ser interesante aprender sobre un programa. Esto ha sido probado, por lo que no es probable que cambie en el corto plazo.

Volviendo a su punto principal. Los métodos no son automáticamente seguros para subprocesos. Hay una razón práctica para esto, que es que los métodos seguros para subprocesos también son más lentos incluso cuando no se usan subprocesos. Rust decide que pueden eliminar los problemas de tiempo de ejecución al hacer que los métodos sean seguros para los subprocesos de forma predeterminada, y esa es su elección. Sin embargo, tiene un costo.

Puede ser posible demostrar matemáticamente la corrección de un programa, pero sería con la advertencia de que literalmente tendría cero funciones de tiempo de ejecución en el lenguaje. Podrías leer este idioma y saber lo que hace sin sorpresas. El lenguaje probablemente se vería de naturaleza muy matemática, y eso probablemente no sea una coincidencia allí. La segunda advertencia es que aún se producen errores de tiempo de ejecución , que pueden no tener nada que ver con el programa en sí. Por lo tanto, el programa puede ser probada correcta, asumiendo una serie de supuestos sobre el equipo que se está ejecutando en son precisos y no cambian, lo que por supuesto siempre no suceda de todos modos y frecuencia.

Los sistemas de tipos son pruebas verificables automáticamente de algunos aspectos de corrección. Por ejemplo, el sistema de tipos de Rust puede probar que una referencia no sobrevive al objeto referenciado, o que un objeto referenciado no es modificado por otro hilo.

Pero los sistemas de tipos son bastante restringidos:

• Rápidamente se encuentran con problemas de capacidad de decisión. En particular, el sistema de tipos en sí debería ser decidible, sin embargo, muchos sistemas de tipos prácticos se completan accidentalmente con Turing (incluyendo C ++ debido a plantillas y Rust debido a rasgos). Además, ciertas propiedades del programa que están verificando podrían ser indecidibles en el caso general, sobre todo si algunos programas se detienen (o divergen).

• Además, los sistemas de tipos deben ejecutarse rápidamente, idealmente en tiempo lineal. No todas las pruebas posibles deben aparecer en el sistema de tipos. Por ejemplo, generalmente se evita el análisis completo del programa, y ​​las pruebas se analizan en módulos o funciones individuales.

Debido a estas limitaciones, los sistemas de tipos tienden a verificar solo propiedades bastante débiles que son fáciles de probar, por ejemplo, que una función se llama con valores de tipo correcto. Sin embargo, incluso eso limita sustancialmente la expresividad, por lo que es común tener soluciones alternativas (como interface{}en Go, dynamicen C #, Objecten Java, void*en C) o incluso usar lenguajes que evitan por completo la escritura estática.

Cuantas más propiedades verifiquemos, menos expresivo será el lenguaje. Si ha escrito Rust, conocerá estos momentos de "lucha con el compilador" en los que el compilador rechaza el código aparentemente correcto, porque no pudo probar la corrección. En algunos casos, no es posible expresar un determinado programa en Rust, incluso cuando creemos que podemos demostrar su corrección. El unsafemecanismo en Rust o C # le permite escapar de los límites del sistema de tipos. En algunos casos, aplazar las comprobaciones al tiempo de ejecución puede ser otra opción, pero esto significa que no podemos rechazar algunos programas no válidos. Esto es una cuestión de definición. Un programa Rust que entra en pánico es seguro en lo que respecta al sistema de tipos, pero no necesariamente desde la perspectiva de un programador o usuario.

Los idiomas están diseñados junto con su sistema de tipos. Es raro que se imponga un nuevo sistema de tipos en un lenguaje existente (pero vea, por ejemplo, MyPy, Flow o TypeScript). El lenguaje intentará facilitar la escritura de código que se ajuste al sistema de tipos, por ejemplo, ofreciendo anotaciones de tipo o introduciendo estructuras de flujo de control fáciles de probar. Diferentes idiomas pueden terminar con diferentes soluciones. Por ejemplo, Java tiene el concepto de finalvariables que se asignan exactamente una vez, similar a las no mutvariables de Rust :

final int x;
if (...) { ... }
else     { ... }
doSomethingWith(x);

Java tiene reglas de sistema de tipo para determinar si todas las rutas asignan la variable o terminan la función antes de que se pueda acceder a la variable. Por el contrario, Rust simplifica esta prueba al no tener variables declaradas pero no diseñadas, pero le permite devolver valores de las declaraciones de flujo de control:

let x = if ... { ... } else { ... };
do_something_with(x)

Esto parece un punto realmente menor al calcular la asignación, pero un alcance claro es extremadamente importante para las pruebas relacionadas con la vida útil.

Si tuviéramos que aplicar un sistema de tipo Rust-style a Java, tendríamos problemas mucho más grandes que eso: los objetos Java no están anotados con vidas, por lo que tendríamos que tratarlos como &'static SomeClasso Arc<dyn SomeClass>. Eso debilitaría cualquier prueba resultante. Java tampoco tiene un concepto de inmutabilidad a nivel de tipo, por lo que no podemos distinguir entre &y &muttipos. Tendríamos que tratar cualquier objeto como una Celda o un Mutex, aunque esto podría asumir garantías más fuertes que las que Java realmente ofrece (cambiar un campo Java no es seguro a menos que esté sincronizado y sea volátil). Finalmente, Rust no tiene un concepto de herencia de implementación de estilo Java.

TL; DR: los sistemas de tipos son demostradores de teoremas. Pero están limitados por problemas de capacidad de decisión y problemas de rendimiento. No puede simplemente tomar un sistema de tipo y aplicarlo a un idioma diferente, ya que la sintaxis del idioma del destino puede no proporcionar la información necesaria y porque la semántica puede ser incompatible.

¿Qué tan seguro es seguro?

Sí, es casi posible escribir un verificador de este tipo: su programa solo tiene que devolver la constante INSEGURO. Estarás en lo cierto el 99% del tiempo

Porque incluso si ejecuta un programa Rust seguro, alguien puede desconectarlo durante su ejecución: por lo tanto, su programa podría detenerse incluso si, en teoría, no se supone que lo haga.

E incluso si su servidor se está ejecutando en una jaula de faraday en un búnker, un proceso vecino podría ejecutar una explotación de martillo de remo y hacer un pequeño giro en uno de su programa Rust supuestamente seguro.

Lo que intento decir es que su software se ejecutará en un entorno no determinista y muchos factores externos pueden influir en la ejecución.

Broma aparte, verificación automatizada

Ya hay analizadores de código estático que pueden detectar construcciones de programación riesgosas (variables no inicializadas, desbordamientos de búfer, etc.). Estos funcionan creando un gráfico de su programa y analizando la propagación de restricciones (tipos, rangos de valores, secuenciación).

Por cierto, este tipo de análisis también lo realizan algunos compiladores en aras de la optimización.

Ciertamente es posible ir un paso más allá, y también analizar la concurrencia y hacer deducciones sobre la propagación de restricciones a través de varios hilos, sincronización y condiciones de carrera. Sin embargo, muy rápidamente se toparía con el problema de la explosión combinatoria entre las rutas de ejecución y muchas incógnitas (E / S, programación del sistema operativo, entrada del usuario, comportamiento de programas externos, interrupciones, etc.) que diluirán las restricciones conocidas. mínimo y hace que sea muy difícil sacar conclusiones automatizadas útiles sobre código arbitrario.

Turing abordó esto en 1936 con su artículo sobre el problema de la detención. Uno de los resultados es que, solo que es imposible escribir un algoritmo que el 100% del tiempo pueda analizar el código y determinar correctamente si se detendrá o no, es imposible escribir un algoritmo que pueda el 100% del tiempo correctamente determine si el código tiene alguna propiedad en particular o no, incluyendo "seguridad" como quiera definirlo.

Sin embargo, el resultado de Turing no excluye la posibilidad de un programa que pueda 100% del tiempo (1) determinar absolutamente que el código es seguro, (2) determinar absolutamente que el código no es seguro o (3) levantar las manos antropomórficamente y decir "Diablos, no lo sé". El compilador de Rust, en general, está en esta categoría.

Si un programa es total (el nombre técnico de un programa que se garantiza que se detendrá), entonces es teóricamente posible probar cualquier propiedad arbitraria sobre el programa con suficientes recursos. Simplemente puede explorar cada estado potencial en el que podría ingresar el programa y verificar si alguno de ellos viola su propiedad. El lenguaje de verificación del modelo TLA + utiliza una variante de este enfoque, usando la teoría de conjuntos para verificar sus propiedades contra conjuntos de estados potenciales del programa, en lugar de calcular todos los estados.

Técnicamente, cualquier programa ejecutado en cualquier hardware físico práctico es total o un bucle comprobable debido al hecho de que solo tiene una cantidad limitada de almacenamiento disponible, por lo que solo hay un número finito de estados en los que puede estar la computadora. la computadora es en realidad una máquina de estado finito, no está completa, pero el espacio de estado es tan grande que es más fácil fingir que se está completando).

El problema con este enfoque es que tiene una complejidad exponencial a la cantidad de almacenamiento y tamaño del programa, lo que lo hace poco práctico para cualquier cosa que no sea el núcleo de los algoritmos e imposible de aplicar a bases de código significativas en su totalidad.

Entonces, la gran mayoría de la investigación se centra en las pruebas. La correspondencia de Curry-Howard afirma que una prueba de corrección y un sistema de tipos son la misma cosa, por lo que la mayor parte de la investigación práctica se denomina sistemas de tipos. Particularmente relevantes para esta discusión son Coq e Idriss, además de Rust que ya has mencionado. Coq aborda el problema de ingeniería subyacente desde la otra dirección. Tomando una prueba de la corrección del código arbitrario en el lenguaje Coq, puede generar código que ejecute el programa probado. Mientras tanto, Idriss utiliza un sistema de tipos dependiente para probar código arbitrario en un lenguaje puro como Haskell. Lo que estos dos lenguajes hacen es empujar los problemas difíciles de generar una prueba factible en el escritor, permitiendo que el verificador de tipos se centre en verificar la prueba. Verificar la prueba es un problema mucho más simple, pero esto hace que los idiomas sean mucho más difíciles de trabajar.

Ambos lenguajes se diseñaron específicamente para facilitar las pruebas, utilizando la pureza para controlar qué estado es relevante para qué partes del programa. Para muchos idiomas convencionales, el simple hecho de demostrar que una parte del estado es irrelevante para una prueba de una parte del programa puede ser un problema complejo debido a la naturaleza de los efectos secundarios y los valores mutables.