Designing security protocols using Intel SGX

This project involves working together with the Nokia Bell Labs in Finland on verifying the security properties of applications that they build using TPM (Trusted Platform Module) or Intel SGX (Software Guard Extenssions).

The student will first learn about the specifications of these hardware security components and about tools and techniques for analyzing security/communication protocols like Proverif from INRIA, Murphi from the Stanford security lab, the AVISPA, or the FDR3 from Oxford. The goal is to model the new protocol as well as the hardware runtime, and then analyze security/privacy properties of the combination. A starting point will be the papers like:

  1. Intel SGX Explained  by Victor Costan and Srinivas Devadas
  2. Automated Verification of Dynamic Root of Trust Protocols

Ask for discussions with one of the supervisors, for more information or variations of the project. See also general concerns.

See a recent MSc thesis that one can build on.

Tags: security, TPM, Intel SGX, protocol, Proverif, AVISPA, modelling
Published July 30, 2019 4:31 PM - Last modified July 30, 2019 4:31 PM

Scope (credits)