Soporte para ARM en un compilador verificado | Trabajo Especial de la Licenciatura en Ciencias de la Computación

14 Dic. 2022 - Aula 27 - FAMAF | Google meet

Estudiante: Santiago ARRANZ OLMOS | Director: Miguel PAGANO

Sala de Meet: https://meet.google.com/jrn-sahg-rtw

Resumen: 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.