Mohit Kumar Jangid, The Ohio State University; Guoxing Chen, Shanghai Jiao Tong University; Yinqian Zhang, Southern University of Science and Technology; Zhiqiang Lin, The Ohio State University
Trusted Execution Environments such as Intel SGX provide software applications with hardware support for preventing attacks from privileged software. However, these applications are still subject to rollback or replay attacks due to their lack of state continuity protection from the hardware. Therefore, maintaining state continuity has become a burden of software developers, which is not only challenging to implement but also difficult to validate. In this paper, we make the first attempt towards formally verifying the property of state continuity for SGX enclave programs by leveraging the symbolic verification tool, Tamarin Prover, to model SGX-specific program semantics and operations, and verify the property of state continuity with respect to monotonic counters, global variables, and sealed data, respectively. We apply this method to analyze these three types of state continuity issues exhibited in three open-source SGX applications. We show that our method can successfully identify the flaws that lead to failures of maintaining state continuity, and formally verify the corrected implementation with respect to the desired property. The discovered flaws have been reported to the developers and some have been addressed.
Open Access Media
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.
![](https://www.usenix.org/sites/all/modules/usenix/usenix_files/images/usenix-locked.png)
author = {Mohit Kumar Jangid and Guoxing Chen and Yinqian Zhang and Zhiqiang Lin},
title = {Towards Formal Verification of State Continuity for Enclave Programs},
booktitle = {30th USENIX Security Symposium (USENIX Security 21)},
year = {2021},
isbn = {978-1-939133-24-3},
pages = {573--590},
url = {https://www.usenix.org/conference/usenixsecurity21/presentation/jangid},
publisher = {USENIX Association},
month = aug
}