{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T05:24:45Z","timestamp":1755926685726,"version":"3.41.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2022,12,24]],"date-time":"2022-12-24T00:00:00Z","timestamp":1671840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF","award":["2019283"],"award-info":[{"award-number":["2019283"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2023,3,31]]},"abstract":"<jats:p>\n            Due to the globalization of Integrated Circuit supply chain, hardware Trojans and the attacks that can trigger them have become an important security issue. One type of hardware Trojans leverages the \u201cdon\u2019t care transitions\u201d in Finite-state Machines (FSMs) of hardware designs. In this article, we present a symbolic approach to detecting don\u2019t care transitions and the hidden Trojans. Our detection approach works at both register-transfer level (RTL) and gate level, does not require a golden design, and works in three stages. In the first stage, it explores the reachable states. In the second stage, it performs an approximate analysis to find the don\u2019t care transitions and any discrepancies in the register values or output lines due to don\u2019t care transitions. The second stage can be used for both predicting don\u2019t care triggered Trojans and for guiding don\u2019t care aware reachability analysis. In the third stage, it performs a state-space exploration from reachable states that have incoming don\u2019t care transitions to explore the Trojan payload and to find behavioral discrepancies with respect to what has been observed in the first stage. We also present a pruning technique based on the reachability of FSM states. We present a methodology that leverages both RTL and gate-level for soundness and efficiency. Specifically, we show that don\u2019t care transitions and Trojans that leverage them must be detected at the gate-level, i.e., after synthesis has been performed, for soundness. However, under specific conditions, Trojan payload exploration can be performed more efficiently at RTL. Additionally, the modular design of our approach also provides a fast Trojan prediction method even at the gate level when the reachable states of the FSM is known\n            <jats:italic>a priori<\/jats:italic>\n            . Evaluation of our approach on a set of benchmarks from OpenCores and TrustHub and using gate-level representation generated by two synthesis tools, YOSYS and Synopsis Design Compiler (SDC), shows that our approach is both efficient (up to 10\u00d7 speedup w.r.t. no pruning) and precise (0% false positives both at RTL and gate-level netlist) in detecting don\u2019t care transitions and the Trojans that leverage them. Additionally, the total analysis time can achieve up to 1.62\u00d7 (using YOSYS) and 1.92\u00d7 (using SDC) speedup when synthesis preserves the FSM structure, the foundry is trusted, and the Trojan detection is performed at RTL.\n          <\/jats:p>","DOI":"10.1145\/3558392","type":"journal-article","created":{"date-parts":[[2022,8,22]],"date-time":"2022-08-22T11:42:47Z","timestamp":1661168567000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["A Symbolic Approach to Detecting Hardware Trojans Triggered by Don\u2019t Care Transitions"],"prefix":"10.1145","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8393-0198","authenticated-orcid":false,"given":"Ruochen","family":"Dai","sequence":"first","affiliation":[{"name":"University of Florida, Gainesville, FL, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5542-2142","authenticated-orcid":false,"given":"Tuba","family":"Yavuz","sequence":"additional","affiliation":[{"name":"University of Florida, Gainesville, FL, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,12,24]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"209","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908), Richard Draves and Robbert van Renesse (Eds.). USENIX Association, 209\u2013224."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2638555"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2017.55"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/TEST.2015.7342387"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2747939"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.18"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10836-016-5632-y"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593147"},{"key":"e_1_3_2_13_2","unstructured":"LLVM Language Reference Manual. [n.d.]. Retrieved from https:\/\/llvm.org\/docs\/LangRef.html."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2011.2160627"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3287624.3288739"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2897937.2897992"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/HST.2011.5954999"},{"key":"e_1_3_2_18_2","unstructured":"OpenCores. [n.d.]. Retrieved from https:\/\/opencores.org\/."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744823"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2014.6865092"},{"key":"e_1_3_2_21_2","article-title":"State Machine Design Techniques for Verilog and VHDL","author":"Golson Steve","unstructured":"Steve Golson. [n.d.]. State Machine Design Techniques for Verilog and VHDL. Retrieved from https:\/\/trilobyte.com\/pdf\/golson_snug94.pdf.","journal-title":"Retrieved from https:\/\/trilobyte.com\/pdf\/golson_snug94.pdf"},{"key":"e_1_3_2_22_2","unstructured":"Synopsys. [n.d.]. Retrieved from https:\/\/www.synopsys.com\/implementation-and-signoff\/rtl-synthesis-test\/design-compiler-graphical.html."},{"key":"e_1_3_2_23_2","unstructured":"TrustHub. [n.d.]. Retrieved from https:\/\/www.trust-hub.org\/#\/home."},{"key":"e_1_3_2_24_2","unstructured":"VERILATOR. [n.d.]. Retrieved from https:\/\/www.veripool.org\/verilator\/."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516654"},{"key":"e_1_3_2_26_2","unstructured":"Wiki. [n.d.]. Retrieved from https:\/\/wiki.multimedia.cx\/index.php."},{"key":"e_1_3_2_27_2","unstructured":"Clifford Wolf. [n.d.]. Retrieved from http:\/\/www.clifford.at\/yosys\/about.html."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSM.2017.2763088"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2887268"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2016.2576444"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2422836"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00071"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/HST.2011.5954998"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/VTS.2013.6548922"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3558392","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3558392","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3558392","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:32Z","timestamp":1750182572000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3558392"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,24]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,3,31]]}},"alternative-id":["10.1145\/3558392"],"URL":"https:\/\/doi.org\/10.1145\/3558392","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2022,12,24]]},"assertion":[{"value":"2021-11-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-08-12","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-12-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}