Title: Formal verification of software-only mechanisms for live migration of SGX enclaves

Authors: Oualid Demigha; Nabil Haddad

Addresses: Department of Computer Science, Ecole Militaire Polytechnique, P.O. Box 17, 16111 Algiers, Algeria ' Department of Computer Science, Ecole Militaire Polytechnique, P.O. Box 17, 16111 Algiers, Algeria

Abstract: Live migration is not supported by current Intel® SGX implementations. So, software emulation is unavoidable to enable deployed hypervisors migrating live virtual machines running SGX enclaves in the cloud. However, copying the running state of an enclave requires read/write of enclave's memory from outside, which is impossible. Therefore, software-only mechanisms, as opposed to hardware extensions, are not transparent to the virtual machines, and need to deduce some hardware-defined metadata by emulation. Also, they need to synchronise enclaves' stop/resume between two remote platforms. In this paper, we formally verify the only solution proposed in the literature that uses such a mechanism, in which we identify a severe critical situation where the whole live migration process gets stuck. Moreover and due to a specification flaw, we determine a condition that leads to the violation of instance uniqueness of enclaves. That may induce vulnerabilities for fork and rollback attacks. To remedy to these design shortcomings, we propose some easy-to-implement solutions to remove deadlock situations and ensure state uniqueness at the expense of a longer downtime.

Keywords: trusted execution environment; trust cloud computing; Intel® SGX; hardware-assisted security; SPIN; PROMELA; model-checking; live migration; fork attack; rollback attack.

DOI: 10.1504/IJICS.2023.134965

International Journal of Information and Computer Security, 2023 Vol.22 No.2, pp.230 - 261

Received: 29 Nov 2021
Accepted: 17 May 2022
Published online: 22 Nov 2023 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article