{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,3]],"date-time":"2026-01-03T06:45:09Z","timestamp":1767422709881,"version":"3.28.0"},"reference-count":41,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.23919\/fmcad.2019.8894262","type":"proceedings-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T09:25:06Z","timestamp":1573637106000},"page":"110-119","source":"Crossref","is-referenced-by-count":6,"title":["Verification of Authenticated Firmware Loaders"],"prefix":"10.23919","author":[{"given":"Sujit Kumar","family":"Muduli","sequence":"first","affiliation":[]},{"given":"Pramod","family":"Subramanyan","sequence":"additional","affiliation":[]},{"given":"Sayak","family":"Ray","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_11"},{"key":"ref38","article-title":"UEFI Secure Boot in Modern Computer Security Solutions","author":"wilkins","year":"2013","journal-title":"UEFI Forum"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"ref32","first-page":"161","article-title":"Property directed self composition","author":"shemer","year":"2019","journal-title":"Computer Aided Verification"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"ref30","first-page":"143","author":"ruan","year":"2014","journal-title":"Boot with Integrity or Don’t Boot"},{"journal-title":"UCLID5 Verification and Synthesis System","year":"2019","key":"ref37"},{"journal-title":"Available at Design (MEMOCODE)","article-title":"UCLID5 Models of Authenticated Loaders","year":"2018","key":"ref36"},{"key":"ref35","first-page":"352","article-title":"Secure information flow as a safety problem","author":"terauchi","year":"2005","journal-title":"Proceedings of the International Static Analysis Symposium"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542266"},{"journal-title":"Intel trusted execution technology","year":"2019","key":"ref10"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2003.1212703"},{"journal-title":"Secure firmware update","year":"2006","author":"cottrell","key":"ref11"},{"key":"ref12","article-title":"When Firmware Modifications Attack: A Case Study of Embedded Exploitation","author":"cui","year":"2013","journal-title":"20th Annual Network and Distributed System Security Symposium NDSS 2013"},{"key":"ref13","article-title":"Z3: An Efficient SMT Solver","author":"de moura","year":"2008","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref14","first-page":"183","article-title":"Efficient E-Matching for SMT Solvers","author":"moura","year":"2007","journal-title":"Frank Pfenning editor Proceedings of the International Conference on Automated Deduction (CADE)"},{"journal-title":"Boogiepl A Typed Procedural Language for Checking Object-oriented Programs","year":"2005","author":"deline","key":"ref15"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1981.32"},{"key":"ref17","first-page":"200","article-title":"Automated hypersafety verification","author":"farzan","year":"2019","journal-title":"Computer Aided Verification 31st International Conference CAV 2019"},{"key":"ref18","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","article-title":"Algorithms for Model Checking HyperLTL and HyperCTL*","author":"finkbeiner","year":"2015","journal-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015)"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"journal-title":"Binary diff\/patch utility","year":"2003","key":"ref28"},{"key":"ref4","first-page":"364","article-title":"Boogie: A Modular Reusable Verifier for Object-Oriented Programs","author":"barnett","year":"2005","journal-title":"FMCO ’05 LNCS 4111"},{"key":"ref27","first-page":"855","article-title":"Fault-based attack of rsa authentication","author":"pellegrini","year":"2010","journal-title":"Proceedings of the Design Automation & Test in Europe Conference DATE"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1109\/JPROC.2005.862424","article-title":"The sorcerer’s apprentice guide to fault attacks","volume":"94","author":"bar-el","year":"2006","journal-title":"Proceedings of the IEEE"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1995.398927"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","article-title":"The NUXMV Symbolic Model Checker","author":"cavada","year":"2014","journal-title":"Proceedings of the International Conference on Computer Aided Verification"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1997.601317"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_28"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1133572.1133600"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/2678373.2665726","article-title":"Flipping Bits in Memory Without Accessing Them: An Experimental Study of DRAM Disturbance Errors","author":"kim","year":"2014","journal-title":"Proceeding of the 41st Annual International Symposium on Computer Architecuture ISCA ’14"},{"key":"ref21","first-page":"91:1","article-title":"Formal security verification of concurrent firmware in socs using instruction-level abstraction for hardware","author":"huang","year":"2018","journal-title":"Proc 55th Design Automation Conference DAC'2018"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00011"},{"journal-title":"Method for performing a trusted firmware\/BIOS update","year":"2005","author":"zimmer","key":"ref41"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/HST.2014.6855571"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1992-1103"},{"key":"ref25","first-page":"348","article-title":"Dafny: An automatic program verifier for functional correctness","author":"rustan","year":"2010","journal-title":"International Conference on Logic for Programming Artificial Intelligence and Reasoning"}],"event":{"name":"2019 Formal Methods in Computer Aided Design (FMCAD)","start":{"date-parts":[[2019,10,22]]},"location":"San Jose, CA, USA","end":{"date-parts":[[2019,10,25]]}},"container-title":["2019 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8891869\/8894241\/08894262.pdf?arnumber=8894262","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T21:05:04Z","timestamp":1722027904000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8894262\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":41,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2019.8894262","relation":{},"subject":[],"published":{"date-parts":[[2019,10]]}}}