Un Sistema de Tipos Físicos Nominales Dependientes para el Análisis Estático de Memoria en Código de Bajo Nivel

Abordamos el problema de verificar código sin prueba, es decir, demostrar automáticamente la seguridad de tipos (lo que implica en nuestro sistema de tipos la seguridad de memoria espacial) del código C de bajo nivel o del código de máquina resultante de su compilación sin modificación. Esto requiere un análisis estático preciso que obtenemos al tener un sistema de tipos que (i) es lo suficientemente expresivo para codificar modismos comunes de bajo nivel, como la aritmética de punteros, variantes discriminatorias mediante robo de bits en punteros alineados, almacenar el tamaño y la dirección base de un buffer en partes distintas de la memoria, o registros con miembros de arreglo flexible, entre otros; y (ii) puede ser integrado en un intérprete abstracto. Proponemos un nuevo sistema de tipos que cumple con estos criterios. La característica distintiva de este sistema de tipos es una organización nominal de regiones de memoria contiguas, que (i) permite anidamiento, concatenación, unión y compartir parámetros entre regiones; (ii) induce una retícula sobre conjuntos de direcciones a partir de las definiciones de tipos; y (iii) permite actualizaciones a celdas de memoria que cambian su tipo sin requerir controlar la aliasing. Proporcionamos un modelo semántico para nuestro sistema de tipos, que nos permite derivar reglas de comprobación de tipos sólidas mediante interpretación abstracta, y luego integrar estas reglas como un dominio abstracto en un análisis estático sensible al flujo estándar. Nuestros experimentos en varios benchmarks desafiantes muestran que la comprobación de tipos semántica utilizando este sistema de tipos expresivo generalmente tiene éxito en demostrar la seguridad de tipos y la seguridad de memoria espacial de programas en C y código de máquina sin modificación, utilizando solo prototipos de función proporcionados por el usuario.