Soporte para ARM en un compilador verificado

Abstract

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.