¿Seguridad de memoria basada en tipos sin administración manual de memoria o recolección de basura en tiempo de ejecución?

Digamos que queríamos un lenguaje de programación funcional y puro, como Haskell o Idris, que esté dirigido a la programación de sistemas sin recolección de basura y no tenga tiempo de ejecución (o al menos no más que los "tiempos de ejecución" de C y Rust). Algo que puede correr, más o menos, sobre metal desnudo.

¿Cuáles son algunas de las opciones para la seguridad de la memoria estática que no requieren la administración manual de la memoria o la recolección de basura en tiempo de ejecución, y cómo podría resolverse el problema utilizando el sistema de tipo de una funcionalidad pura similar a Haskell o Idris?

En términos generales, hay dos estrategias principales para la gestión segura de la memoria manual.

1. El primer enfoque es usar alguna lógica subestructural como la lógica lineal para controlar el uso de recursos. Esta idea ha flotado básicamente desde el inicio de la lógica lineal, y básicamente funciona en la observación de que al prohibir la regla estructural de contracción, cada variable se usa como máximo una vez, por lo que no hay alias. Como resultado, la diferencia entre la actualización in situ y la reasignación es invisible para el programa, por lo que puede implementar su idioma con la gestión manual de la memoria.

   Esto es lo que hace Rust (utiliza un sistema de tipo afín). Si está interesado en la teoría de los lenguajes al estilo Rust, uno de los mejores artículos para leer es L3: Un lenguaje lineal con ubicaciones de Ahmed et al . Como comentario aparte, el cálculo de LFPL que Damiano Mazza mencionó también es lineal, tiene un lenguaje completo derivado de él en el lenguaje RAML .

   Si está interesado en la verificación de estilo Idris, debe mirar el lenguaje ATS de Xi et al , que es un lenguaje de estilo Rust / L3 con soporte para verificación basado en tipos indexados de estilo Haskell, solo hecho irrelevante y lineal para proporcionar más control sobre el rendimiento.

   Un enfoque aún más agresivamente dependiente es el lenguaje F-star desarrollado en Microsoft Research, que es una teoría de tipo totalmente dependiente. Este lenguaje tiene una interfaz monádica con condiciones previas y posteriores en el espíritu de la teoría de tipos de Hoare de Nanevski et al (o incluso mis propios tipos integradores lineales y dependientes ), y tiene un subconjunto definido que se puede compilar en código C de bajo nivel - De hecho, ¡ya están enviando código criptográfico verificado como parte de Firefox!

   Para ser claros, ni F-star ni HTT son lenguajes de tipo lineal, pero el lenguaje índice para sus mónadas generalmente se basa en la lógica de separación de Reynold y O'Hearn , que es una lógica subestructural relacionada con la lógica lineal que ha tenido un gran éxito como El lenguaje de afirmación para las lógicas Hoare para programas de puntero.

2. El segundo enfoque es simplemente especificar qué ensamblaje (o cualquier IR de bajo nivel que desee) hace, y luego usar alguna forma de lógica lineal o de separación para razonar sobre su comportamiento en un asistente de prueba directamente. Esencialmente, puede usar el asistente de prueba o el lenguaje de tipo dependiente como un ensamblador de macros muy elegante que solo genera programas correctos.

   La lógica de separación de alto nivel de Jensen et al para código de bajo nivel es un ejemplo particularmente puro de esto: ¡construye lógica de separación para el ensamblaje x86! Sin embargo, hay muchos proyectos en este sentido, como Verified Software Toolchain en Princeton y el proyecto CertiKOS en Yale.

Todos estos enfoques se sentirán un poco como Rust, ya que el seguimiento de la propiedad al restringir el uso de variables es clave para todos ellos.

Los tipos lineales y la lógica de separación son excelentes, pero pueden requerir bastante esfuerzo del programador. Escribir una lista enlazada segura en Rust podría ser bastante difícil, por ejemplo.

Pero hay una alternativa que requiere mucho menos esfuerzo del programador, aunque con garantías menos estrictas. Un flujo de trabajo (bastante antiguo) es garantizar la seguridad de la memoria mediante el uso de (generalmente una pila de) regiones. Usando la inferencia de la región, un compilador puede decidir estáticamente en qué región debe ir una parte de los datos asignados, y desasignar la región cuando está fuera de alcance.

La inferencia de la región es demostrablemente segura (no puede desasignar la memoria accesible) y requiere una mínima interferencia del programador, pero no es "total" (es decir, todavía puede perder memoria, aunque definitivamente es mucho mejor que "no hacer nada"), por lo que generalmente se combina con GC en la práctica. losMLtonEl compilador de ML Kit usa regiones para eliminar la mayoría de las llamadas de GC, pero todavía tiene un GC porque de lo contrario aún perdería memoria. Según algunos de los primeros pioneros en las regiones, la inferencia regional no se inventó realmente para este propósito (creo que fue para la paralelización automática); pero resultó que también podría usarse para la gestión de la memoria.

Para un punto de partida, diría que vaya al documento "Implementación del cálculo λ de llamada por valor tipado usando una pila de regiones" por Mads Tofte y Jean-Pierre Talpin. Para más documentos sobre inferencia regional, busque otros documentos de M. Tofte y J.-P. Talpin, algunos de los trabajos de Pierre Jouvelot, así como la serie de documentos de Greg Morrisett, Mike Hicks y Dan Grossman sobre Cyclone.

Un esquema trivial para los sistemas "bare metal" es simplemente no permitir todas las asignaciones de memoria en tiempo de ejecución. Recuerde, incluso el malloc/freepar C requiere una biblioteca de tiempo de ejecución. Pero incluso cuando todos los objetos se definen en tiempo de compilación, se pueden definir de forma segura.

El principal problema aquí es la ficción de valores inmutables en lenguajes funcionales puros, que se crean mientras se ejecuta el programa. El hardware real (y ciertamente los sistemas de metal desnudo) dependen de RAM mutable, que tiene un suministro limitado. El tiempo de ejecución de una implementación de lenguaje funcional en la práctica asigna dinámicamente RAM a medida que se crean nuevos valores "inmutables", y la basura los recoge cuando el valor "inmutable" ya no es necesario.

Y para los problemas más interesantes, la vida útil de al menos algunos valores depende de la entrada de tiempo de ejecución (usuario), por lo que la vida útil no puede determinarse estáticamente. Pero incluso si la vida útil no depende de la entrada, puede ser altamente no trivial. Tome el programa simple para encontrar primos repetidamente simplemente verificando cada número en orden, verificando todos los primos hasta sqrt(N). Claramente esto necesita mantener los primos y puede reciclar la memoria utilizada para los no primos.