Side channels; SGX; model checking

Recent advances of isolated execution technologies, especially the emergence of Intel Software Guard eXtension (SGX), revolutionize the model of computer security and empower programs with sensitive data and code to be shielded from untrusted operating systems. However, their security guarantees have not yet been thoroughly investigated against the notorious vector of information leakage side-channel attacks. It is conceivable that side-channel attacks with full control of the underlying operating system are more diverse, efficient and robust than those from unprivileged programs.