Soporte para ARM en un compilador verificado

Tesis (Lic. en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2022.

Guardado en:
Detalles Bibliográficos
Autor principal: Arranz Olmos, Santiago
Otros Autores: Pagano, Miguel María
Formato: bachelorThesis
Lenguaje:Español
Publicado: 2023
Materias:
Seguridad y privacidad
Jasmin
ARM Cortex M4
Lenguajes de programación
Formalización de hardware
Compiladores
Verificación
Criptografía
Security and privacy
Formal methods and theory of security
Acceso en línea:http://hdl.handle.net/11086/546410
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-546410
record_format dspace
spelling I10-R141-11086-5464102023-08-31T13:19:07Z Soporte para ARM en un compilador verificado Arranz Olmos, Santiago Pagano, Miguel María Seguridad y privacidad Jasmin ARM Cortex M4 Lenguajes de programación Formalización de hardware Compiladores Verificación Criptografía Security and privacy Formal methods and theory of security Tesis (Lic. en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2022. Fil: Arranz Olmos, Santiago. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Este trabajo es un estudio de un lenguaje de programación, llamado Jasmin, utilizado para desarrollar criptografía eficiente y confiable, así como una propuesta de una extensión a esta herramienta para agregar soporte para nuevas arquitecturas de hardware como ARM Cortex M4. Se estudia el problema de desarrollar software crítico con aplicaciones en seguridad, en particular criptografía, y se describen brevemente algunos de los fundamentos y herramientas utilizados para especificar e implementar estos sistemas. Luego, se describen el lenguaje de programación Jasmin, su compilador y la verificación formal de este último; y por último una generalización del compilador para adecuarlo a nuevos casos de interés. This work is a study on the Jasmin programming language, used to develop high-speed high-assurance cryptography, as well as a proposal for an extension to add support for new hardware architectures such as ARM Cortex M4. We study the problem of developing critical security software, in particular cryptography, as well as some of the theoretic foundations and tools used to specify and implement these systems. Then, we describe the Jasmin programming language, its compiler and the formal verification of the latter; finally, we report on a generalization proposed by us to adapt the compiler to new cases of interest. Fil: Arranz Olmos, Santiago. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2023-03-07T14:36:39Z 2023-03-07T14:36:39Z 2022-12 bachelorThesis http://hdl.handle.net/11086/546410 spa Atribución-CompartirIgual 4.0 Internacional http://creativecommons.org/licenses/by-sa/4.0/
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Español
topic Seguridad y privacidad
Jasmin
ARM Cortex M4
Lenguajes de programación
Formalización de hardware
Compiladores
Verificación
Criptografía
Security and privacy
Formal methods and theory of security
spellingShingle Seguridad y privacidad
Jasmin
ARM Cortex M4
Lenguajes de programación
Formalización de hardware
Compiladores
Verificación
Criptografía
Security and privacy
Formal methods and theory of security
Arranz Olmos, Santiago
Soporte para ARM en un compilador verificado
topic_facet Seguridad y privacidad
Jasmin
ARM Cortex M4
Lenguajes de programación
Formalización de hardware
Compiladores
Verificación
Criptografía
Security and privacy
Formal methods and theory of security
description Tesis (Lic. en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2022.
author2 Pagano, Miguel María
author_facet Pagano, Miguel María
Arranz Olmos, Santiago
format bachelorThesis
author Arranz Olmos, Santiago
author_sort Arranz Olmos, Santiago
title Soporte para ARM en un compilador verificado
title_short Soporte para ARM en un compilador verificado
title_full Soporte para ARM en un compilador verificado
title_fullStr Soporte para ARM en un compilador verificado
title_full_unstemmed Soporte para ARM en un compilador verificado
title_sort soporte para arm en un compilador verificado
publishDate 2023
url http://hdl.handle.net/11086/546410
work_keys_str_mv AT arranzolmossantiago soporteparaarmenuncompiladorverificado
_version_ 1782014198679601152

Ejemplares similares