{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T07:24:21Z","timestamp":1763018661720,"version":"3.37.3"},"reference-count":57,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62132014"],"award-info":[{"award-number":["62132014"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Zhejiang Science and Technology Plan Project","award":["2022C01045"],"award-info":[{"award-number":["2022C01045"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Dependable and Secure Comput."],"published-print":{"date-parts":[[2024,11]]},"DOI":"10.1109\/tdsc.2024.3375311","type":"journal-article","created":{"date-parts":[[2024,3,11]],"date-time":"2024-03-11T18:26:03Z","timestamp":1710181563000},"page":"5341-5358","source":"Crossref","is-referenced-by-count":7,"title":["ProveriT: A Parameterized, Composable, and Verified Model of TEE Protection Profile"],"prefix":"10.1109","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-4527-2500","authenticated-orcid":false,"given":"Jilin","family":"Hu","sequence":"first","affiliation":[{"name":"School of Cyber Science and Technology, College of Computer Science and Technology, Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6606-1602","authenticated-orcid":false,"given":"Fanlang","family":"Zeng","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, College of Computer Science and Technology, Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2284-1383","authenticated-orcid":false,"given":"Yongwang","family":"Zhao","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, College of Computer Science and Technology, Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7896-1694","authenticated-orcid":false,"given":"Zhuoruo","family":"Zhang","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, College of Computer Science and Technology, Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-5120-1093","authenticated-orcid":false,"given":"Leping","family":"Zhang","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Beihang Univerisity, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-6524-1759","authenticated-orcid":false,"given":"Jianhong","family":"Zhao","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, College of Computer Science and Technology, Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0178-0171","authenticated-orcid":false,"given":"Rui","family":"Chang","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, College of Computer Science and Technology, Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1969-2591","authenticated-orcid":false,"given":"Kui","family":"Ren","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, College of Computer Science and Technology, Zhejiang University, Hangzhou, China"}]}],"member":"263","reference":[{"year":"2022","key":"ref1","article-title":"TEE system architecture v1.3 | GPD_SPE_009"},{"year":"2011","key":"ref2","article-title":"The trusted execution environment: Delivering enhanced security at a lower cost to the mobile market"},{"year":"2020","key":"ref3","article-title":"TEE protection profile v1.3 | GPD_SPE_021"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/CIC.2016.065"},{"issue":"86","key":"ref5","first-page":"1","article-title":"Intel SGX explained","volume":"2016","author":"Costan","year":"2016","journal-title":"Cryptol. ePrint Arch."},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3342195.3387532"},{"key":"ref7","first-page":"275","article-title":"Scalable memory protection in the PENGLAI enclave","volume-title":"Proc. 15th USENIX Symp. Operating Syst. Des. Implementation","author":"Feng"},{"year":"2021","key":"ref8","article-title":"Qualcomm trusted execution environment (TEE) v5.8 on Qualcomm Snapdragon\u2122 865 security target lite"},{"year":"2022","key":"ref9","article-title":"Riscure and trustonic achieve the first EAL 5+ TEE certificate compliant with GP TEE PP"},{"year":"2020","key":"ref10","article-title":"GlobalPlatform TEE certification report"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_15"},{"journal-title":"Common Criteria for Information Technology Security Evaluation","year":"2002","key":"ref12"},{"key":"ref13","first-page":"223","article-title":"Modeling the security objectives according to the common criteria methodology","volume-title":"Proc. Int. Conf. Secur. Manage.","author":"Bia\u0142as"},{"key":"ref14","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_26"},{"key":"ref17","first-page":"653","article-title":"CertiKOS: An extensible architecture for building certified concurrent OS kernels","volume-title":"Proc. 12th USENIX Symp. Operating Syst. Des. Implementation","author":"Gu"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_29"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2017.2672983"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446748"},{"key":"ref23","first-page":"1","article-title":"Push-button verification of file systems via crash refinement","volume-title":"Proc. 12th USENIX Conf. Operating Syst. Des. Implementation","author":"Sigurbjarnarson"},{"key":"ref24","first-page":"523","article-title":"BesFS: A POSIX filesystem for enclaves with a mechanized safety proof","volume-title":"Proc. 29th USENIX Secur. Symp.","author":"Shinde"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"ref27","first-page":"447","article-title":"Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning","volume-title":"Proc. 16th USENIX Symp. Operating Syst. Des. Implementation","author":"Chajed"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"ref29","first-page":"423","article-title":"GoJournal: A verified, concurrent, crash-safe journaling system","volume-title":"Proc. 15th USENIX Symp. Operating Syst. Des. Implementation","author":"Chajed"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813608"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2021.3133576"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560595"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134098"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.5555\/3241094.3241161"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_28"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87698-4_34"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04135-8_6"},{"key":"ref41","first-page":"395","article-title":"A bottom-up formal verification approach for common criteria certification: Application to JavaCard virtual machine","volume-title":"Proc. 11th Eur. Congr. Embedded Real Time Syst.","author":"Djoudi"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2245276.2232039"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39650-5_13"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/ICACT.2007.358355"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010277"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/52.566430"},{"key":"ref47","article-title":"Used formal methods","author":"Blasum","year":"2015","journal-title":"White Paper, EURO-MILS"},{"year":"2011","key":"ref48","article-title":"Writing security standards"},{"article-title":"Noninterference, transitivity, and channel-control security policies","year":"1992","author":"Rushby","key":"ref49"},{"year":"2023","key":"ref50","article-title":"Xiaomi HyperOS"},{"year":"2023","key":"ref51","article-title":"HyperOS introduction"},{"year":"2023","key":"ref52","article-title":"Open portable trusted execution environment"},{"year":"2023","key":"ref53","article-title":"Trusty TEE"},{"journal-title":"Guideline for the Development and Evaluation of Formal Security Policy Models in the Scope of ITSEC and Common Criteria","year":"2004","author":"Mantel","key":"ref54"},{"article-title":"Operating system protection profile","year":"2010","author":"M\u00fcller","key":"ref55"},{"year":"2022","key":"ref56","article-title":"Biometric mechanisms protection profle (BMPP)"},{"article-title":"Firewall protection profile","year":"2015","author":"Persson","key":"ref57"}],"container-title":["IEEE Transactions on Dependable and Secure Computing"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8858\/10750463\/10465667.pdf?arnumber=10465667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T23:54:02Z","timestamp":1732665242000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10465667\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11]]},"references-count":57,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/tdsc.2024.3375311","relation":{},"ISSN":["1545-5971","1941-0018","2160-9209"],"issn-type":[{"type":"print","value":"1545-5971"},{"type":"electronic","value":"1941-0018"},{"type":"electronic","value":"2160-9209"}],"subject":[],"published":{"date-parts":[[2024,11]]}}}