{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:09:54Z","timestamp":1784239794963,"version":"3.55.0"},"reference-count":51,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T00:00:00Z","timestamp":1777852800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T00:00:00Z","timestamp":1777852800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2422053"],"award-info":[{"award-number":["2422053"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,5,4]]},"DOI":"10.1109\/host68814.2026.11604884","type":"proceedings-article","created":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T20:02:14Z","timestamp":1784145734000},"page":"162-173","source":"Crossref","is-referenced-by-count":0,"title":["Formal Firmware Verification of an At-Scale VM-level TEE Architecture"],"prefix":"10.1109","author":[{"given":"Sophia","family":"Zhang","sequence":"first","affiliation":[{"name":"Princeton Univ.,ECE Dept."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bo-Yuan","family":"Huang","sequence":"additional","affiliation":[{"name":"Intel Corp.,INT31"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sayak","family":"Ray","sequence":"additional","affiliation":[{"name":"Intel Corp.,INT31"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jason","family":"Fung","sequence":"additional","affiliation":[{"name":"Intel Corp.,INT31"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton Univ.,CS Dept."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[{"name":"Princeton Univ.,ECE Dept."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1536414.1536440"},{"key":"ref2","doi-asserted-by":"crossref","DOI":"10.23919\/DATE.2019.8715182","article-title":"Sanctorum: A lightweight security monitor for secure enclaves","volume-title":"Cryptology ePrint Archive, Paper 2019\/001","author":"Lebedev","year":"2019"},{"key":"ref3","article-title":"Intel Software Guard Extensions (Intel SGX)","volume-title":"Intel Corporation","year":"2025"},{"key":"ref4","volume-title":"ARM TrustZone","year":"2023"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3586040"},{"key":"ref6","author":"Micro","year":"2025","journal-title":"AMD Secure Encrypted Virtualization (SEV) - Overview"},{"key":"ref7","article-title":"Intel\u00ae Trust Domain Extensions (Intel TDX) - Overview","volume-title":"Intel Corporation","year":"2025"},{"key":"ref8","volume-title":"The Rocq Prover","year":"2025"},{"key":"ref9","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":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_10"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.3233\/sat190101"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_12"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3652597"},{"key":"ref19","volume-title":"Intel Trust Domain Extensions (Intel\u00ae TDX) Module Base Architecture Specification","year":"2025"},{"key":"ref20","volume-title":"Intel\u00ae Trust Domain Extensions (Intel\u00ae TDX) Module Architecture Application Binary Interface (ABI) Reference Specification","year":"2025"},{"key":"ref21","volume-title":"TDX","year":"2025"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-020-00344-2"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"ref25","volume-title":"Intel Trust Domain Extensions (TDX) Security Review","author":"Aktas","year":"2023"},{"key":"ref26","article-title":"Intel TDX Joint Security Review with Microsoft","volume-title":"Intel Corporation & Microsoft, Tech. Rep.","author":"Hania","year":"2024"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/HOST55342.2024.10545349"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2024.3443008"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134098"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813608"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC51365.2020.00023"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2974487"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC51365.2020.00023"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2024.3375311"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3087421"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2023.3346501"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/3623652.3623668"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_9"},{"key":"ref40","first-page":"465","article-title":"Design and verification of the arm confidential compute architecture","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Li"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695956"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2025.3541567"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_7"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19458-5_5"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693074"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_28"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1016\/s0065-2458(03)58003-2"},{"key":"ref50","first-page":"25","article-title":"Sat-based semiformal verification of hardware","author":"Agbaria","year":"2010","journal-title":"Formal Methods in Computer Aided Design"},{"key":"ref51","volume-title":"Jasper Formal Verification Platform","year":"2025"}],"event":{"name":"2026 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)","location":"Washington, DC, USA","start":{"date-parts":[[2026,5,4]]},"end":{"date-parts":[[2026,5,7]]}},"container-title":["2026 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11604575\/11604182\/11604884.pdf?arnumber=11604884","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T21:45:58Z","timestamp":1784238358000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11604884\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,4]]},"references-count":51,"URL":"https:\/\/doi.org\/10.1109\/host68814.2026.11604884","relation":{},"subject":[],"published":{"date-parts":[[2026,5,4]]}}}