{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T03:41:08Z","timestamp":1743046868647,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572586"},{"type":"electronic","value":"9783031572593"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Trusted execution environments (TEEs) have emerged as a key technology in the cybersecurity domain. A TEE provides an isolated environment in which sensitive computations can be executed securely. Trusted applications running in TEEs are developed using standardized APIs that many hardware platforms for TEE adhere to. However, formal models tailored to standard TEE APIs are not well developed. In this paper, we present a formal specification of TEE APIs using Maude. We focus on Trusted Storage API and Cryptographic Operations API, which are foundational to mobile and IoT applications. The effectiveness of our approach is demonstrated through formal analysis of MQT-TZ, an open-source TEE application for IoT. Our formal analysis has revealed security vulnerabilities in the implementation of MQT-TZ, and we patch and confirm its integrity using model checking.<\/jats:p>","DOI":"10.1007\/978-3-031-57259-3_5","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:01:39Z","timestamp":1712322099000},"page":"101-121","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Specification of Trusted Execution Environment APIs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6171-9911","authenticated-orcid":false,"given":"Geunyeol","family":"Yu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-1199-7172","authenticated-orcid":false,"given":"Seunghyun","family":"Chae","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6430-5175","authenticated-orcid":false,"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3153-4662","authenticated-orcid":false,"given":"Sungkun","family":"Moon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Ayoade, G., Karande, V., Khan, L., Hamlen, K.: Decentralized IoT data management using blockchain and trusted execution environment. In: IEEE International Conference on Information Reuse and Integration (IRI). pp. 15\u201322. IEEE (2018). https:\/\/doi.org\/10.1109\/IRI.2018.00011","DOI":"10.1109\/IRI.2018.00011"},{"key":"5_CR2","unstructured":"Beniamini, G.: Trust issues: Exploiting TrustZone TEEs. Accessed: Aug 03, 2022 (online) (2017), https:\/\/googleprojectzero.blogspot.com\/2017\/07\/trust-issues-exploiting-trustzone-tees.html"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Bogdanas, D., Ro\u015fu, G.: K-Java: A complete semantics of Java. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). pp. 445\u2013456. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676982","DOI":"10.1145\/2676726.2676982"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All about Maude - A high-performance logical framework, Lecture Notes in Computer Science, vol. 4350. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Coppolino, L., D\u2019Antonio, S., Formicola, V., Mazzeo, G., Romano, L.: VISE: Combining Intel SGX and homomorphic encryption for cloud industrial control systems. IEEE Transactions on Computers 70(5), 711\u2013724 (2021). https:\/\/doi.org\/10.1109\/TC.2020.2995638","DOI":"10.1109\/TC.2020.2995638"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). pp. 533\u2013544. ACM (2012). https:\/\/doi.org\/10.1145\/2103656.2103719","DOI":"10.1145\/2103656.2103719"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Fitzek, A., Achleitner, F., Winter, J., Hein, D.: The ANDIX research OS \u2014 ARM TrustZone meets industrial control systems security. In: IEEE International Conference on Industrial Informatics (INDIN). pp. 88\u201393. IEEE (2015). https:\/\/doi.org\/10.1109\/INDIN.2015.7281715","DOI":"10.1109\/INDIN.2015.7281715"},{"key":"5_CR8","unstructured":"GlobalPlatform: TEE Internal Core API Specification v1.3.1 (2021), https:\/\/globalplatform.org\/specs-library\/tee-internal-core-api-specification\/"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: A complete formal semantics of the Ethereum virtual machine. In: IEEE Computer Security Foundations Symposium (CSF). pp. 204\u2013217. IEEE (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"5_CR10","unstructured":"Hua, Z., Gu, J., Xia, Y., Chen, H., Zang, B., Guan, H.: vTZ: virtualizing ARM TrustZone. In: USENIX Conference on Security Symposium (SEC). pp. 541\u2013556. USENIX Association (2017), https:\/\/dl.acm.org\/doi\/10.5555\/3241189.3241232"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Li, W., Xia, Y., Lu, L., Chen, H., Zang, B.: TEEv: Virtualizing trusted execution environments on mobile platforms. In: ACM SIGPLAN\/SIGOPS International Conference on Virtual Execution Environments (VEE). pp. 2\u201316. ACM (2019). https:\/\/doi.org\/10.1145\/3313808.3313810","DOI":"10.1145\/3313808.3313810"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Machiry, A., Gustafson, E., Spensky, C., Salls, C., Stephens, N., Wang, R., Bianchi, A., Choe, Y.R., Kruegel, C., Vigna, G.: BOOMERANG: Exploiting the semantic gap in trusted execution environments. In: Network and Distributed System Security Symposium (NDSS) (2017). http:\/\/dx.doi.org\/10.14722\/ndss.2017.23227","DOI":"10.14722\/ndss.2017.23227"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"M\u00e9n\u00e9trey, J., Pasin, M., Felber, P., Schiavoni, V.: WaTZ: A trusted WebAssembly runtime environment with remote attestation for TrustZone. In: IEEE International Conference on Distributed Computing Systems (ICDCS). pp. 1177\u20131189. IEEE (2022), https:\/\/doi.ieeecomputersociety.org\/10.1109\/ICDCS54860.2022.00116","DOI":"10.1109\/ICDCS54860.2022.00116"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73\u2013155 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Nguyen, H., Ivanov, R., Phan, L.T., Sokolsky, O., Weimer, J., Lee, I.: LogSafe: Secure and scalable data logger for IoT devices. In: IEEE\/ACM International Conference on Internet-of-Things Design and Implementation (IoTDI). pp. 141\u2013152. IEEE (2018). https:\/\/doi.org\/10.1109\/IoTDI.2018.00023","DOI":"10.1109\/IoTDI.2018.00023"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Ro\u015fu, G., \u015eerb\u0103nut\u0103, T.F.: An overview of the K semantic framework. The Journal of Logic and Algebraic Programming 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.03.012","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Sabt, M., Achemlal, M., Bouabdallah, A.: Trusted execution environment: what it is, and what it is not. In: IEEE International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom). pp. 57\u201364. IEEE (2015). https:\/\/doi.org\/10.1109\/Trustcom.2015.357","DOI":"10.1109\/Trustcom.2015.357"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Sardar, M.U., Faqeh, R., Fetzer, C.: Formal foundations for Intel SGX data center attestation primitives. In: International Conference on Formal Engineering Methods (ICFEM). Lecture Notes in Computer Science, vol. 12531, pp. 268\u2013283. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-63406-3_16","DOI":"10.1007\/978-3-030-63406-3_16"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Sardar, M.U., Musaev, S., Fetzer, C.: Demystifying attestation in Intel Trust Domain Extensions via formal verification. IEEE Access 9, 83067\u201383079 (2021). https:\/\/doi.org\/10.1109\/ACCESS.2021.3087421","DOI":"10.1109\/ACCESS.2021.3087421"},{"key":"5_CR20","unstructured":"Segarra, C., Delgado-Gonzalo, R., Schiavoni, V.: MQT-TZ fork of the open source Mosquitto MQTT broker leveraging ARM TrustZone, https:\/\/github.com\/mqttz\/mqttz"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Segarra, C., Delgado-Gonzalo, R., Schiavoni, V.: MQT-TZ: hardening IoT brokers using ARM TrustZone. In: International Symposium on Reliable Distributed Systems (SRDS). pp. 256\u2013265. IEEE (2020). https:\/\/doi.org\/10.1109\/SRDS51746.2020.00033","DOI":"10.1109\/SRDS51746.2020.00033"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Shepherd, C., Akram, R.N., Markantonakis, K.: Remote credential management with mutual attestation for trusted execution environments. In: IFIP International Conference on Information Security Theory and Practice (WISTP). Lecture Notes in Computer Science, vol. 11469, pp. 157\u2013173. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-20074-9_12","DOI":"10.1007\/978-3-030-20074-9_12"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Valadares, D.C.G., Sobrinho, \u00c1.A.d.C.C., Perkusich, A., Gorgonio, K.C.: Formal verification of a trusted execution environment-based architecture for IoT applications. IEEE Internet of Things Journal 8(23), 17199\u201317210 (2021). https:\/\/doi.org\/10.1109\/JIOT.2021.3077850","DOI":"10.1109\/JIOT.2021.3077850"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Wesemeyer, S., Newton, C.J., Treharne, H., Chen, L., Sasse, R., Whitefield, J.: Formal analysis and implementation of a TPM 2.0-based direct anonymous attestation scheme. In: ACM Asia Conference on Computer and Communications Security (ASIA CCS). pp. 784\u2013798. ACM (2020). https:\/\/doi.org\/10.1145\/3320269.3372197","DOI":"10.1145\/3320269.3372197"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Yu, G., Chae, S., Bae, K., Moon, S.: The artifact of TEE formal specification (2023). https:\/\/doi.org\/10.5281\/zenodo.10462106","DOI":"10.5281\/zenodo.10462106"},{"key":"5_CR26","unstructured":"Yu, G., Chae, S., Bae, K., Moon, S.: Supplementary material. (2023), https:\/\/github.com\/postechsv\/tee-formal-spec"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57259-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:02:59Z","timestamp":1712322179000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57259-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572586","9783031572593"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57259-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}