{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,10]],"date-time":"2025-05-10T11:07:36Z","timestamp":1746875256905,"version":"3.37.3"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T00:00:00Z","timestamp":1701388800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T00:00:00Z","timestamp":1701388800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA8650-20-C-1719","FA8650-20-C-1719"],"award-info":[{"award-number":["FA8650-20-C-1719","FA8650-20-C-1719"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NSF","award":["2016624","2016624"],"award-info":[{"award-number":["2016624","2016624"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Hardw Syst Secur"],"published-print":{"date-parts":[[2023,12]]},"DOI":"10.1007\/s41635-023-00141-3","type":"journal-article","created":{"date-parts":[[2023,12,26]],"date-time":"2023-12-26T11:02:34Z","timestamp":1703588554000},"page":"147-164","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["EXERTv2: Exhaustive Integrity Analysis for Information Flow Security with FSM Integration"],"prefix":"10.1007","volume":"7","author":[{"given":"Jiaming","family":"Wu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Domenic","family":"Forte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,12,26]]},"reference":[{"issue":"1","key":"141_CR1","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1109\/MDT.2010.7","volume":"27","author":"M Tehranipoor","year":"2010","unstructured":"Tehranipoor M, Koushanfar F (2010) A survey of hardware Trojan taxonomy and detection. IEEE Des Test Comput 27(1):10\u201325","journal-title":"IEEE Des Test Comput"},{"key":"141_CR2","doi-asserted-by":"crossref","unstructured":"Zhang\u00a0X, Tehranipoor\u00a0M (2011) Case study: detecting hardware Trojans in third-party digital IP cores. In 2011 IEEE International Symposium on Hardware-Oriented Security and Trust, pp 67\u201370","DOI":"10.1109\/HST.2011.5954998"},{"key":"141_CR3","doi-asserted-by":"crossref","unstructured":"Kocher P,\u00a0Horn J,\u00a0Fogh A,\u00a0Genkin D,\u00a0Gruss D,\u00a0Haas W,\u00a0Hamburg M,\u00a0Lipp M,\u00a0Mangard S,\u00a0Prescher T,\u00a0Schwarz M,\u00a0Yarom Y (2018) Spectre attacks: exploiting speculative execution. In 2019 IEEE Symposium on Security and Privacy (SP), pp\u00a01\u201319","DOI":"10.1109\/SP.2019.00002"},{"key":"141_CR4","unstructured":"Lipp M,\u00a0Schwarz M,\u00a0Gruss D,\u00a0Prescher T,\u00a0Haas W,\u00a0Fogh A,\u00a0Horn J,\u00a0Mangard S,\u00a0Kocher P,\u00a0Genkin D,\u00a0Yarom Y,\u00a0Hamburg M (2018) Meltdown: reading kernel memory from user space. In 27th USENIX Security Symposium (USENIX Security 18), (Baltimore, MD), pp\u00a0973\u2013990. USENIX Association"},{"key":"141_CR5","doi-asserted-by":"crossref","unstructured":"Contreras GK,\u00a0Nahiyan A,\u00a0Bhunia S,\u00a0Forte D,\u00a0Tehranipoor M (2017) Security vulnerability analysis of design-for-test exploits for asset protection in SoCs. In 2017 22nd Asia and South Pacific Design Automation Conference (ASP-DAC), pp\u00a0617\u2013622","DOI":"10.1109\/ASPDAC.2017.7858392"},{"key":"141_CR6","doi-asserted-by":"crossref","unstructured":"Buhren R, Jacob H-N,\u00a0Krachenfels T, Seifert J-P (2021) One glitch to rule them all: fault injection attacks against AMD\u2019s secure encrypted virtualization. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, CCS \u201921, (New York, NY, USA), p\u00a02875-2889. Association for Computing Machinery","DOI":"10.1145\/3460120.3484779"},{"key":"141_CR7","doi-asserted-by":"crossref","unstructured":"Roy S, Millican SK, Agrawal VD (2021) Training neural network for machine intelligence in automatic test pattern generator. In 2021 34th International Conference on VLSI Design and 2021 20th International Conference on Embedded Systems (VLSID), pp\u00a0316\u2013321","DOI":"10.1109\/VLSID51830.2021.00059"},{"key":"141_CR8","doi-asserted-by":"crossref","unstructured":"Hu W,\u00a0Mu D,\u00a0Oberg J,\u00a0Mao B,\u00a0Tiwari M,\u00a0Sherwood T,\u00a0Kastner R (2014) Gate-level information flow tracking for security lattices. ACM Trans Des Autom Electron Syst 20","DOI":"10.1145\/2676548"},{"key":"141_CR9","doi-asserted-by":"publisher","first-page":"1691","DOI":"10.23919\/DATE.2017.7927266","volume":"2017","author":"A Ardeshiricham","year":"2017","unstructured":"Ardeshiricham A, Hu W, Marxen J, Kastner R (2017) Register transfer level information flow tracking for provably secure hardware design. In Design. Automation Test in Europe Conference Exhibition (DATE) 2017:1691\u20131696","journal-title":"Design Automation Test in Europe Conference Exhibition (DATE)"},{"key":"141_CR10","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1145\/2786763.2694372","volume":"43","author":"D Zhang","year":"2015","unstructured":"Zhang D, Wang Y, Suh GE, Myers AC (2015) A hardware design language for timing-sensitive information-flow security. SIGARCH Comput Archit News 43:503\u2013516","journal-title":"SIGARCH Comput Archit News"},{"key":"141_CR11","doi-asserted-by":"crossref","unstructured":"Cruz J,\u00a0Farahmandi F,\u00a0Ahmed A,\u00a0Mishra P (2018) Hardware trojan detection using ATPG and model checking. In 2018 31st International Conference on VLSI Design and 2018 17th International Conference on Embedded Systems (VLSID), pp\u00a091\u201396","DOI":"10.1109\/VLSID.2018.43"},{"key":"141_CR12","doi-asserted-by":"crossref","unstructured":"Nahiyan A,\u00a0Sadi M,\u00a0Vittal R,\u00a0Contreras G,\u00a0Forte D,\u00a0Tehranipoor M (2017) Hardware Trojan detection through information flow security verification. In 2017 IEEE International Test Conference (ITC), pp\u00a01\u201310","DOI":"10.1109\/TEST.2017.8242062"},{"key":"141_CR13","unstructured":"Jasper security path verification app (2023). https:\/\/www.cadence.com\/en_US\/home\/tools\/system-design-and-verification\/formal-and-static-verification\/jasper-gold-verification-platform\/"},{"key":"141_CR14","doi-asserted-by":"crossref","unstructured":"Goldstein L,\u00a0Thigpen E (1980) SCOAP: Sandia controllability\/observability analysis program. In 17th Design Automation Conference, pp\u00a0190\u2013196","DOI":"10.1145\/800139.804528"},{"key":"141_CR15","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1109\/TIFS.2016.2613842","volume":"12","author":"H Salmani","year":"2017","unstructured":"Salmani H (2017) COTD: reference-free hardware trojan detection and recovery based on controllability and observability in gate-level netlist. IEEE Transactions on Information Forensics and Security 12:338\u2013350","journal-title":"IEEE Transactions on Information Forensics and Security"},{"key":"141_CR16","doi-asserted-by":"crossref","unstructured":"Suh GE, Lee JW,\u00a0Zhang D,\u00a0Devadas S (2004) Secure program execution via dynamic information flow tracking. In Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XI, (New York, NY, USA), p\u00a085-96. Association for Computing Machinery","DOI":"10.1145\/1024393.1024404"},{"key":"141_CR17","doi-asserted-by":"crossref","unstructured":"Hu W,\u00a0Ardeshiricham A,\u00a0Kastner R (2021) Hardware information flow tracking. ACM Comput Surv 54","DOI":"10.1145\/3447867"},{"key":"141_CR18","unstructured":"Synopsys TetraMAX II Speeds Test Generation (2016). https:\/\/news.synopsys.com\/2016-07-12-Synopsys-TetraMAX-II-Speeds-Test-Generation-for-STMicroelectronics-SoC-Designs"},{"issue":"9","key":"141_CR19","doi-asserted-by":"publisher","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"P Stephan","year":"1996","unstructured":"Stephan P, Brayton R, Sangiovanni-Vincentelli A (1996) Combinational test generation using satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 15(9):1167\u20131176","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"141_CR20","doi-asserted-by":"crossref","unstructured":"Eggersgl\u00fc\u00df S,\u00a0Wille R,\u00a0Drechsler R (2013) Improved SAT-based ATPG: more constraints, better compaction. In 2013 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp\u00a085\u201390","DOI":"10.1109\/ICCAD.2013.6691102"},{"key":"141_CR21","doi-asserted-by":"crossref","unstructured":"Meade T,\u00a0Portillo J,\u00a0Zhang S,\u00a0Jin Y (2019) Neta: When IP fails, secrets leak. In Proceedings of the 24th Asia and South Pacific Design Automation Conference, ASPDAC \u201919, (New York, NY, USA), p\u00a090-95. Association for Computing Machinery","DOI":"10.1145\/3287624.3288739"},{"key":"141_CR22","doi-asserted-by":"crossref","unstructured":"Wang L-T (2009) Chapter 3 - design for testability. In Electronic Design Automation (L.-T. Wang, Y.-W. Chang, and K.-T.\u00a0T. Cheng, eds.), pp\u00a097\u2013172 Boston: Morgan Kaufmann","DOI":"10.1016\/B978-0-12-374364-0.50010-2"},{"key":"141_CR23","doi-asserted-by":"crossref","unstructured":"Reimann LM,\u00a0Hanel L,\u00a0Sisejkovic D,\u00a0Merchant F,\u00a0Leupers R (2021) QFlow: quantitative information flow for security-aware hardware design in Verilog. In 2021 IEEE 39th International Conference on Computer Design (ICCD), (Los Alamitos, CA, USA), pp\u00a0603\u2013607 IEEE Computer Society","DOI":"10.1109\/ICCD53106.2021.00097"},{"key":"141_CR24","doi-asserted-by":"crossref","unstructured":"Guo X, Dutta RG,\u00a0He J, Tehranipoor MM,\u00a0Jin Y (2019) QIF-Verilog: quantitative information-flow based hardware description languages for pre-silicon security assessment. In 2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp\u00a091\u2013100","DOI":"10.1109\/HST.2019.8740840"},{"key":"141_CR25","doi-asserted-by":"crossref","unstructured":"Nahiyan A,\u00a0Xiao K,\u00a0Yang K,\u00a0Jin Y,\u00a0Forte D,\u00a0Tehranipoor M (2016) AVFSM: a framework for identifying and mitigating vulnerabilities in FSMS. In 2016 53nd ACM\/EDAC\/IEEE Design Automation Conference (DAC), pp\u00a01\u20136","DOI":"10.1145\/2897937.2897992"},{"key":"141_CR26","unstructured":"The glucose SAT solver (2017). https:\/\/www.labri.fr\/perso\/lsimon\/glucose\/"},{"key":"141_CR27","unstructured":"Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification (2012). http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"141_CR28","unstructured":"Biere A,\u00a0Heljanko K,\u00a0Wieringa S (2011) AIGER 1.9 and beyond, Tech. Rep. 11\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria"},{"key":"141_CR29","unstructured":"pyAiger: a python library for manipulating sequential and combinatorial circuits (2018). https:\/\/github.com\/mvcisback\/py-aiger"},{"key":"141_CR30","doi-asserted-by":"crossref","unstructured":"Xin-Feng Z,\u00a0Jian-Dong W,\u00a0Bin L,\u00a0Jun-Wu Z,\u00a0Jun W (2009) Methods to tackle state explosion problem in model checking. 2009 Third International Symposium on Intelligent Information Technology Application\u00a02:329\u2013331","DOI":"10.1109\/IITA.2009.50"},{"key":"141_CR31","doi-asserted-by":"crossref","unstructured":"Salmani H,\u00a0Tehranipoor M,\u00a0Karri R (2013) On design vulnerability analysis and trust benchmarks development. In 2013 IEEE 31st International Conference on Computer Design (ICCD), pp\u00a0471\u2013474","DOI":"10.1109\/ICCD.2013.6657085"},{"key":"141_CR32","doi-asserted-by":"crossref","unstructured":"Rajendran J,\u00a0Vedula V,\u00a0Karri R (2015) Detecting malicious modifications of data in third-party intellectual property cores. In 2015 52nd ACM\/EDAC\/IEEE Design Automation Conference (DAC), pp\u00a01\u20136","DOI":"10.1145\/2744769.2744823"},{"key":"141_CR33","unstructured":"PIC16F84A data sheet (2010). https:\/\/ww1.microchip.com\/downloads\/en\/DeviceDoc\/35007b.pdf"},{"key":"141_CR34","doi-asserted-by":"crossref","unstructured":"Daemen J, Massolino PMC,\u00a0Mehrdad A,\u00a0Rotella Y (2020) The Subterranean 2.0 cipher suite. IACR Trans Symmetric Cryptol 2020:262-294","DOI":"10.46586\/tosc.v2020.iS1.262-294"},{"key":"141_CR35","unstructured":"Naito Y,\u00a0Matsui M,\u00a0Sugawara T,\u00a0Suzuki D (2019) SAEB: a lightweight blockcipher-based AEAD mode of operation. Cryptology ePrint Archive. Paper 2019\/700. https:\/\/eprint.iacr.org\/2019\/700"},{"key":"141_CR36","unstructured":"The RISC-V instruction set manual (2017). https:\/\/riscv.org\/wp-content\/uploads\/2017\/05\/riscv-privileged-v1.10.pdf"},{"key":"141_CR37","doi-asserted-by":"crossref","unstructured":"Wu J,\u00a0Fowze F,\u00a0Forte D (2022) EXERT: exhaustive integrity analysis for information flow security. In 2022 Asian Hardware Oriented Security and Trust Symposium (AsianHOST), pp\u00a01\u20136","DOI":"10.1109\/AsianHOST56390.2022.10022211"}],"container-title":["Journal of Hardware and Systems Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s41635-023-00141-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s41635-023-00141-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s41635-023-00141-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,20]],"date-time":"2024-02-20T07:03:58Z","timestamp":1708412638000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s41635-023-00141-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["141"],"URL":"https:\/\/doi.org\/10.1007\/s41635-023-00141-3","relation":{},"ISSN":["2509-3428","2509-3436"],"issn-type":[{"type":"print","value":"2509-3428"},{"type":"electronic","value":"2509-3436"}],"subject":[],"published":{"date-parts":[[2023,12]]},"assertion":[{"value":"31 July 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 December 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 December 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Statements and Declarations"}},{"value":"This research was partially supported by NSF under award # 2016624 and AFOSR under Award ID FA8650-20-C-1719.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Funding"}},{"value":"The authors declare no competing interests.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}},{"value":"Jiaming Wu and Domenic Forte wrote the whole manuscript. All authors reviewed the manuscript.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Author Contribution"}},{"value":"Not applicable","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Availability of Data and Materials"}},{"value":"Not applicable","order":6,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical Approval"}}]}}