Análisis de flujo de control y código móvil seguro

Abstract

La interacción entre sistemas de software por medio de código móvil es un método poderoso que permite instalar y ejecutar código dinámicamente. De este modo, un servidor puede proveer medios flexibles de acceso a sus recursos y servicios internos. Pero este método poderoso presenta un riesgo grave para la seguridad del receptor, ya que el código móvil puede utilizarse también con fines maliciosos. Seguridad basada en el Lenguaje Fuente es un conjunto de técnicas, basadas en lógicas formales y sistemas de tipos, desarrolladas para garantizar y demostrar estáticamente que el software posee ciertas cualidades. En particular, esta técnica se concentra en el análisis de cualidades críticas, tales como seguridad de tipos y seguridad de memoria. Para que estas técnicas puedan ser aplicadas industrialmente es necesario llegar a una implementación eficiente, totalmente efectiva y que genere certificados (pruebas de seguridad) de tamaño reducido. En este trabajo se presenta evidencia que demuestra que la combinación de análisis estático de flujo de control y verificaciones dinámicas (siguiendo los lineamientos de Seguridad basada en el Lenguaje Fuente) puede constituir una aproximación que permita implementaciones eficientes que generen pruebas de tamaño lineal con respecto a la longitud del código de entrada.