Verificação de software criptográfico de elevado desempenho

Abstract

A proteção dos dados que circulam na Internet deve ser alcançada, sempre que se justifique, ao nível da confidencialidade, integridade e autenticidade, com recurso a técnicas criptográficas. Contudo, está associado ao uso deste tipo de técnicas um custo computacional não negligenciável. Por isso, é necessário investir em optimizações recorrendo, por exemplo, a linguagens que se situam no nível do assembly.

O objectivo desta dissertação consiste em apresentar um método que permita a verificação estática de código criptográfico desenvolvido numa linguagem de baixo nível denominada qhasm. Este método consiste em traduzir código qhasm para código C, semanticamente equivalente, de forma a que todos os resultados da verificação sobre o código C traduzido possam ser transpostos para o código qhasm original.

The protection of data that circulates on the Internet should always be a matter of concern, and security properties such as confidentiality, integrity and authenticity should be ensured whenever needed using cryptographic techniques. However, there is a non negligible computational cost associated to the use of such techniques. Therefore it is necessary to invest in optimizations using, for instance, programming languages that operate at the assembly level. The aim of this dissertation is to present a method which allows static verification of cryptographic code developed in a low level language called qhasm. It consists in translating qhasm code into a semantically equivalent C code, in order to assure that all the verifications performed in C can be transposed back to the original qhasm code.