{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T17:46:24Z","timestamp":1784310384660,"version":"3.55.0"},"reference-count":82,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"5","license":[{"start":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:00:00Z","timestamp":1567296000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:00:00Z","timestamp":1567296000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:00:00Z","timestamp":1567296000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100004040","name":"KU Leuven","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004040","id-type":"DOI","asserted-by":"publisher"}]},{"name":"imec"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Dependable and Secure Comput."],"published-print":{"date-parts":[[2019,9,1]]},"DOI":"10.1109\/tdsc.2019.2928541","type":"journal-article","created":{"date-parts":[[2019,10,9]],"date-time":"2019-10-09T19:45:03Z","timestamp":1570650303000},"page":"885-901","source":"Crossref","is-referenced-by-count":37,"title":["S The Security MicroVisor: A Formally-Verified Software-Based Security Architecture for the Internet of Things"],"prefix":"10.1109","volume":"16","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4963-5854","authenticated-orcid":false,"given":"Mahmoud","family":"Ammar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruno","family":"Crispo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3605-249X","authenticated-orcid":false,"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Danny","family":"Hughes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wilfried","family":"Daniels","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref73","doi-asserted-by":"crossref","DOI":"10.1007\/11601494_3","article-title":"Remote Software-Based Attestation for Wireless Sensors","author":"shaneck","year":"2005","journal-title":"Proc 2nd Eur Conf Secur Privacy Ad-Hoc Sensor Netw"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74477-1_97"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS.2007.31"},{"key":"ref70","first-page":"89","article-title":"Side effects are not sufficient to authenticate software","volume":"13","author":"shankar","year":"2014","journal-title":"Proc 13th Conf USENIX Secur Symp"},{"key":"ref76","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","article-title":"Scalable shape analysis for systems code","author":"yang","year":"2008","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321719"},{"key":"ref74","article-title":"Formally verified hardware\/software co-design for remote attestation","author":"eldefrawy","year":"2018","journal-title":"arXiv 1811 00175"},{"key":"ref39","article-title":"AVR Raven","year":"2007"},{"key":"ref75","first-page":"115","article-title":"Smallfoot: Modular automatic assertion checking with separation logic","author":"berdine","year":"2005","journal-title":"Proc Second Int l Symp Formal Methods for Components and Objects"},{"key":"ref38","article-title":"Zigduino","year":"2013"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_17"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_21"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.25"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2714576.2714618"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.36"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2523649.2523675"},{"key":"ref37","article-title":"AVR ATmega 1284p 8-bit microcontroller","year":"2009"},{"key":"ref36","article-title":"Intel 64 and IA-32 architectures software developer's manual - Instruction set reference A-Z","year":"2016"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.2004.1260985"},{"key":"ref34","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1145\/173668.168635","article-title":"Efficient software-based fault isolation","volume":"27","author":"wahbe","year":"1993","journal-title":"ACM SIGOPS Operating Syst Rev"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2017.2647955"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1145\/1067170.1067188"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1145\/1236360.1236404"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1997.601317"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1323293.1294294"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.32"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.17487\/RFC7554"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2009.5270348"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2008.09.005"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.17"},{"key":"ref67","article-title":"TPM main specification Level 2 Version 1.2","year":"2011"},{"key":"ref68","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/978-3-642-13869-0_2","article-title":"SBAP: Software-based attestation for peripherals","author":"li","year":"2010","journal-title":"Proceedings of the 3rd International Conference on Trust and Trustworthy Computing"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69170-9_25"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1658997.1659015"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455775"},{"key":"ref20","article-title":"Global IoT microcontroller (MCU) market analysis and research report by experts 2024","author":"herald","year":"2019"},{"key":"ref22","article-title":"IoT microcontroller market 2019 global analysis, segments, size, segmentation, share, demands, industry growth and recent trends by forecast to 2023","year":"2019"},{"key":"ref21","article-title":"IoT MCU market to reach USD 4.61 billion by 2026–Reports and data","year":"2019"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2988546"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","article-title":"VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java","author":"jacobs","year":"2011","journal-title":"Proc 3rd Int Conf NASA Formal Methods"},{"key":"ref26","article-title":"$\\mu$?PnP: Plug and Play Peripherals for the Internet of Things","author":"yang","year":"2015","journal-title":"Proc 10th Eur Conf Comput Syst"},{"key":"ref25","article-title":"source code of verified security MicroVisor.","author":"ammar","year":"0"},{"key":"ref50","article-title":"Sc22\/wg14. iso\/iec 9899: 2011","author":"jtc","year":"2011","journal-title":"Information technologyProgramming languagesC"},{"key":"ref51","article-title":"A minimalist approach to remote attestation","author":"francillon","year":"2014","journal-title":"Proc Conf Des Autom Test Eur"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046752"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1145\/2799647"},{"key":"ref57","first-page":"1","article-title":"Innovative technology for cpu based attestation and sealing","volume":"13","author":"anati","year":"2013","journal-title":"Proc 2nd Int Workshop Hardw Archit Support Secur Privacy"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1145\/2487726.2488368"},{"key":"ref55","article-title":"Trustzone: Integrated hardware and software security","author":"alves","year":"2004","journal-title":"White Paper"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2747946"},{"key":"ref53","article-title":"Announcing the first SHA1 collision","year":"2017"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/3176258.3176337"},{"key":"ref10","first-page":"479","article-title":"Sancus: Low-cost trustworthy extensible networked devices with a zero-software trusted computing base","author":"noorman","year":"2013","journal-title":"Proc 22nd USENIX Conf Secur"},{"key":"ref11","first-page":"1","article-title":"SMART: Secure and al architecture for (establishing dynamic) root of trust","author":"eldefrawy","year":"2012","journal-title":"Proc 19th Netw Distrib Syst Secur Symp"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2002.1134340"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2592798.2592824"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2004.1301329"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.17487\/rfc7228"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3154448.3154454"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.01.006"},{"key":"ref16","article-title":"8-bit AVR microcontrollers peripheral integration","year":"2018"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"ref17","article-title":"NXP Microcontrollers overview","year":"2017"},{"key":"ref18","article-title":"Arm cortex-m for beginners; an overview of the arm cortex-m processor family and comparison","author":"yiu","year":"2016","journal-title":"White Paper ARM Limited"},{"key":"ref19","article-title":"GLOBAL IOT MICROCONTROLLER (MCU) MARKET FORECAST 2018–2026","author":"research","year":"2018"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"ref4","article-title":"Target attack shows danger of remotely accessible HVAC systems","author":"vijayan","year":"2014"},{"key":"ref3","article-title":"Ransomware hijacks hotel smart keys to lock guests out of their rooms","author":"kumar","year":"2017"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.13"},{"key":"ref5","article-title":"Hackers broke into a casinos high-roller database through a thermometer in the lobby fish tank","author":"trends","year":"2018"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046711"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1095809.1095812","article-title":"Pioneer: : Verifying code integrity and enforcing untampered code execution on legacy systems","volume":"39","author":"seshadri","year":"2005","journal-title":"ACM SIGOPS Operating Syst Rev"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040327"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744922"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1561\/3300000013"},{"key":"ref48","author":"mecklenburg","year":"2004","journal-title":"Managing Projects with GNU Make The Power of GNU Make for Building Anything"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/502059.502042"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653711"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038687"},{"key":"ref43","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","article-title":"Z3: An efficient smt solver","author":"de moura","year":"2008","journal-title":"Proc Int Conf Tools Algorithms Construction Anal Syst"}],"container-title":["IEEE Transactions on Dependable and Secure Computing"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8858\/8821488\/08821489.pdf?arnumber=8821489","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,13]],"date-time":"2022-07-13T20:53:03Z","timestamp":1657745583000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8821489\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,1]]},"references-count":82,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.1109\/tdsc.2019.2928541","relation":{},"ISSN":["1545-5971","1941-0018","2160-9209"],"issn-type":[{"value":"1545-5971","type":"print"},{"value":"1941-0018","type":"electronic"},{"value":"2160-9209","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9,1]]}}}