A Cryptographic Side-Channel Security Modeling and Formal Verification Method

WANG Xingxin; HU Wei; HUANG Xuan; LIN Chenyu; ZHOU Yi

doi:10.11999/JEIT260631

Article Contents

Article Navigation > Journal of Electronics & Information Technology > 2026 >

WANG Xingxin, HU Wei, HUANG Xuan, LIN Chenyu, ZHOU Yi. A Cryptographic Side-Channel Security Modeling and Formal Verification Method[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT260631

Citation:

WANG Xingxin, HU Wei, HUANG Xuan, LIN Chenyu, ZHOU Yi. A Cryptographic Side-Channel Security Modeling and Formal Verification Method[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT260631

Citation:

PDF( 3234 KB)

A Cryptographic Side-Channel Security Modeling and Formal Verification Method

doi: 10.11999/JEIT260631 cstr: 32379.14.JEIT260631

School of Cybersecurity, Northwestern Polytechnical University, Xi’an, Shaanxi 710072, China

Funds: The National Natural Science Foundation of China (No. U23B2041, 62074131, 62504188)

Received Date: 2026-05-15
Accepted Date: 2026-08-13
Rev Recd Date: 2026-08-13

Available Online: 2026-08-20

Abstract

Abstract

Objective Compared with post-silicon side-channel security analysis, pre-silicon side-channel security verification during the design phase enables the earlier identification of potential side-channel security vulnerabilities in cryptographic core designs, thereby effectively reducing the cost and time of post-silicon remediation. However, most existing pre-silicon side-channel security assessment approaches rely on data-driven statistical analysis or artificial intelligence techniques and require complex calculations on large amounts of data to mitigate the impact of insufficient coverage on the assessment results. In addition, existing methods typically adopt independent modeling strategies for different types of side channels, lacking a unified side-channel security modeling approach. A cryptographic side-channel security modeling and formal verification method is proposed, supporting unified and automated modeling of different types of side channels by constructing a side-channel security model. The method can identify potential timing side-channel, power side-channel and fault injection vulnerabilities in cryptographic core designs, and analyze the effectiveness of side-channel countermeasures based on side-channel security property checking. Methods The proposed cryptographic side-channel security modeling and formal verification method includes side-channel security model construction, side-channel security property extraction, and side-channel security verification. The side-channel security model uses information flow analysis to characterize timing side-channel leakage, power side-channel leakage, and fault propagation behavior in cryptographic core designs, providing an effective mathematical model for side-channel security verification. Specifically, the side-channel security model utilizes changes in signal labels to analyze information flows during the encryption process by assigning a label to a signal bit and defining label propagation rules. Side-channel security properties formally describe the behavioral characteristics of side-channel leakage, including timing properties, power properties, and fault properties, providing theoretical support for side-channel security verification. Side-channel security verification uses the extracted security properties as verification constraints and employs formal verification tools to identify potential timing side-channel, power side-channel, and fault injection vulnerabilities in cryptographic core designs. Furthermore, the method can analyze the effectiveness of masking and fault injection countermeasures against side-channel vulnerabilities. Results and Discussions The proposed side-channel security verification method utilizes formal verification techniques to accurately identify potential side-channel security vulnerabilities in various block cipher core designs, and evaluate the effectiveness of side-channel countermeasures based on side-channel security property constraints. The timing side-channel verification results demonstrate that the proposed method can accurately identify timing side-channel security vulnerabilities in AES, SM4, LED, PRESENT, and IDEA core designs within 20s (Table 2, Fig. 7). No timing side-channel vulnerabilities are identified in the other cryptographic core designs, except for IDEA, which exhibits timing side-channel vulnerabilities caused by modular multiplication operations. The power side-channel security verification results show that formal checks based on controllability property, key–power distinguishability coupling property and key–power nonlinear coupling property can accurately identify target modules with potential power side-channel security vulnerabilities in AES, SM4, LED and PRESENT within 1 minute (Table 3). The key expansion module in cryptographic core designs does not cause key leakage through key-dependent power consumption, as it fails to satisfy the controllability property. In addition, the experimental results indicate that the masking protection in the RSM core design can prevent the correct key from being distinguished through random masking (Fig. 8). The fault injection security verification results for three AES core designs with infective countermeasures demonstrate that the proposed method can analyze the effectiveness of fault infection countermeasures. The results show that the infection countermeasure requires not only altering the fault propagation path but also disrupting the algebraic relationships among faults (Table 4, Fig. 10). Conclusions This paper proposes a cryptographic side-channel security modeling and formal verification method to address the lack of formal mathematical models and the limited completeness of existing data-driven side-channel security assessment methods. The proposed method first achieves unified modeling of timing leakage, power leakage, and fault propagation behaviors from the perspective of information flow analysis. Based on the constructed side-channel security model, side-channel security properties are extracted to formally characterize the behavioral features of side-channel information leakage and propagation during the encryption process. Potential side-channel security vulnerabilities in cryptographic core designs are then identified through formal checking using the extracted security properties as constraints. The proposed method provides an effective solution for the unified modeling and formal security verification of different types of side channels. Experimental results obtained from the side-channel security verification of various block cryptographic core designs demonstrate that: (1) the proposed method can uniformly model timing side-channel leakage, power side-channel leakage, and fault propagation behaviors in cryptographic core designs; (2) the proposed method can accurately identify timing side-channel vulnerabilities, power side-channel vulnerabilities, and fault injection vulnerabilities in cryptographic core designs, including AES, SM4, IDEA, LED and PRESENT; (3) the proposed method can analyze the effectiveness of masking and fault infection countermeasures. However, this study only qualitatively identifies side-channel security vulnerabilities in cryptographic core designs; pre-silicon quantitative assessment of side-channel leakage should be investigated in future work.
- Hardware security,
- Side-Channel security verification,
- Property checking,
- Information flow analysis,
- Security assessment

FullText(HTML)

References(22)

References

[1]	PARIKH R S and PARIKH K. Survey on hardware security: PUFs, Trojans, and side-channel attacks[J]. International Journal of Engineering Research and Applications, 2025, 15(2): 30–37. doi: 10.9790/9622-15023037.
[2]	赵毅强, 闫明凯, 张启智, 等. 基于多阶段相关功耗分析的SM4-XTS侧信道分析方法[J]. 电子与信息学报, 2024, 46(11): 4161–4169. doi: 10.11999/JEIT240183. ZHAO Yiqiang, YAN Mingkai, ZHANG Qizhi, et al. SM4-XTS side channel analysis method based on multi-stage CPA[J]. Journal of Electronics & Information Technology, 2024, 46(11): 4161–4169. doi: 10.11999/JEIT240183.
[3]	严智广, 韦永壮, 叶涛. 全轮超轻量级分组密码PFP的相关密钥差分分析[J]. 电子与信息学报, 2025, 47(3): 729–738. doi: 10.11999/JEIT240782. YAN Zhiguang, WEI Yongzhuang, and YE Tao. Related-key differential cryptanalysis of full-round PFP ultra-lightweight block cipher[J]. Journal of Electronics & Information Technology, 2025, 47(3): 729–738. doi: 10.11999/JEIT240782.
[4]	BEPARY M K, ZHANG Tao, FARAHMANDI F, et al. PreSCAN: A comprehensive review of pre-silicon physical side-channel vulnerability assessment methodologies[J]. Chips, 2024, 3(4): 311–333. doi: 10.3390/chips3040016.
[5]	SOCHA P, MIŠKOVSKÝ V, and NOVOTNÝ M. A comprehensive survey on the non-invasive passive side-channel analysis[J]. Sensors, 2022, 22(21): 8096. doi: 10.3390/s22218096.
[6]	ALATOUN K and VEMURI R. Power side-channel verification in hardware designs[C]. NAECON 2024 - IEEE National Aerospace and Electronics Conference, Dayton, USA, 2024: 291–296. doi: 10.1109/NAECON61878.2024.10670646.
[7]	KHANNA P, REBEIRO C, and HAZRA A. XFC: A framework for exploitable fault characterization in block ciphers[C]. Proceedings of the 54th Annual Design Automation Conference, Austin, USA, 2017: 8. doi: 10.1145/3061639.3062340.
[8]	VAN WOUDENBERG J, GROSSMANN P, VARNA A L, et al. Invited: Pre-silicon side channel and fault analysis[C]. 2023 60th ACM/IEEE Design Automation Conference, San Francisco, USA, 2023: 1–4. doi: 10.1109/DAC56929.2023.10247882.
[9]	FENG Jingyi, CHEN Hua, LI Yang, et al. A framework for evaluation and analysis on infection countermeasures against fault attacks[J]. IEEE Transactions on Information Forensics and Security, 2020, 15: 391–406. doi: 10.1109/TIFS.2019.2903653.
[10]	毛保磊, 胡伟, 慕德俊, 等. 基于信息熵的RSA硬件时间隐通道信息泄露量化研究[J]. 计算机学报, 2018, 41(2): 426–438. doi: 10.11897/SP.J.1016.2018.00426. MAO Baolei, HU Wei, MU Dejun, et al. Quantitative analysis of information leakage through hardware RSA timing channel based on entropy theory[J]. Chinese Journal of Computers, 2018, 41(2): 426–438. doi: 10.11897/SP.J.1016.2018.00426.
[11]	HE Miao, PARK J, NAHIYAN A, et al. RTL-PSC: Automated power side-channel leakage assessment at register-transfer level[C]. 2019 IEEE 37th VLSI Test Symposium, Monterey, USA, 2019: 1–6. doi: 10.1109/VTS.2019.8758600.
[12]	LI Yanbin, ZHU Jiajie, LIU Zhe, et al. Deep learning gradient visualization-based pre-silicon side-channel leakage location[J]. IEEE Transactions on Information Forensics and Security, 2024, 19: 2340–2355. doi: 10.1109/TIFS.2024.3350375.
[13]	SRIVASTAVA A, DAS S, CHOUDHURY N, et al. SCAR: Power side-channel analysis at RTL level[J]. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 2024, 32(6): 1110–1123. doi: 10.1109/TVLSI.2024.3390601.
[14]	KULIK T, DONGOL B, LARSEN P G, et al. A survey of practical formal methods for security[J]. Formal Aspects of Computing, 2022, 34(1): 5. doi: 10.1145/3522582.
[15]	唐时博, 朱嘉诚, 慕德俊, 等. RISC-V处理器权限正确性验证与提权漏洞自动挖掘方法[J]. 电子与信息学报, 2025, 47(9): 3081–3092. doi: 10.11999/JEIT250362. TANG Shibo, ZHU Jiacheng, MU Dejun, et al. Verification of privilege correctness and automated exploitation of privilege escalation vulnerabilities in RISC-V processors[J]. Journal of Electronics & Information Technology, 2025, 47(9): 3081–3092. doi: 10.11999/JEIT250362.
[16]	KIBRIA R, FARAHMANDI F, and TEHRANIPOOR M. A survey on SoC security verification methods at the pre-silicon stage[EB/OL]. https://eprint.iacr.org/2024/1280, 2024.
[17]	PUNDIR N, LI Henian, LIN Lang, et al. Security properties driven pre-silicon laser fault injection assessment[C]. 2022 IEEE International Symposium on Hardware Oriented Security and Trust, McLean, USA, 2022: 9–12. doi: 10.1109/HOST54066.2022.9840109.
[18]	UDDIN A, SAHA S K, FARAHMANDI F, et al. Case study: Fault-injection vulnerability assessment at RTL level[C]. 2024 IEEE Physical Assurance and Inspection of Electronics, Huntsville, USA, 2024: 1–7. doi: 10.1109/PAINE62042.2024.10792811.
[19]	Digital Electronic Systems. DPA contest v4[EB/OL]. https://dpacontest.telecom-paris.fr/v4/index.php, 2013.
[20]	JOYE M, MANET P, and RIGAUD J B. Strengthening hardware AES implementations against fault attacks[J]. IET Information Security, 2007, 1(3): 106–110. doi: 10.1049/iet-ifs:20060163.
[21]	FOURNIER J, RIGAUD J B, BOUQUET S, et al. Design and characterisation of an AES chip embedding countermeasures[J]. International Journal of Intelligent Engineering Informatics, 2011, 1(3/4): 328–347. doi: 10.1504/IJIEI.2011.044101.
[22]	GIERLICHS B, SCHMIDT J M, and TUNSTALL M. Infective computation and dummy rounds: Fault protection for block ciphers without check-before-output[C]. 2nd International Conference on Cryptology and Information Security in Latin America, Santiago, Chile, 2012: 305–321. doi: 10.1007/978-3-642-33481-8_17.