{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T15:47:58Z","timestamp":1762876078305,"version":"3.41.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,5,7]],"date-time":"2019-05-07T00:00:00Z","timestamp":1557187200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Discovery Grants Programme"},{"name":"Strategic Networks Grants programme for Developing next generation Intelligent Vehicular Networks and Application"},{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,5,31]]},"abstract":"<jats:p>The Internet of Things (IoT) is playing an important role in different aspects of our lives. Smart grids, smart cars, and medical devices all incorporate IoT devices as key components. The ubiquity and criticality of these devices make them an attractive target for attackers. Therefore, we need techniques to analyze their security so that we can address their potential vulnerabilities. IoT devices, unlike remote servers, are user-facing and, therefore, an attacker may interact with them more extensively, e.g., via physical access. Existing techniques for analyzing security of IoT devices either rely on a pre-defined set of attacks and, therefore, have limited effect or do not consider the specific capabilities the attackers have against IoT devices.<\/jats:p>\n          <jats:p>Security analysis techniques may operate at the design-level, leveraging abstraction to avoid state-space explosion, or at the code-level for ensuring accuracy. In this article, we introduce two techniques, one at the design-level, and the other at the code-level, to analyze security of IoT devices, and compare their effectiveness. The former technique uses model checking, while the latter uses symbolic execution, to find attacks based on the attacker\u2019s capabilities. We evaluate our techniques on an open source smart meter. We find that our code-level analysis technique is able to find three times more attacks and complete the analysis in half the time, compared to the design-level analysis technique, with no false positives.<\/jats:p>","DOI":"10.1145\/3310353","type":"journal-article","created":{"date-parts":[[2019,5,8]],"date-time":"2019-05-08T14:11:11Z","timestamp":1557324671000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Design-Level and Code-Level Security Analysis of IoT Devices"],"prefix":"10.1145","volume":"18","author":[{"given":"Farid Molazem","family":"Tabrizi","sequence":"first","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karthik","family":"Pattabiraman","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,5,7]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2017. In-Stat and NDP Group Company. Retrieved from http:\/\/www.instat.com\/press.asp?ID&equals;33528sku&equals;IN1104731WH.  2017. In-Stat and NDP Group Company. Retrieved from http:\/\/www.instat.com\/press.asp?ID&equals;33528sku&equals;IN1104731WH."},{"key":"e_1_2_1_2_1","unstructured":"2017. Smart Energy Groups Home Page. Retrieved from http:\/\/smartenergygroups.com.  2017. Smart Energy Groups Home Page. Retrieved from http:\/\/smartenergygroups.com."},{"key":"e_1_2_1_3_1","unstructured":"2017. Acunetix Web Application Security Scanner. Retrieved from http:\/\/www.acunetix.com\/.  2017. Acunetix Web Application Security Scanner. Retrieved from http:\/\/www.acunetix.com\/."},{"key":"e_1_2_1_4_1","unstructured":"2017. Clang: A C Language Family Frontend for LLVM. Retrieved from https:\/\/clang.llvm.org\/.  2017. Clang: A C Language Family Frontend for LLVM. Retrieved from https:\/\/clang.llvm.org\/."},{"key":"e_1_2_1_5_1","unstructured":"2017. FBI: Smart Meter Hacks Likely to Spread. Retrieved from http:\/\/krebsonsecurity.com\/2012\/04\/fbi-smart-meter-hacks-likely-to-spread\/.  2017. FBI: Smart Meter Hacks Likely to Spread. Retrieved from http:\/\/krebsonsecurity.com\/2012\/04\/fbi-smart-meter-hacks-likely-to-spread\/."},{"key":"e_1_2_1_6_1","unstructured":"2017. Hacking Humans. Retrieved from http:\/\/blog.kaspersky.com\/hacking-humans\/.  2017. Hacking Humans. Retrieved from http:\/\/blog.kaspersky.com\/hacking-humans\/."},{"key":"e_1_2_1_7_1","unstructured":"2017. Hacking Medical Devices for Fun and Insulin: Breaking the Human. Retrieved from https:\/\/media.blackhat.com\/bh-us-11\/Radcliffe\/BH_US_11_Radcliffe_Hacking_Medical_Devices_WP.pdf.  2017. Hacking Medical Devices for Fun and Insulin: Breaking the Human. Retrieved from https:\/\/media.blackhat.com\/bh-us-11\/Radcliffe\/BH_US_11_Radcliffe_Hacking_Medical_Devices_WP.pdf."},{"key":"e_1_2_1_8_1","unstructured":"2017. HP WebInspect. Retrieved from http:\/\/www8.hp.com\/us\/en\/software-solutions\/webinspect-dynamic-analysis-dast\/index.html.  2017. HP WebInspect. Retrieved from http:\/\/www8.hp.com\/us\/en\/software-solutions\/webinspect-dynamic-analysis-dast\/index.html."},{"key":"e_1_2_1_9_1","unstructured":"2017. IBM Security AppScan. Retrieved from http:\/\/www-03.ibm.com\/software\/products\/en\/appscan.  2017. IBM Security AppScan. Retrieved from http:\/\/www-03.ibm.com\/software\/products\/en\/appscan."},{"volume-title":"Retrieved","year":"2017","key":"e_1_2_1_10_1","unstructured":"2017. Arduino home page . Retrieved July 31, 2017 from http:\/\/www.arduino.cc. 2017. Arduino home page. Retrieved July 31, 2017 from http:\/\/www.arduino.cc."},{"volume-title":"Smart Meter Design Document. Retrieved","year":"2017","key":"e_1_2_1_11_1","unstructured":"2017. UK Department of Energy , Smart Meter Design Document. Retrieved July 31, 2017 from https:\/\/www.ofgem.gov.uk\/ofgem-publications\/63541\/smart-metering-prospectus.pdf. 2017. UK Department of Energy, Smart Meter Design Document. Retrieved July 31, 2017 from https:\/\/www.ofgem.gov.uk\/ofgem-publications\/63541\/smart-metering-prospectus.pdf."},{"key":"e_1_2_1_12_1","unstructured":"2017. National Vulnerability Database. Retrieved from https:\/\/nvd.nist.gov\/.  2017. National Vulnerability Database. Retrieved from https:\/\/nvd.nist.gov\/."},{"key":"e_1_2_1_13_1","unstructured":"2017. SymbolicLua. Retrieved from https:\/\/github.com\/kohyatoh\/symboliclua.  2017. SymbolicLua. Retrieved from https:\/\/github.com\/kohyatoh\/symboliclua."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102165"},{"key":"e_1_2_1_15_1","first-page":"37","article-title":"Software defect reduction top 10 list","volume":"426","author":"Boehm Barry","year":"2005","unstructured":"Barry Boehm and Victor R. Basili . 2005 . Software defect reduction top 10 list . Foundations of Empirical Software Engineering: The Legacy of Victor R. Basili 426 (2005), 37 . Barry Boehm and Victor R. Basili. 2005. Software defect reduction top 10 list. Foundations of Empirical Software Engineering: The Legacy of Victor R. Basili 426 (2005), 37.","journal-title":"Basili"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1080\/10157891.1988.10472819"},{"volume-title":"Smart Hacking for Privacy. In 28th Chaos Communication Congress","author":"Brinkhaus S.","key":"e_1_2_1_17_1","unstructured":"S. Brinkhaus , D. Carluccio , U. Greveler , D. B. Justus , and C. Wegener . 2011 . Smart Hacking for Privacy. In 28th Chaos Communication Congress . Berlin, Germany. S. Brinkhaus, D. Carluccio, U. Greveler, D. B. Justus, and C. Wegener. 2011. Smart Hacking for Privacy. In 28th Chaos Communication Congress. Berlin, Germany."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the International Infrastructure Survivability Workshop. Citeseer.","author":"Byres Eric J.","year":"2004","unstructured":"Eric J. Byres , Matthew Franz , and Darrin Miller . 2004 . The use of attack trees in assessing vulnerabilities in SCADA systems . In Proceedings of the International Infrastructure Survivability Workshop. Citeseer. Eric J. Byres, Matthew Franz, and Darrin Miller. 2004. The use of attack trees in assessing vulnerabilities in SCADA systems. In Proceedings of the International Infrastructure Survivability Workshop. Citeseer."},{"key":"e_1_2_1_19_1","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , Dawson R. Engler , 2008 . KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs . In OSDI , Vol. 8. 209 -- 224 . Cristian Cadar, Daniel Dunbar, Dawson R. Engler, et al. 2008. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, Vol. 8. 209--224.","journal-title":"OSDI"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2005.36"},{"volume-title":"All About Maude-a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic","author":"Clavel Manuel","key":"e_1_2_1_21_1","unstructured":"Manuel Clavel , Francisco Dur\u00e1n , Steven Eker , Patrick Lincoln , Narciso Mart\u00ed-Oliet , Jos\u00e9 Meseguer , and Carolyn Talcott . 2007. All About Maude-a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic . Springer-Verlag . Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn Talcott. 2007. All About Maude-a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag."},{"key":"e_1_2_1_22_1","volume-title":"USENIX Security Symposium. 463--478","author":"Davidson Drew","year":"2013","unstructured":"Drew Davidson , Benjamin Moench , Thomas Ristenpart , and Somesh Jha . 2013 . FIE on firmware: Finding vulnerabilities in embedded systems using symbolic execution . In USENIX Security Symposium. 463--478 . Drew Davidson, Benjamin Moench, Thomas Ristenpart, and Somesh Jha. 2013. FIE on firmware: Finding vulnerabilities in embedded systems using symbolic execution. In USENIX Security Symposium. 463--478."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891831"},{"key":"e_1_2_1_25_1","unstructured":"K. Fehrenbacher. 2010. Smart Meter Worm Could Spread Like a Virus. Retrieved from http:\/\/earth2tech.com\/2009\/07\/31\/smart-meter-worm-could-spread-like-a-virus\/.  K. Fehrenbacher. 2010. Smart Meter Worm Could Spread Like a Virus. Retrieved from http:\/\/earth2tech.com\/2009\/07\/31\/smart-meter-worm-could-spread-like-a-virus\/."},{"volume-title":"Advances in Digital","author":"Fernandez Eduardo","key":"e_1_2_1_26_1","unstructured":"Eduardo Fernandez , Juan Pelaez , and Maria Larrondo-Petrie . 2007. Attack patterns: A new forensic and design tool . In Advances in Digital Forensics III. Springer , 345--357. Eduardo Fernandez, Juan Pelaez, and Maria Larrondo-Petrie. 2007. Attack patterns: A new forensic and design tool. In Advances in Digital Forensics III. Springer, 345--357."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1082983.1083211"},{"volume-title":"The Science of Programming","author":"Gries David","key":"e_1_2_1_28_1","unstructured":"David Gries . 2012. The Science of Programming . Springer Science 8 Business Media. David Gries. 2012. The Science of Programming. Springer Science 8 Business Media."},{"key":"e_1_2_1_29_1","unstructured":"itron. 2018. Retrieved from https:\/\/www.itron.com\/.  itron. 2018. Retrieved from https:\/\/www.itron.com\/."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/794201.795177"},{"key":"e_1_2_1_31_1","volume-title":"Smart Metering Implementation Programm. Retrieved","author":"Department of Energy and Climate","year":"2017","unstructured":"Department of Energy and Climate Change and the Office of Gas and Electricity Markets. 2011 . Smart Metering Implementation Programm. Retrieved July 31, 2017 from http:\/\/www.ofgem.gov.uk\/e-serve\/sm\/Documentation\/Documents1\/Design20Requirements.pdf. Department of Energy and Climate Change and the Office of Gas and Electricity Markets. 2011. Smart Metering Implementation Programm. Retrieved July 31, 2017 from http:\/\/www.ofgem.gov.uk\/e-serve\/sm\/Documentation\/Documents1\/Design20Requirements.pdf."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2010.49"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00450-014-0290-8"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.34"},{"key":"e_1_2_1_35_1","unstructured":"landis. 2018. Retrieved from https:\/\/www.landisgyr.com\/.  landis. 2018. Retrieved from https:\/\/www.landisgyr.com\/."},{"key":"e_1_2_1_36_1","volume-title":"Retrieved","author":"Lewson N.","year":"2010","unstructured":"N. Lewson . 2010 . Smart Meter Crypto Flaw Worse Than Thought . Retrieved July 31, 2017 from http:\/\/rdist.root.org\/2010\/01\/11\/smart-meter-crypto-flaw-worse-than-thought. N. Lewson. 2010. Smart Meter Crypto Flaw Worse Than Thought. Retrieved July 31, 2017 from http:\/\/rdist.root.org\/2010\/01\/11\/smart-meter-crypto-flaw-worse-than-thought."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2013.2284438"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00040-4"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2008.13"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/11734727_17"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2009.76"},{"volume-title":"Critical Information Infrastructures Security","author":"McLaughlin Stephen","key":"e_1_2_1_42_1","unstructured":"Stephen McLaughlin , Dmitry Podkuiko , and Patrick McDaniel . 2010. Energy theft in the advanced metering infrastructure . In Critical Information Infrastructures Security . Springer , 176--187. Stephen McLaughlin, Dmitry Podkuiko, and Patrick McDaniel. 2010. Energy theft in the advanced metering infrastructure. In Critical Information Infrastructures Security. Springer, 176--187."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1920261.1920277"},{"key":"e_1_2_1_44_1","volume-title":"SOFSEM","volume":"11","author":"Miculan Marino","year":"2011","unstructured":"Marino Miculan and Caterina Urban . 2011 . Formal analysis of Facebook connect single sign-on authentication protocol . In SOFSEM , Vol. 11 . Citeseer, 22--28. Marino Miculan and Caterina Urban. 2011. Formal analysis of Facebook connect single sign-on authentication protocol. In SOFSEM, Vol. 11. Citeseer, 22--28."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/96267.96279"},{"key":"e_1_2_1_46_1","volume-title":"Dependable Systems and Networks Workshops (DSN-W).","author":"Molazem Farid","year":"2012","unstructured":"Farid Molazem and Karthik Pattabiraman . 2012 . A model for security analysis of smart meters. In WRAITS , Dependable Systems and Networks Workshops (DSN-W). Farid Molazem and Karthik Pattabiraman. 2012. A model for security analysis of smart meters. In WRAITS, Dependable Systems and Networks Workshops (DSN-W)."},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the 2016 Annual Computer Security Applications Conference (ACSAC\u201916)","author":"Molazem Farid","year":"2016","unstructured":"Farid Molazem and Karthik Pattabiraman . 2016 . Formal security analysis of smart embedded systems . In Proceedings of the 2016 Annual Computer Security Applications Conference (ACSAC\u201916) . IEEE Computer Society. Farid Molazem and Karthik Pattabiraman. 2016. Formal security analysis of smart embedded systems. In Proceedings of the 2016 Annual Computer Security Applications Conference (ACSAC\u201916). IEEE Computer Society."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSE.2009.206"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2006.72"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 12th Network and Distributed Systems Security Symposium. 3--4.","author":"Newsome James","year":"2005","unstructured":"James Newsome and Dawn Song . 2005 . Dynamic taint analysis: Automatic detection, analysis, and signature generation of exploit attacks on commodity software . In Proceedings of the 12th Network and Distributed Systems Security Symposium. 3--4. James Newsome and Dawn Song. 2005. Dynamic taint analysis: Automatic detection, analysis, and signature generation of exploit attacks on commodity software. In Proceedings of the 12th Network and Distributed Systems Security Symposium. 3--4."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3052973.3053038"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/PESMG.2013.6672638"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/11555827_14"},{"key":"e_1_2_1_54_1","volume-title":"2010 IEEE International Carnahan Conference on Security Technology (ICCST). IEEE, 276--285","author":"Ray Partha Datta","year":"2010","unstructured":"Partha Datta Ray , Rajgopal Harnoor , and Mariana Hentea . 2010 . Smart power grid security: A unified risk management approach . In 2010 IEEE International Carnahan Conference on Security Technology (ICCST). IEEE, 276--285 . Partha Datta Ray, Rajgopal Harnoor, and Mariana Hentea. 2010. Smart power grid security: A unified risk management approach. In 2010 IEEE International Carnahan Conference on Security Technology (ICCST). IEEE, 276--285."},{"key":"e_1_2_1_55_1","volume-title":"Attack trees. Dr. Dobb\u2019s Journal 24, 12","author":"Schneier Bruce","year":"1999","unstructured":"Bruce Schneier . 1999. Attack trees. Dr. Dobb\u2019s Journal 24, 12 ( 1999 ), 21--29. Bruce Schneier. 1999. Attack trees. Dr. Dobb\u2019s Journal 24, 12 (1999), 21--29."},{"volume-title":"Proceeding of the 2002 IEEE Symposium on Security and Privacy. IEEE, 273--284","author":"Sheyner Oleg","key":"e_1_2_1_56_1","unstructured":"Oleg Sheyner , Joshua Haines , Somesh Jha , Richard Lippmann , and Jeannette M. Wing . 2002. Automated generation and analysis of attack graphs . In Proceeding of the 2002 IEEE Symposium on Security and Privacy. IEEE, 273--284 . Oleg Sheyner, Joshua Haines, Somesh Jha, Richard Lippmann, and Jeannette M. Wing. 2002. Automated generation and analysis of attack graphs. In Proceeding of the 2002 IEEE Symposium on Security and Privacy. IEEE, 273--284."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2165269"},{"key":"e_1_2_1_58_1","unstructured":"Smart meter testing framework Termineter. 2017. Retrieved from https:\/\/code.google.com\/p\/termineter\/.  Smart meter testing framework Termineter. 2017. Retrieved from https:\/\/code.google.com\/p\/termineter\/."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.diin.2008.05.012"},{"key":"e_1_2_1_60_1","volume-title":"Security pros question deployment of smart meters. Threat Level: Privacy, Crime and Security Online (March","author":"Zetter K.","year":"2010","unstructured":"K. Zetter . 2010. Security pros question deployment of smart meters. Threat Level: Privacy, Crime and Security Online (March 2010 ). K. Zetter. 2010. Security pros question deployment of smart meters. Threat Level: Privacy, Crime and Security Online (March 2010)."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISGT.2012.6175770"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310353","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3310353","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:37Z","timestamp":1750204417000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310353"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,7]]},"references-count":61,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,5,31]]}},"alternative-id":["10.1145\/3310353"],"URL":"https:\/\/doi.org\/10.1145\/3310353","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2019,5,7]]},"assertion":[{"value":"2017-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-05-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}