Compilación y certificación de código mediante análisis estático de flujo de control y de datos

Abstract

En la última década el uso de las TIC ha irrumpido en forma explosiva en todas las áreas de actividad humana y han sido incorporadas a una, cada vez más, amplia gama de aplicaciones y artefactos. Paralelamente ha crecido de la misma forma el uso de Código Móvil; esto es, de código que es generado por un productor y usado por uno o numerosos consumidores. La distribución de software por Internet es el ejemplo más evidente, pero el uso de código móvil para la transmisión de actualizaciones o de nuevas versiones de código se extiende a la telefonía celular, a las tarjetas inteligentes y a todas las áreas donde pueda resultar importante la incorporación de nuevas funcionalidades a dispositivos controlados por software. La migración de código brinda una manera automática, de costo mínimo, para resolver la distribución o substitución de código para enormes cantidades de destinatarios. Sin embargo esta técnica también entraña graves riesgos, ya que el software migrado puede comprometer la seguridad de sus numerosos destinatarios, tanto por fallas de programación, como por maliciosas intenciones. La búsqueda de soluciones para este problema ha dado origen a activas líneas de investigación, dentro de las que se cuentan las referidas a la producción de Compiladores Certificantes, iniciadas con la introducción del Proof-Carrying Code (PCC) por G. Necula y P. Lee en 1996. Un Compilador Certificante genera, además del código ejecutable, una prueba o demostración de que dicho código no puede violar la política de seguridad preestablecida para su consumidor. Al consumidor le basta entonces someter exitosamente al código recibido a su prueba, para poder asegurar que su ejecución le resultara segura. Algunas líneas de investigación sobre compilación certificante se basan en frameworks lógicos y utilizan demostradores de teoremas, otras en modelar la seguridad mediante un sistema de tipos. Las primeras tienen la dificultad de que las pruebas son de alta complejidad, generalmente exponenciales, y muchas veces necesitan asistencia humana; mientras que las últimas, aún, sólo pueden aplicarse a políticas seguridad sumamente restringidas. Esta tesis se desarrolló dentro de un proyecto destinado a experimentar la construcción de compiladores certificantes basados en las técnicas de Análisis Estático de Flujo de Control y Datos, de difundido uso en la construcción de compiladores optimizantes. Se esperaba que este enfoque permitiera obtener soluciones lineales respecto de la longitud del programa fuente, tanto para la verificación de las pruebas obtenidas como para su generación. En dicho proyecto se definió un marco para el desarrollo de compiladores certificantes y sus correspondientes entornos de ejecución segura, al que se denominó Proof-Carrying Code based-on Static Analysis (PCC-SA). La definición, prototipación y evaluación de PCC-SA se dividió en dos tesis de maestría del INCO, Universidad de la República, Uruguay. Ambas tesis compartieron el relevamiento del Estado del Arte, el diseño general, la definición del lenguaje fuente y la evaluación global del framework, ientras que una se ocupó específicamente del diseño y la prototipación de las componentes del productor de código y la otra de las componentes del consumidor. La presente es la primera de dichas tesis (dirigida al entorno del productor). En ella se presenta a CCMini (Certifying Compiler for Mini), un compilador certificante para un subconjunto del lenguaje C, que garantiza que los programas que acepta no pueden leer variables no inicializadas y que en ellos no hay accesos a arreglos fuera de rango. Como lenguaje de código intermedio de CCMini se introducen los ´arboles sintácticos abstractos (ASA). Los ASA tiene una semántica clara que facilita la realización de los diversos análisis estáticos requeridos para generar la prueba de seguridad. Sobre el ASA del programa fuente, CCMini realiza el análisis estático, introduce anotaciones y verifica la seguridad del programa. Luego, si el programa es seguro, genera la información para el consumidor; información que consiste en el ASA anotado y en el esquema de la prueba. En los casos en que no se pueda determinar la seguridad de una computación especificada dentro del ASA (problema que no es decidible en general) CCMini anotar a una indicación de verificación en tiempo de ejecución. Con esta información el receptor correr a la prueba y si esta es exitosa generara código objeto y podrá ejecutarlo en forma segura. En la otra tesis del proyecto, que ya fue defendida, se mostraban varios casos de estudio que corroboraban la hipótesis de que tanto el proceso de generación de las pruebas como el de su verificación tenían un comportamiento lineal respecto de la longitud de los programas fuente. En esta tesis se demuestra que en el peor caso las técnicas usadas tienen un comportamiento cuadrático. Además se demuestra que la complejidad en casos reales (tanto del proceso de generación de la prueba, como el de verificación) es lineal respecto de la longitud del programa fuente. Esta demostración esta basada en la definición de una familia de programas C, a los que se llama linealmente acotables, y los cuales satisfacen algunas propiedades que se demostraron. Finalmente se inspecciona una conjunto de programas C de bibliotecas de uso universal, conjunto que comprende más de 4.000.000 de líneas de código y más de 90.000 funciones, convalidándose la hipótesis del comportamiento lineal de PCC-SA en la práctica ya que esta inspección permitió observar que estos programas pertenecen a la familia definida.