{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:57:03Z","timestamp":1759971423625,"version":"build-2065373602"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"6","funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2023YFB4403000"],"award-info":[{"award-number":["2023YFB4403000"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Natural Science Foundation of Tianjin City","award":["22JCQNJC00970"],"award-info":[{"award-number":["22JCQNJC00970"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2025,11,30]]},"abstract":"<jats:p>Side-channel analysis (SCA) attacks pose a significant threat to cryptographic integrated circuits (ICs). While designers have endeavored to introduce various countermeasures during the IC development phase, many of these solutions incur substantial overheads in terms of area, power, and performance. Additionally, they often necessitate a full-custom circuit design for effective deployment. This issue arises due to the absence of systematic methodologies and analytical tools for circuit designers to accurately identify the sources of side-channel leakage within the hardware design. In this article, we propose the concept of side-channel tracking logic and, building upon this foundation, introduce a novel framework that seamlessly integrates with commercial design flows to automatically identify and safeguard leaky paths. Our approach begins by pinpointing partial logic cells that exhibit the highest information leakage using dynamic correlation analysis. Subsequently, formal-based leakage property checking constructs comprehensive leaky paths centered on these cells. In this process, side-channel tracking logic was proposed and applied for the first time to trace and extract side-channel leakage paths. Based on this, an automated formal modeling and leakage property verification tool was designed. Once these paths are discerned, we deploy apt hardware countermeasures, encompassing Boolean masking and random precharge, to eradicate information leakage along these routes. This framework has been experimentally validated across different encryption circuits and the efficacy of our methodology is corroborated through both simulated and real-world measurements on FPGA implementations. Empirical results showcase an enhancement of over 1000\u00d7 in side-channel resistance, incurring a modest overhead of less than 6.53% across power, area, and performance metrics.<\/jats:p>","DOI":"10.1145\/3768154","type":"journal-article","created":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T11:19:41Z","timestamp":1758021581000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Boosting Cryptographic ICs\u2019 Side-Channel Resistance: A Formal Framework for Automatic Identification and Protection of Leaky Paths"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9111-119X","authenticated-orcid":false,"given":"Qizhi","family":"Zhang","sequence":"first","affiliation":[{"name":"Tianjin University","place":["Tianjin, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4505-7495","authenticated-orcid":false,"given":"Ya","family":"Gao","sequence":"additional","affiliation":[{"name":"Tianjin University","place":["Tianjin, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7118-9379","authenticated-orcid":false,"given":"Haocheng","family":"Ma","sequence":"additional","affiliation":[{"name":"Tianjin University","place":["Tianjin, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1443-9279","authenticated-orcid":false,"given":"Jiaji","family":"He","sequence":"additional","affiliation":[{"name":"Tianjin University","place":["Tianjin, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9387-8813","authenticated-orcid":false,"given":"Yiqiang","family":"Zhao","sequence":"additional","affiliation":[{"name":"Tianjin University","place":["Tianjin, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9896-9407","authenticated-orcid":false,"given":"Xiaolong","family":"Guo","sequence":"additional","affiliation":[{"name":"Kansas State University","place":["Manhattan, United States"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,8]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48405-1_25"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/VTS.2019.8758600"},{"key":"e_1_3_1_4_2","volume-title":"Proceedings of the 2020 IEEE International Symposium on Hardware Oriented Security and Trust (HOST) IEEE. 23\u201334","author":"Vinod Ganesan Muhammad Arsath KF","year":"2020","unstructured":"Muhammad Arsath KF, Vinod Ganesan, Rahul Bodduna, and Chester Rebeiro. 2020. PARAM: A microprocessor hardened for power side-channel attack resistance. In Proceedings of the 2020 IEEE International Symposium on Hardware Oriented Security and Trust (HOST) IEEE. 23\u201334."},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3383445"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASP-DAC52403.2022.9712551"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20465-4_6"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530413"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/HOST45689.2020.9300271"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.29007\/mbf3"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2463209.2488830"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSSC.2019.2945944"},{"key":"e_1_3_1_13_2","volume-title":"Proceedings of the 2020 IEEE International Solid-State Circuits Conference-(ISSCC) . IEEE, 424\u2013426","author":"Das Debayan","year":"2020","unstructured":"Debayan Das, Josef Danial, Anupam Golder, Nirmoy Modak, Shovan Maity, Baibhab Chatterjee, Donghyun Seo, Muya Chang, Avinash Varna, Harish Krishnamurthy, et\u00a0al. 2020. 27.3 EM and power SCA-resilient AES-256 in 65nm CMOS through \\(\\gt 350 \\times\\) current-domain signature attenuation. In Proceedings of the 2020 IEEE International Solid-State Circuits Conference-(ISSCC) . IEEE, 424\u2013426."},{"key":"e_1_3_1_14_2","doi-asserted-by":"crossref","unstructured":"David Knichel Amir Moradi Nicolai M\u00fcller and Pascal Sasdrich. 2021. Automated generation of masked hardware. Cryptology ePrint Archive (2021).","DOI":"10.46586\/tches.v2022.i1.589-629"},{"volume-title":"Advances in Cryptology\u2013ASIACRYPT 2020: Proceedings of the 26th International Conference on the Theory and Application of Cryptology and Information Security, Part I","author":"Knichel David","key":"e_1_3_1_15_2","unstructured":"David Knichel, Pascal Sasdrich, and Amir Moradi. 2020. Silver\u2013statistical independence and leakage verification. In Advances in Cryptology\u2013ASIACRYPT 2020: Proceedings of the 26th International Conference on the Theory and Application of Cryptology and Information Security, Part I . Springer, 787\u2013816."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.46586\/tches.v2021.i2.189-228"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508258"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2011.2120970"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.3390\/electronics11244216"},{"key":"e_1_3_1_20_2","volume-title":"C","author":"Qin Maoyuan","year":"2019","unstructured":"Maoyuan Qin, Wei Hu, Xinmu Wang, Dejun Mu, and Baolei Mao. 2019. Theorem proof based gate level information flow tracking for hardware security verification. Computers & Security 85, C (2019), 225\u2013239."},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/ATS49688.2020.9301533"},{"key":"e_1_3_1_22_2","unstructured":"Jeremy Blackstone Wei Hu Alric Althoff Armaiti Ardeshiricham Lu Zhang and Ryan Kastner. 2020. A unified model for gate level propagation analysis. arXiv:2012.02791. Retrieved from https:\/\/arxiv.org\/abs\/2012.02791"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2013.2247457"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2331332"},{"volume-title":"Proceedings of the 2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD) . IEEE, 1\u20138.","author":"Slpsk Patanjali","key":"e_1_3_1_25_2","unstructured":"Patanjali Slpsk, Prasanna Karthik Vairam, Chester Rebeiro, and V. Kamakoti. 2019. Karna: A gate-sizing based security aware EDA flow for improved power side-channel attack protection. In Proceedings of the 2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD) . IEEE, 1\u20138."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3212719"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.46586\/tches.v2021.i1.305-342"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.29007\/ptmg"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3768154","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T13:51:31Z","timestamp":1759931491000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3768154"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,8]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,11,30]]}},"alternative-id":["10.1145\/3768154"],"URL":"https:\/\/doi.org\/10.1145\/3768154","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2025,10,8]]},"assertion":[{"value":"2024-09-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-30","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}