{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T14:33:20Z","timestamp":1754145200904,"version":"3.41.2"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"ISSTA","funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2022YFB4501903"],"award-info":[{"award-number":["2022YFB4501903"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2025,6,22]]},"abstract":"<jats:p>The Trusted Execution Environment (TEE), a security extension in modern processors, provides a secure runtime environment for sensitive code and data. Although TEEs are designed to protect applications and their private data, their large code bases often harbor vulnerabilities that could compromise data security. Even though some formal verification efforts have been directed toward the functionality and security of TEE standards and implementations, the verification of TEE correctness in concurrent scenarios remains insufficient. This paper introduces an enhancement for ensuring concurrency safety in TEEs, named Freesia, which is formally verified using concurrent separation logic. Through a thorough analysis of the GlobalPlatform TEE standards, Freesia addresses data race issues in the TEE communication interfaces and ensures consistency protection for shared memory between the client and the TEE. A prototype of Freesia is implemented in the open-source TEE platform, OP-TEE. Additionally, the concurrency correctness of Freesia is modeled and verified using the Iris concurrent separation logic framework. The effectiveness and efficiency of Freesia are further demonstrated through real-world case study and performance evaluations.<\/jats:p>","DOI":"10.1145\/3728967","type":"journal-article","created":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T10:52:56Z","timestamp":1750589576000},"page":"2045-2067","source":"Crossref","is-referenced-by-count":0,"title":["Freesia: Verifying Correctness of TEE Communication with Concurrent Separation Logic"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6606-1602","authenticated-orcid":false,"given":"Fanlang","family":"Zeng","sequence":"first","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0178-0171","authenticated-orcid":false,"given":"Rui","family":"Chang","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-7355-0893","authenticated-orcid":false,"given":"Hongjian","family":"Liu","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00061"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3652597"},{"key":"e_1_2_1_6_1","unstructured":"Victor Costan and Srinivas Devadas. 2016. Intel SGX Explained. Cryptology ePrint Archive. https:\/\/eprint.iacr.org\/2016\/086"},{"key":"e_1_2_1_7_1","unstructured":"CVE. 2017. A race condition may occur in Secure Driver resulting in potential buffer overflow vulnerability. https:\/\/www.cve.org\/CVERecord?id=CVE-2017-18647"},{"key":"e_1_2_1_8_1","unstructured":"CVE. 2018. NVIDIA TrustZone Software contains a TOCTOU issue in the DRM application. https:\/\/www.cve.org\/CVERecord?id=CVE-2017-6296"},{"key":"e_1_2_1_9_1","unstructured":"CVE. 2020. Qualcomm Snapdragon buffer overflow. https:\/\/www.cve.org\/CVERecord?id=CVE-2019-14041"},{"key":"e_1_2_1_10_1","unstructured":"CVE. 2020. Qualcomm Snapdragon TrustZone TOCTOU. https:\/\/www.cve.org\/CVERecord?id=CVE-2020-3619"},{"key":"e_1_2_1_11_1","unstructured":"CVE. 2023. OP-TEE double free in shdr_verify_signature. https:\/\/www.cve.org\/CVERecord?id=CVE-2023-41325"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF57540.2023.00021"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3407023.3407072"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586040"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_2_1_17_1","unstructured":"GlobalPlatform. 2010. TEE Client API Specification. https:\/\/globalplatform.org\/specs-library\/tee-client-api-specification"},{"key":"e_1_2_1_18_1","unstructured":"GlobalPlatform. 2021. TEE Internal Core API Specification Version 1.3.1. https:\/\/globalplatform.org\/specs-library\/tee-internal-core-api-specification"},{"volume-title":"White Paper: TEE System Architecture v1.3. https:\/\/globalplatform.org\/specs-library\/tee-system-architecture","year":"2022","key":"e_1_2_1_19_1","unstructured":"GlobalPlatform. 2022. White Paper: TEE System Architecture v1.3. https:\/\/globalplatform.org\/specs-library\/tee-system-architecture"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2024.3375311"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314595"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.22028\/D291-31946"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_27_1","unstructured":"David Kaplan Jeremy Powell and Tom Woller. 2021. AMD memory encryption. White Paper https:\/\/www.amd.com\/content\/dam\/amd\/en\/documents\/epyc-business-docs\/white-papers\/memory-encryption-white-paper.pdf"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560595"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3342195.3387532"},{"key":"e_1_2_1_31_1","volume-title":"Design and Verification of the ARM Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Li Xupeng","year":"2022","unstructured":"Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. 2022. Design and Verification of the ARM Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). 465\u2013484. https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/li"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632848"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2021.3133576"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CIC.2016.065"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591265"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813608"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134098"},{"key":"e_1_2_1_43_1","unstructured":"TEESEC Research. 2020. OP-TEE Trusted Applications vulnerable to memory corruption bugs. https:\/\/github.com\/teesec-research\/optee_examples\/tree\/vuln\/heap"},{"key":"e_1_2_1_44_1","unstructured":"TrustedFirmware. 2024. Open Portable Trusted Execution Environment. https:\/\/www.trustedfirmware.org\/projects\/op-tee"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00260"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3575735"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15181173"},{"key":"e_1_2_1_49_1","unstructured":"Fanlang Zeng Rui Chang and Hongjian Liu. 2025. Freesia Repository. https:\/\/github.com\/FLZeng\/Freesia"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3728967","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T16:47:33Z","timestamp":1752684453000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3728967"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,22]]},"references-count":49,"journal-issue":{"issue":"ISSTA","published-print":{"date-parts":[[2025,6,22]]}},"alternative-id":["10.1145\/3728967"],"URL":"https:\/\/doi.org\/10.1145\/3728967","relation":{},"ISSN":["2994-970X"],"issn-type":[{"type":"electronic","value":"2994-970X"}],"subject":[],"published":{"date-parts":[[2025,6,22]]}}}