{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T15:32:46Z","timestamp":1780673566867,"version":"3.54.1"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,1,19]],"date-time":"2023-01-19T00:00:00Z","timestamp":1674086400000},"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":["J. Emerg. Technol. Comput. Syst."],"published-print":{"date-parts":[[2023,1,31]]},"abstract":"<jats:p>System-on-Chip (SoC) security is vital in designing trustworthy systems. Detecting and fixing a vulnerability in the early stages is easier and cost-effective. Assertion-based verification is widely used for functional validation of Register-Transfer Level (RTL) designs. Assertions can improve the controllability and observability that can lead to faster error detection and localization. Although assertions are widely used for functional validation of RTL models, there is limited effort in applying assertions to detect SoC security vulnerabilities. Specifically, a fundamental challenge in SoC security and trust validation is how to develop high-quality security assertions. In this article, we perform automated vulnerability analysis of RTL models to generate security assertions for six classes of vulnerabilities. Experimental results show that the generated security assertions can detect a wide variety of vulnerabilities. Our automated framework can drastically reduce the overall security validation effort compared to the manual development of security assertions. Automated generation of security assertions will enable assertion-based verification to be one of the most promising pre-silicon security sign-off solutions.<\/jats:p>","DOI":"10.1145\/3565801","type":"journal-article","created":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T11:53:31Z","timestamp":1669118011000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Automated Generation of Security Assertions for RTL Models"],"prefix":"10.1145","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0761-6169","authenticated-orcid":false,"given":"Hasini","family":"Witharana","sequence":"first","affiliation":[{"name":"University of Florida"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8347-5065","authenticated-orcid":false,"given":"Aruna","family":"Jayasena","sequence":"additional","affiliation":[{"name":"University of Florida"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2928-0275","authenticated-orcid":false,"given":"Andrew","family":"Whigham","sequence":"additional","affiliation":[{"name":"University of Florida"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3653-6221","authenticated-orcid":false,"given":"Prabhat","family":"Mishra","sequence":"additional","affiliation":[{"name":"University of Florida"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,19]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"Harry Foster. 2020. Wilson Research Group Functional Verification Study. GitHub. Retrieved November 28 2022 from https:\/\/uobdv.github.io\/Design-Verification\/WilsonResearchGroupFunctionalVerificationStudy\/2020-WRGFV-Study\/2020-WrG-FV-Study-Webinar-Oct13.pdf."},{"issue":"1","key":"e_1_3_1_3_2","first-page":"21","article-title":"System-on-chip platform security assurance: Architecture and validation","volume":"106","author":"Ray Sandip","year":"2017","unstructured":"Sandip Ray, Eric Peeters, Mark M. Tehranipoor, and Swarup Bhunia. 2017. System-on-chip platform security assurance: Architecture and validation. Proceedings of the IEEE 106, 1 (2017), 21\u201337.","journal-title":"Proceedings of the IEEE"},{"key":"e_1_3_1_4_2","article-title":"System-on-chip security assertions","author":"Lyu Yangdi","year":"2020","unstructured":"Yangdi Lyu and Prabhat Mishra. 2020. System-on-chip security assertions. arXiv preprint arXiv:2001.06719 (2020).","journal-title":"arXiv preprint arXiv:2001.06719"},{"key":"e_1_3_1_5_2","first-page":"626","volume-title":"Proceedings of DATE","author":"Vasudevan Shobha","year":"2010","unstructured":"Shobha Vasudevan, David Sheridan, Sanjay Patel, David Tcheng, Bill Tuohy, and Daniel Johnson. 2010. Goldmine: Automatic assertion generation using data mining and static analysis. In Proceedings of DATE. IEEE, Los Alamitos, CA, 626\u2013629."},{"key":"e_1_3_1_6_2","first-page":"84","volume-title":"Proceedings of ASP-DAC","year":"2018","unstructured":"Chenguang Wang, Yici Cai, Qiang Zhou, and Haoyi Wang. 2018. ASAX: Automatic security assertion extraction for detecting hardware Trojans. In Proceedings of ASP-DAC. IEEE, Los Alamitos, CA, 84\u201389."},{"key":"e_1_3_1_7_2","first-page":"392","volume-title":"Proceedings of DATE","author":"Farahmandi Farimah","year":"2017","unstructured":"Farimah Farahmandi, Ronny Morad, Avi Ziv, Ziv Nevo, and Prabhat Mishra. 2017. Cost-effective analysis of post-silicon functional coverage events. In Proceedings of DATE. IEEE, Los Alamitos, CA, 392\u2013397."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98116-1"},{"key":"e_1_3_1_9_2","first-page":"1","volume-title":"Proceedings of DAC","author":"Danese Alessandro","year":"2017","unstructured":"Alessandro Danese, Nicol\u00f2 Dalla Riva, and Graziano Pravadelli. 2017. A-team: Automatic template-based assertion miner. In Proceedings of DAC. IEEE, Los Alamitos, CA, 1\u20136."},{"key":"e_1_3_1_10_2","first-page":"1550","volume-title":"Proceedings of DATE","author":"Danese Alessandro","year":"2018","unstructured":"Alessandro Danese, Valeria Bertacco, and Graziano Pravadelli. 2018. Symbolic assertion mining for security validation. In Proceedings of DATE. 1550\u20131555."},{"key":"e_1_3_1_11_2","article-title":"Mangrove: An inference-based dynamic invariant mining for GPU architectures","author":"Pravadelli Nicola Bombieri, Federico Busato, Alessandro Danese, Luca Piccolboni, and Graziano","year":"2020","unstructured":"Nicola Bombieri, Federico Busato, Alessandro Danese, Luca Piccolboni, and Graziano Pravadelli. 2020. Mangrove: An inference-based dynamic invariant mining for GPU architectures. IEEE Transactions on Computers 69, 4 (2020), 606\u2013620.","journal-title":"IEEE Transactions on Computers"},{"key":"e_1_3_1_12_2","first-page":"1","volume-title":"Proceedings of FDL","author":"Ghasempouri Tara","year":"2019","unstructured":"Tara Ghasempouri, Alessandro Danese, Graziano Pravadelli, Nicola Bombieri, and Jaan Raik. 2019. RTL assertion mining with automated RTL-to-TLM abstraction. In Proceedings of FDL. 1\u20138."},{"key":"e_1_3_1_13_2","first-page":"111","volume-title":"Proceedings of VLSI-SoC","author":"Ghasempouri Tara","year":"2019","unstructured":"Tara Ghasempouri, Jan Malburg, Alessandro Danese, Graziano Pravadelli, Goerschwin Fey, and Jaan Raik. 2019. Engineering of an effective automatic dynamic assertion mining platform. In Proceedings of VLSI-SoC. IEEE, Los Alamitos, CA, 111\u2013116."},{"key":"e_1_3_1_14_2","first-page":"607","volume-title":"Proceedings of ASP-DAC","author":"Chang Po-Hsien","year":"2010","unstructured":"Po-Hsien Chang and Li-C. Wang. 2010. Automatic assertion extraction via sequential data mining of simulation traces. In Proceedings of ASP-DAC. IEEE, Los Alamitos, CA, 607\u2013612."},{"key":"e_1_3_1_15_2","first-page":"67","volume-title":"Proceedings of DATE","author":"Danese Alessandro","year":"2015","unstructured":"Alessandro Danese, Tara Ghasempouri, and Graziano Pravadelli. 2015. Automatic extraction of assertions from execution traces of behavioural models. In Proceedings of DATE. IEEE, Los Alamitos, CA, 67\u201372."},{"key":"e_1_3_1_16_2","first-page":"714","volume-title":"Proceedings of ICCAD","author":"Fern Nicole","year":"2017","unstructured":"Nicole Fern and Kwang-Ting Cheng. 2017. Mining mutation testing simulation traces for security and testbench debugging. In Proceedings of ICCAD. IEEE, Los Alamitos, CA, 714\u2013721."},{"key":"e_1_3_1_17_2","first-page":"34","volume-title":"Proceedings of ATS","author":"Hekmatpour Amir","year":"2005","unstructured":"Amir Hekmatpour and Azadeh Salehi. 2005. Block-based schema-driven assertion generation for functional verification. In Proceedings of ATS. IEEE, Los Alamitos, CA, 34\u201339."},{"key":"e_1_3_1_18_2","unstructured":"Takamitsu Yamada. 2009. Assertion generating system program thereof circuit verifying system and assertion generating method. US Patent 7 603 636."},{"key":"e_1_3_1_19_2","first-page":"545","volume-title":"Proceedings of DATE","author":"Rogin Frank","year":"2008","unstructured":"Frank Rogin, Thomas Klotz, Gorschwin Fey, Rolf Drechsler, and Steffen Rulke. 2008. Automatic generation of complex properties for hardware designs. In Proceedings of DATE. IEEE, Los Alamitos, CA, 545\u2013548."},{"key":"e_1_3_1_20_2","volume-title":"Proceedings of MEMOCODE","year":"2011","unstructured":"Lingyi Liu, David Sheridan, Viraj Athavale, and Shobha Vasudevan. 2011. Automatic generation of assertions from system level design using data mining. In Proceedings of MEMOCODE. IEEE, Los Alamitos, CA, 191\u2013200."},{"key":"e_1_3_1_21_2","first-page":"775","volume-title":"Proceedings of DAC","author":"Hangal Sudheendra","year":"2005","unstructured":"Sudheendra Hangal, Sridhar Narayanan, Naveen Chandra, and Sandeep Chakravorty. 2005. Iodine: A tool to automatically infer dynamic invariants for hardware designs. In Proceedings of DAC. IEEE, Los Alamitos, CA, 775\u2013778."},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2013.2241176"},{"key":"e_1_3_1_23_2","doi-asserted-by":"crossref","DOI":"10.1145\/3510578","article-title":"A survey on assertion-based hardware verification","author":"Witharana Hasini","year":"2022","unstructured":"Hasini Witharana, Yangdi Lyu, Subodha Charles, and Prabhat Mishra. 2022. A survey on assertion-based hardware verification. ACM Computing Surveys 54, 11s (2022), Article 225, 33 pages.","journal-title":"ACM Computing Surveys"},{"key":"e_1_3_1_24_2","first-page":"256","volume-title":"Proceedings of DAC.","author":"Turumella Babu","year":"2008","unstructured":"Babu Turumella and Mukesh Sharma. 2008. Assertion-based verification of a 32 thread SPARC\u2122 CMT microprocessor. In Proceedings of DAC.IEEE, Los Alamitos, CA, 256\u2013261."},{"key":"e_1_3_1_25_2","doi-asserted-by":"crossref","unstructured":"Vivek N. Kallankara M. H. Neishaburi Katarzyna Radecka and Zeljko Zilic. 2010. Using assertions for wireless system monitoring and debugging. In Proceedings of NEWCAS . IEEE Los Alamitos CA 401\u2013404.","DOI":"10.1109\/NEWCAS.2010.5603989"},{"key":"e_1_3_1_26_2","volume-title":"Proceedings of LATW","year":"2014","unstructured":"Nicola Bombieri, Franco Fummi, Valerio Guarnieri, Graziano Pravadelli, Francesco Stefanni, Tara Ghasempouri, Michele Lora, Giovanni Auditore, and Mirella Negro Marcigaglia. 2014. On the reuse of RTL assertions in SystemC TLM verification. In Proceedings of LATW. IEEE, Los Alamitos, CA."},{"key":"e_1_3_1_27_2","first-page":"85","volume-title":"Proceedings of DATE","author":"Bombieri Nicola","year":"2015","unstructured":"Nicola Bombieri, Riccardo Filippozzi, Graziano Pravadelli, and Francesco Stefanni. 2015. RTL property abstraction for TLM assertion-based verification. In Proceedings of DATE. 85\u201390."},{"key":"e_1_3_1_28_2","unstructured":"Dominique Borrione Katell Morin-Allory P. Ostier and Miao Liu. 2005. On-line assertion-based verification with proven correct monitors. In Proceedings of ITI . IEEE Los Alamitos CA."},{"issue":"2","key":"e_1_3_1_29_2","article-title":"Hybrid, incremental assertion-based verification for TLM design flows","volume":"24","author":"Bombieri Nicola","year":"2007","unstructured":"Nicola Bombieri, Franco Fummi, Graziano Pravadelli, and Andrea Fedeli. 2007. Hybrid, incremental assertion-based verification for TLM design flows. IEEE Design & Test of Computers 24, 2 (2007), 140\u2013152.","journal-title":"IEEE Design & Test of Computers"},{"key":"e_1_3_1_30_2","volume-title":"Proceedings of the DATE Workshop","author":"Chenard Jean-Samuel","year":"2007","unstructured":"Jean-Samuel Chenard, Stephan Bourduas, Nathaniel Azuelos, and Marc Boule. 2007. Hardware assertion checkers in on-line detection of faults in a hierarchical-ring network-on-chip. In Proceedings of the DATE Workshop."},{"key":"e_1_3_1_31_2","volume-title":"Proceedings of PRIME-LA","author":"Alsaiari Uthman","year":"2017","unstructured":"Uthman Alsaiari, Fayez Gebali, and Mostafa Abd-El-Barr. 2017. Programmable assertion checkers for hardware Trojan detection. In Proceedings of PRIME-LA. IEEE, Los Alamitos, CA."},{"key":"e_1_3_1_32_2","first-page":"49","volume-title":"Proceedings of HOST","author":"Bilzor Michael","year":"2012","unstructured":"Michael Bilzor, Ted Huffmire, Cynthia Irvine, and Tim Levin. 2012. Evaluating security requirements in a general-purpose processor by combining assertion checkers with code coverage. In Proceedings of HOST. IEEE, Los Alamitos, CA, 49\u201354."},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3441297"},{"key":"e_1_3_1_34_2","unstructured":"https:\/\/www.accellera.org\/downloads\/standards\/ovl. Accellera. (n.d.). Download OVL (Open Verification Library)"},{"key":"e_1_3_1_35_2","unstructured":"IEEE. 2010. 1850-2010\u2014IEEE Standard for Property Specification Language (PSL) . IEEE Los Alamitos CA."},{"key":"e_1_3_1_36_2","unstructured":"IEEE. (n.d.). 1800-2012\u2014IEEE Standard for SystemVerilog\u2013Unified Hardware Design Specification and Verification Language . IEEE Los Alamitos CA."},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/3086868"},{"key":"e_1_3_1_38_2","first-page":"495","volume-title":"Proceedings of UIC-ATC-SCALCOM","author":"Yang Xia","year":"2014","unstructured":"Xia Yang, Peng Shi, Bo Tian, Bing Zeng, and Wei Xiao. 2014. Trust-E: A trusted embedded operating system based on the ARM trustzone. In Proceedings of UIC-ATC-SCALCOM. 495\u2013501."},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2528521.1508258"},{"key":"e_1_3_1_40_2","volume-title":"Proceedings of ICCD","author":"Farahmandi Farimah","year":"2017","unstructured":"Farimah Farahmandi and Prabhat Mishra. 2017. FSM anomaly detection using formal analysis. In Proceedings of ICCD. IEEE, Los Alamitos, CA."},{"key":"e_1_3_1_41_2","doi-asserted-by":"crossref","DOI":"10.1109\/TCAD.2011.2120970","article-title":"Theoretical fundamentals of gate level information flow tracking","author":"Hu Wei","year":"2011","unstructured":"Wei Hu, Jason Oberg, Ali Irturk, Mohit Tiwari, Timothy Sherwood, Dejun Mu, and Ryan Kastner. 2011. Theoretical fundamentals of gate level information flow tracking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 30, 8 (2011), 1128\u20131140.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2017.7927266"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISVLSI.2015.107"},{"key":"e_1_3_1_44_2","unstructured":"https:\/\/www.trust-hub.org\/. TrustHub"},{"key":"e_1_3_1_45_2","unstructured":"OpenCores. 2021. Home Page. Retrieved November 28 2022 from https:\/\/www.opencores.org\/."}],"container-title":["ACM Journal on Emerging Technologies in Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3565801","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3565801","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:48:52Z","timestamp":1750182532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3565801"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,19]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,31]]}},"alternative-id":["10.1145\/3565801"],"URL":"https:\/\/doi.org\/10.1145\/3565801","relation":{},"ISSN":["1550-4832","1550-4840"],"issn-type":[{"value":"1550-4832","type":"print"},{"value":"1550-4840","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,19]]},"assertion":[{"value":"2021-12-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-20","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}