Please use this identifier to cite or link to this item: http://hdl.handle.net/11182/104
Title: Validador de certificados de propiedades de seguridad de código fuente Java
Authors: Alba Castro, Mauricio Fernando
Grisales Badillo, Luis Fernando
Keywords: Programación lógica JAVA (Lenguaje de programación de computadores)
Programación orientada a objetos (Computadores)
Verificación de programas para computador
Semántica
Códigos de corrección (Teoría de la información)
Lenguajes formales
Issue Date: 2017
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”.
URI: http://hdl.handle.net/11182/104
Appears in Collections:Maestría en Gestión y Desarrollo de Proyectos de Software



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.