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.