Validador de certificados de propiedades de seguridad de código fuente Java

Abstract

En el trabajo desarrollado en (Alba, 2011) se diseñó una metodología de certificación de propiedades de seguridad de software escrito en código fuente Java, que modela los programas Java –su semántica- como un sistema de transición de estados y realiza un análisis del programa para determinar la alcanzabilidad de estados considerados como “no seguros”; como resultado final, si el programa es seguro –i.e. no alcanza estados inseguros- la metodología de certificación entrega un certificado de seguridad en el que se incluye la demostración formal de que el programa es seguro, la cual es una inferencia lógica que corresponde a una computación en programación lógica en el lenguaje Maude; este certificado lo puede obtener un consumidor de código para así tener una evidencia de que el código que va a utilizar es seguro, pero actualmente los posibles usuarios del código no tienen cómo comprobar estos certificados, es decir que no pueden comprobar si el certificado es válido (corresponde con el programa, y con la semántica del lenguaje Java). La metodología de certificación se basa en la especificación de la semántica abstracta de Java en el lenguaje de programación declarativa y lógica Maude; el certificado es básicamente la traza de ejecución abstracta del programa Maude que hace la verificación de la no alcanzabilidad de estados inseguros mediante la interpretación del programa; esta traza es una inferencia lógica en lógica de reescritura y por esto puede utilizarse como demostración formal. El trabajo presente en este documento muestra el desarrollo del subsistema de validación de los certificados generados por herramientas que usen la metodología de certificación de propiedades de seguridad desarrollada en el trabajo mencionado anteriormente. Básicamente lo que busca el subsistema de validación es garantizar tres cosas; 1) Que los certificados de seguridad entregados a un consumidor de código corresponden con el código fuente del programa del que se dice que pertenecen; 2) Que los cambios de estado del programa suministrados en el certificado, se correspondan con la aplicación de las reglas de reescritura de la semántica abstracta; 3) Que en el certificado se evidencie que se aplicaron todas las reglas de reescritura de la semántica abstracta Java que se podían aplicar en la interpretación del código fuente. La semántica abstracta de Java además de reglas de reescritura contiene funciones cuya aplicación también significa cambios de estado en la interpretación del programa, pero el trabajo solo incluye la validación de la aplicación de las reglas. La metodología de certificación y validación se enmarca en el paradigma PCC (Proof-Carrying Code) que tiene como objetivo la ejecución segura de código móvil, la arquitectura que plantea esta técnica contempla elementos del lado del productor y del consumidor del código, en el marco de esta técnica, la metodología de certificación realiza las actividades de parte del “productor” y el subsistema de validación está concebido para apoyar la parte del “consumidor”