{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T23:20:14Z","timestamp":1768519214928,"version":"3.49.0"},"reference-count":26,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,12,14]],"date-time":"2025-12-14T00:00:00Z","timestamp":1765670400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,12,14]],"date-time":"2025-12-14T00:00:00Z","timestamp":1765670400000},"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":["U22B2023"],"award-info":[{"award-number":["U22B2023"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,12,14]]},"DOI":"10.1109\/icpads67057.2025.11323130","type":"proceedings-article","created":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T20:36:54Z","timestamp":1768423014000},"page":"1-8","source":"Crossref","is-referenced-by-count":0,"title":["Write-Once, Prove-Once: A Reusable Framework for Secure Boot Verification in Rocq"],"prefix":"10.1109","author":[{"given":"Minjie","family":"Fan","sequence":"first","affiliation":[{"name":"Institute of Artificial Intelligence, Xiamen University,Xiamen,China"}]},{"given":"Qiyu","family":"Wu","sequence":"additional","affiliation":[{"name":"LeapIO Tech Inc.,Beijing,China"}]},{"given":"Kuai","family":"Yu","sequence":"additional","affiliation":[{"name":"School of Software Technology, Zhejiang University.,Zhejiang,China"}]},{"given":"Gaosong","family":"Xu","sequence":"additional","affiliation":[{"name":"School of Informatics, Xiamen University,Xiamen,China"}]},{"given":"Xiaoyang","family":"Wang","sequence":"additional","affiliation":[{"name":"LeapIO Tech Inc.,Beijing,China"}]},{"given":"Jiwu","family":"Shu","sequence":"additional","affiliation":[{"name":"School of Informatics, Xiamen University,Xiamen,China"}]}],"member":"263","reference":[{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1997.601317"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0269-9"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0058022"},{"key":"ref8","volume-title":"Intel processor and intel core i3 and intel core 3 n-series datasheet","volume":"1 of 2"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3421473.3421477"},{"key":"ref12","volume-title":"Tpm 2.0 library specification, version 184","year":"2016"},{"key":"ref13","first-page":"653","article-title":"CertiKOS: An extensible architecture for building certified concurrent OS kernels","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Gu"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"ref16","volume-title":"Apple t2 security chip security overview","year":"2018"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"issue":"1","key":"ref18","first-page":"179","article-title":"Myreen, Michael Norrish, and Scott Owens","volume":"49","author":"Kumar","year":"2014","journal-title":"Cakeml: a verified implementation of ml. ACM SIGPLAN Notices"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"ref20","article-title":"Rob Spiger (CELA), and Stefan Thom. Cyber-resilient platforms overview","volume-title":"Technical Report MSR-T R-2017-40, Microsoft","author":"Marochko","year":"2017"},{"key":"ref21","volume-title":"Object-oriented software construction","volume":"2","author":"Meyer","year":"1997"},{"key":"ref22","volume-title":"Opentitan: Open source silicon root of trust.","year":"2019"},{"key":"ref23","first-page":"1","article-title":"Achilles heel in secure boot: Breaking RSA authentication and bitstream recovery from zynq-7000 SoC","volume-title":"18th USENIX WOOT Conference on Offensive Technologies (WOOT 24)","author":"Ravi"},{"key":"ref24","first-page":"223","article-title":"Design and implementation of a tcg-based integrity measurement architecture","volume-title":"USENIX Security symposium","volume":"13","author":"Sailer","year":"2004"},{"key":"ref25","volume-title":"Towards a verified first-stage bootloader in Coq","year":"2020"},{"key":"ref26","first-page":"1091","article-title":"{DICE*}: A formally verified implementation of {DICE} measured boot","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Tao","year":"2021"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.23919\/DATE58400.2024.10546576"}],"event":{"name":"2025 IEEE 31th International Conference on Parallel and Distributed Systems (ICPADS)","location":"Hefei, China","start":{"date-parts":[[2025,12,14]]},"end":{"date-parts":[[2025,12,18]]}},"container-title":["2025 IEEE 31th International Conference on Parallel and Distributed Systems (ICPADS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11322805\/11322871\/11323130.pdf?arnumber=11323130","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T07:09:43Z","timestamp":1768460983000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11323130\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12,14]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/icpads67057.2025.11323130","relation":{},"subject":[],"published":{"date-parts":[[2025,12,14]]}}}