Please use this identifier to cite or link to this item: http://repositorio.autonoma.edu.co/handle/11182/685
Title: Validador de certificados de propiedades de seguridad de código fuente Java
Authors: Grisales Badillo, Luis Fernando
Advisor: Alba Castro, Mauricio Fernando
Keywords: Programación lógica JAVA-Lenguaje de programación
Programación orientada a objetos-Lenguaje de programación
Verificación de programas para computador
Semántica
Códigos de corrección-Teoría de la información
Keywords: JAVA logic programming-Programming language
Object Oriented Programming-Programming language
Verification of computer programs
Semantics
Correction codes-Information theory
Publisher: Universidad Autónoma de Manizales
Abstract(esp): 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”
Abstract(eng): In the work developed in (Alba, 2011) was designed a certification methodology for security properties of Java code, which is responsible to make a reachability analysis of states considered as "unsafe", as a final result the certification methodology delivers a security certificate that includes all tests done by the reachability analysis, A code consumer can get this certificate in order to have a evidence that the code is safe to use; the certification methodology is based on an abstract Java semantics specification written in Maude, Actually this methodology does not have any element that facilitates the certificates validation from the side of potential code users. This paper present the design of a validation methodology for certificates generated by tools that use the certification methodology for security properties developed in the work mentioned previously. The first validation methodology objective is to ensure that safety certificates delivered to a consumer of code correspond to the source code that says they belong to, the others objectives are to verify that rewrite steps provided in the certificate are correct and that the certificate has applied all possible rules to the Java source code, the validator design makes use of Java abstract semantics used by the certification methodology. The PCC technique (Proof-Carrying Code) tries to guarantee the secure execution of mobile code, the architecture of this technique take into account elements for both producer and consumer of the code, in this context the certification methodology performs the activities part of the "producer" in PCC, the validation methodology is designed to support the "consumer" activities in PCC.
URI: http://repositorio.autonoma.edu.co/handle/11182/685
Appears in Collections:Maestría en Gestión y Desarrollo de Proyectos de Software

Files in This Item:
File Description SizeFormat 
Validador_certificados_propiedades_seguridad_código_fuente_Java.pdfTexto completo2,01 MBAdobe PDFThumbnail
View/Open
Auto_Validador_certificados_propiedades_seguridad_código_fuente_Java.pdfAutorización932,06 kBAdobe PDFThumbnail
View/Open


This item is licensed under a Creative Commons License Creative Commons