Download Slides (PDF)

By Bernardo Portela, HASLab/INESC TEC & University of Minho.

Abstract. Modern trusted hardware technologies offer exciting new capabilities. They allow for the execution of arbitrary code within environments completely isolated from the rest of the system and provide cryptographic mechanisms for securely reporting on these executions to remote parties.

Rigorously proving security of protocols that rely on this type of hardware faces two obstacles. The first is to develop models appropriate for the induced trust assumptions (e.g., what is the correct notion of identity when the peer one wishes to communicate with is a specific instance of an outsourced program). The second is to develop scalable analysis methods, as the inherent stateful nature of the platforms precludes the application of existing modular analysis techniques that require high degrees of independence between the components.

The research effort towards the above issues led to a cryptographic formalization that will be presented in this talk. In particular, the talk will begin by describing the new instruction set architecture by Intel (SGX) alongside its basic usage, proposed protocols, and potential larger-scale applications. Afterwards, a formal treatment for isolated execution environments will be presented, consisting of an incremental approach with novel security models designed to tackle with the aforementioned definitional challenges.

Keywords. Secure computation; privacy-preserving systems; applied cryptography.

Coffee session: at 1:30PM-2PM, Sala de Estar, 4th Floor

Talks session: at 2PM-2:30PM, Auditório A2, 1st Floor