Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/37511
Título: | Cryptographic library support for a certified compiler |
Outro(s) título(s): | Bibliotecas de suporte criptográfico para um compilador certificado |
Autor(es): | Fernandes, Nuno Filipe Trovisco |
Orientador(es): | Almeida, José Bacelar |
Palavras-chave: | GMP LIP Certified compilers Cryptography Mathematical operations Big number libraries Cryptographic algorithms Proofs Gcc Compcert Coq AES SSE Processor extension Intel Compiladores certificados Criptografia Operações matemáticas Bibliotecas de grandes números Algoritmos criptográficos Provas Extensões do processador |
Data: | 4-Abr-2014 |
Resumo(s): | An essential component regarding the development of information systems is the compiler: a tool
responsible for translating high-level language code, like C or Java, into machine code. The issue is,
compilers are themselves big and complex programs, making them also vulnerable to failures that may
be propagated to the compiled programs. To overcome those risks research on “certified compilers” has
been made, and recently some proposals have appeared. That sort of compilers guarantees that the
compilation process runs as specified.
In this dissertation is studied the applicability of the certified compiler CompCert in cryptographic
software development. The first point being addressed was the use of support libraries, such as big
number libraries. As a matter of fact, such libraries are an essential requisite for the considered type of
application, therefore the study of different options for using these libraries, always considering the impact
in program’s performance and semantic preservation offered by the compiler.
The second point being addressed was the use of SIMD extensions available on recent processors.
Here the objective was to demonstrate how one could overcome the current CompCert’s limitations as to
discuss other solutions. Um componente essencial na produção de sistemas informáticos é o compilador: a ferramenta responsável por traduzir o código numa linguagem de alto nível como o C ou o Java em instruções do processador que serão efectivamente executadas. Mas os compiladores são eles próprios programas grandes e complexos, vulneráveis a falhas que se podem propagar de forma incontrolável por todos os programas por eles processados. Com o objectivo de ultrapassar esse risco surgiram recentemente as primeiras propostas de "compiladores certificados" onde se garante que o processo de compilação está conforme o especificado. Nesta dissertação é estudada a aplicabilidade do compilador certificado CompCert no desenvolvimento de software criptográfico. O primeiro aspecto abordado foi a utilização de bibliotecas de suporte, como as bibliotecas de números grandes. De facto, tais bibliotecas são um requisito essencial para tipo de aplicação considerado, estudando-se por isso diferentes alternativas para a utilização dessas bibliotecas, considerando quer o impacto na eficiência dos programas, quer as garantias de preservação semântica oferecidas pelo compilador. Um segundo aspecto abordado foi a utilização de extensões SIMD disponibilizadas pelos processadores mais recentes. Aqui o objectivo foi o de mostrar como é possível ultrapassar as limitações da versão actual do CompCert, assim como discutir soluções mais abrangentes ao problema. |
Tipo: | Dissertação de mestrado |
Descrição: | Dissertação de mestrado em Engenharia Informática |
URI: | https://hdl.handle.net/1822/37511 |
Acesso: | Acesso aberto |
Aparece nas coleções: | BUM - Dissertações de Mestrado |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
eeum_di_dissertacao_PG22787.pdf | 1,28 MB | Adobe PDF | Ver/Abrir |