Provably Secure Computation via Isolated Execution Environments
New capabilities of modern hardware technologies allow for the execution of arbitrary code within environments isolated from the rest of the system, and provide cryptographic mechanisms for reporting on these executions to remote parties. The rigorous security analysis of these protocols requires the development of scalable proof techniques for dealing with new forms of composition of cryptographic primitives arising in this setting.
The attestation guarantees of trusted hardware technologies can be used to bootstrap secure communications between participants and the hardware trust anchor. With a small and functionality-agnostic bootstrapping procedure, the bulk of the computational load can be moved to an untrusted party equipped with trusted hardware, an attractive feature for Cloud-based scenarios.
This presentation describes the first contributions in this direction, formalising the intuition of using hardware-based isolation and attestation guarantees to construct a new generation of efficient cryptographic protocols for searchable encryption, secure outsourcing of computation and secure multiparty computation. We will also briefly overview secure hardware solutions available on the market and discuss the extent to which they match our formal model of security for trusted hardware. Open challenges include designing solutions relying upon weaker hardware assumptions, and developing a heterogeneous, scalable and fault-tolerant attestation-based system.
12/02/2020 14:00
Computer Systems
Bernardo Portela graduated in Informatics Engineering from Universidade do Minho in 2013, and obtained its his Ph.D. in Computer Sciences under the MAPi doctoral programme (http://mapi.map.edu.pt/) in 2018. His recent research contributions are focused around developing security models and provably secure protocols, such as secure outsourcing of computations and general multiparty computation, to be deployed over IEEs. He is a member of NOVA-LINCS, where he plays an active role in the design of hardware-backed decentralized secure solutions in the context of P2020 project HADES. His research interests are the design and implementation of provably secure protocols, and the security analysis of privacy-protecting applications.
