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.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | bachelorThesis |
| Language: | spa |
| Published: |
2023
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/546410 |
| _version_ | 1801212834985541632 |
|---|---|
| author | Arranz Olmos, Santiago |
| author2 | Pagano, Miguel María |
| author_facet | Pagano, Miguel María Arranz Olmos, Santiago |
| author_sort | Arranz Olmos, Santiago |
| collection | Repositorio Digital Universitario |
| 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. |
| format | bachelorThesis |
| id | rdu-unc.546410 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2023 |
| record_format | dspace |
| spelling | rdu-unc.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/ |
| 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 |
| title | 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_short | Soporte para ARM en un compilador verificado |
| title_sort | soporte para arm en un compilador verificado |
| 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 |
| url | http://hdl.handle.net/11086/546410 |
| work_keys_str_mv | AT arranzolmossantiago soporteparaarmenuncompiladorverificado |