Geração de descrições de computação para a cloud

Abstract

Nos últimos anos, a procura por soluções que tirem partido de um computação segura na cloud é um conceito em expansão e de grande interesse. A atratividade deste tema tem motivado a apresentação de inúmeras propostas de protocolos que tiram partido dessas características. Contudo, a grande maioria desses protocolos requerem que as funcionalidades a executar se apresentem descritos a um nível de abstração muito baixo, concretamente na forma de circuitos lógicos Booleanos. Obviamente que não é simples nem produtivo trabalhar a esse nível de abstração, pelo que surge uma necessidade de converter descrições de programas realizado numa linguagem de alto-nível nesses circuitos. Este projeto baseia-se no estudo dessa transformação, assegurando que a mesma é correta garantindo a preservação da semântica do código fonte. Para a realização desta transformação será proposto um compilador certificado, que terá a intenção de gerar descrições de circuitos Booleanos a partir de programas C. Para a produção destas descrições será tido em conta a sua eficiência de forma a melhorar a sua performance mantendo a fiabilidade do mesmo.

Over the last years, the demand of a secure computation in the cloud has been a growing concept in which people are taking interest in. The attractiveness of his theme has been driving the arise of protocols proposals that take advantages in cloud computing characteristics. However, to solve this need the majority of these solutions require that their features to be implemented in a very low-level of abstraction, more precisely in the format of logical Boolean circuits. Clearly it is not simple, neither work productive, to implement these specifications in such a low-level of abstraction. So there is a need to transform the description of the functionality implemented in a higher level language into those circuits. This project is based on the study of this transformation, ensuring its correction and the semantic preservation of the source code. In order to perform this transformation we propose a certified compiler which will be able to generate descriptions of Boolean circuits from a C programs with certain constraints. It will be also take into account the degree of eficiency of these descriptions, keeping its correctness.