{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:30Z","timestamp":1750308690476,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T00:00:00Z","timestamp":1557878400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,5,15]]},"DOI":"10.1145\/3317549.3323403","type":"proceedings-article","created":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T12:52:21Z","timestamp":1558097541000},"page":"45-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Advancing remote attestation via computer-aided formal verification of designs and synthesis of executables"],"prefix":"10.1145","author":[{"given":"Karim","family":"Eldefrawy","sequence":"first","affiliation":[{"name":"SRI International"}]},{"given":"Gene","family":"Tsudik","sequence":"additional","affiliation":[{"name":"UC Irvine"}]}],"member":"320","published-online":{"date-parts":[[2019,5,15]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"The coq proof assistant. https:\/\/coq.inria.fr\/.  The coq proof assistant. https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_2_1","unstructured":"Easycrypt: Computer-aided cryptographic proofs. https:\/\/www.easycrypt.info\/trac\/.  Easycrypt: Computer-aided cryptographic proofs. https:\/\/www.easycrypt.info\/trac\/."},{"key":"e_1_3_2_1_3_1","unstructured":"Pvs specification and verification system. http:\/\/pvs.csl.sri.com\/.  Pvs specification and verification system. http:\/\/pvs.csl.sri.com\/."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897937.2905020"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134017"},{"key":"e_1_3_2_1_6_1","unstructured":"Arm Ltd. Arm TrustZone 2018.  Arm Ltd. Arm TrustZone 2018."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744922"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3196494.3196526"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1655108.1655117"},{"key":"e_1_3_2_1_10_1","volume-title":"Norrathep Rattanavipanon, Michael Steiner, and Gene Tsudik. Formally verified hardware\/software co-design for remote attestation. CoRR, abs\/1811.00175","author":"Eldefrawy Karim","year":"2018","unstructured":"Karim Eldefrawy , Ivan Oliveira Nunes , Norrathep Rattanavipanon, Michael Steiner, and Gene Tsudik. Formally verified hardware\/software co-design for remote attestation. CoRR, abs\/1811.00175 , 2018 . Karim Eldefrawy, Ivan Oliveira Nunes, Norrathep Rattanavipanon, Michael Steiner, and Gene Tsudik. Formally verified hardware\/software co-design for remote attestation. CoRR, abs\/1811.00175, 2018."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098243.3098261"},{"key":"e_1_3_2_1_12_1","volume-title":"SMART: Secure and minimal architecture for (establishing dynamic) root of trust","author":"Eldefrawy Karim","year":"2012","unstructured":"Karim Eldefrawy , Gene Tsudik , Aur\u00e9lien Francillon , and Daniele Perito . SMART: Secure and minimal architecture for (establishing dynamic) root of trust . In NDSS. Internet Society , 2012 . Karim Eldefrawy, Gene Tsudik, Aur\u00e9lien Francillon, and Daniele Perito. SMART: Secure and minimal architecture for (establishing dynamic) root of trust. In NDSS. Internet Society, 2012."},{"key":"e_1_3_2_1_13_1","first-page":"1","volume-title":"Automation Test in Europe Conference Exhibition (DATE)","author":"Francillon A.","year":"2014","unstructured":"A. Francillon , Q. Nguyen , K. B. Rasmussen , and G. Tsudik . A minimalist approach to remote attestation. In 2014 Design , Automation Test in Europe Conference Exhibition (DATE) , pages 1 -- 6 , March 2014 . A. Francillon, Q. Nguyen, K. B. Rasmussen, and G. Tsudik. A minimalist approach to remote attestation. In 2014 Design, Automation Test in Europe Conference Exhibition (DATE), pages 1--6, March 2014."},{"key":"e_1_3_2_1_14_1","volume-title":"Securing the internet of things survey. https:\/\/www.sans.org\/reading-room\/whitepapers\/analyst\/securing-internet-things-survey-34785","author":"SANS Institute","year":"2014","unstructured":"SANS Institute . Securing the internet of things survey. https:\/\/www.sans.org\/reading-room\/whitepapers\/analyst\/securing-internet-things-survey-34785 , 2014 . SANS Institute. Securing the internet of things survey. https:\/\/www.sans.org\/reading-room\/whitepapers\/analyst\/securing-internet-things-survey-34785, 2014."},{"key":"e_1_3_2_1_15_1","unstructured":"Intel. Intel Software Guard Extensions (Intel SGX).  Intel. Intel Software Guard Extensions (Intel SGX)."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2592798.2592824"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.45"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2012.2189794"},{"key":"e_1_3_2_1_20_1","volume-title":"To kill a centrifuge a technical analysis of what Stuxnet's creators tried to achieve","author":"Langner Ralph","year":"2013","unstructured":"Ralph Langner . To kill a centrifuge a technical analysis of what Stuxnet's creators tried to achieve , 2013 . Ralph Langner. To kill a centrifuge a technical analysis of what Stuxnet's creators tried to achieve, 2013."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26096-9_7"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046711"},{"key":"e_1_3_2_1_23_1","volume-title":"The botnet that broke the internet isn't going away. https:\/\/www.wired.com\/2016\/12\/botnet-broke-internet-isnt-going-away\/","author":"Magazine Wired","year":"2016","unstructured":"Wired Magazine . The botnet that broke the internet isn't going away. https:\/\/www.wired.com\/2016\/12\/botnet-broke-internet-isnt-going-away\/ , 2016 . Wired Magazine. The botnet that broke the internet isn't going away. https:\/\/www.wired.com\/2016\/12\/botnet-broke-internet-isnt-going-away\/, 2016."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1888881.1888931"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1161289.1161306"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095809.1095812"},{"key":"e_1_3_2_1_27_1","unstructured":"IEEE Spectrum. The real story of Stuxnet. http:\/\/spectrum.ieee.org\/telecom\/security\/the-real-story-of-stuxnet 2013.  IEEE Spectrum. The real story of Stuxnet. http:\/\/spectrum.ieee.org\/telecom\/security\/the-real-story-of-stuxnet 2013."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/3199700.3199751"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"WiSec '19: 12th ACM Conference on Security and Privacy in Wireless and Mobile Networks","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control","SIGMOBILE ACM Special Interest Group on Mobility of Systems, Users, Data and Computing"],"location":"Miami Florida","acronym":"WiSec '19"},"container-title":["Proceedings of the 12th Conference on Security and Privacy in Wireless and Mobile Networks"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3317549.3323403","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3317549.3323403","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:01:18Z","timestamp":1750276878000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3317549.3323403"}},"subtitle":["opinion"],"short-title":[],"issued":{"date-parts":[[2019,5,15]]},"references-count":29,"alternative-id":["10.1145\/3317549.3323403","10.1145\/3317549"],"URL":"https:\/\/doi.org\/10.1145\/3317549.3323403","relation":{},"subject":[],"published":{"date-parts":[[2019,5,15]]},"assertion":[{"value":"2019-05-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}