Código portador de prueba

El código con prueba de integridad ( PCC , por sus siglas en inglés) es un mecanismo de software que permite al sistema anfitrión verificar las propiedades de una aplicación mediante una prueba formal que acompaña al código ejecutable de la aplicación. El sistema anfitrión puede verificar rápidamente la validez de la prueba y comparar sus conclusiones con su propia política de seguridad para determinar si la aplicación se puede ejecutar de forma segura. Esto puede ser especialmente útil para garantizar la seguridad de la memoria (es decir, para prevenir problemas como desbordamientos de búfer ).

El código con prueba de autenticidad fue descrito originalmente en 1996 por George Necula y Peter Lee .

La publicación original sobre código de prueba en 1996 ^{[ 1 ]} utilizó filtros de paquetes como ejemplo: una aplicación en modo usuario entrega al núcleo una función escrita en código máquina que determina si una aplicación está interesada o no en procesar un paquete de red en particular. Dado que el filtro de paquetes se ejecuta en modo núcleo , podría comprometer la integridad del sistema si contiene código malicioso que escribe en las estructuras de datos del núcleo. Los enfoques tradicionales para este problema incluyen la interpretación de un lenguaje específico de dominio para el filtrado de paquetes, la inserción de comprobaciones en cada acceso a la memoria ( aislamiento de fallos de software ) y la escritura del filtro en un lenguaje de alto nivel que es compilado por el núcleo antes de su ejecución. Estos enfoques tienen desventajas de rendimiento para código que se ejecuta con tanta frecuencia como un filtro de paquetes, excepto el enfoque de compilación en el núcleo, que solo compila el código cuando se carga, no cada vez que se ejecuta.

Con el código portador de prueba, el núcleo publica una política de seguridad que especifica las propiedades que debe cumplir cualquier filtro de paquetes: por ejemplo, el filtro no accederá a la memoria fuera del paquete y su área de memoria temporal. Se utiliza un demostrador de teoremas para demostrar que el código máquina cumple con esta política. Los pasos de esta demostración se registran y se adjuntan al código máquina que se entrega al cargador de programas del núcleo. El cargador de programas puede entonces validar rápidamente la demostración, lo que le permite ejecutar el código máquina sin comprobaciones adicionales. Si un atacante modifica el código máquina o la demostración, el código portador de prueba resultante es inválido o inofensivo (sigue cumpliendo con la política de seguridad).

• Lenguaje ensamblador tipado
• Derivación del programa
• Verificación formal
• Filtro de paquetes de Berkeley

• George C. Necula y Peter Lee. Código con comprobación de integridad . Informe técnico CMU-CS-96-165, noviembre de 1996. (62 páginas)
• George C. Necula y Peter Lee. Agentes seguros y no confiables mediante código con prueba de autenticidad . Agentes móviles y seguridad, Giovanni Vigna (Ed.), Lecture Notes in Computer Science, Vol. 1419, Springer-Verlag, Berlín, ISBN 3-540-64792-9, 1998.
• George C. Necula. Compilación con demostraciones . Tesis doctoral, Escuela de Informática, Universidad Carnegie Mellon, septiembre de 1998.