密码侧信道安全建模与形式化验证方法

王省欣; 胡伟; 黄璇; 林宸羽; 周易

doi:10.11999/JEIT260631

密码侧信道安全建模与形式化验证方法

doi: 10.11999/JEIT260631 cstr: 32379.14.JEIT260631

西北工业大学网络空间安全学院西安 710072

基金项目: 国家自然科学基金项目(No. U23B2041、, 62074131, 62504188)

详细信息

作者简介:
王省欣：女，博士生，研究方向为侧信道安全验证，形式化验证

胡伟：男，教授，研究方向为硬件安全，形式化验证

黄璇：女，博士生，研究方向为形式化验证

林宸羽：女，硕士生，研究方向为处理器安全

周易：男，硕士生，研究方向为侧信道泄露量化评估

通讯作者:
胡伟　weihu@nwpu.edu.cn

中图分类号: TP309
计量
- 文章访问数: 11
- HTML全文浏览量: 1
- PDF下载量: 1
- 被引次数: 0
出版历程
- 收稿日期: 2026-05-15
- 修回日期: 2026-08-13
- 录用日期: 2026-08-13
- 网络出版日期: 2026-08-20

A Cryptographic Side-Channel Security Modeling and Formal Verification Method

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

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

摘要

摘要: 侧信道泄露严重威胁密码核设计的实现安全性。现有侧信道泄露检测方法主要依赖数据驱动的量化评估，缺乏严格的数学模型，完备性有限。针对上述问题，提出了一种密码侧信道安全建模与形式化验证方法。该方法通过构建侧信道安全模型，利用信息流分析实现对时间侧信道泄露、能量侧信道泄露和故障传播行为的统一建模，进一步提取侧信道安全属性，并通过形式化验证所提取的安全属性来识别密码核设计中潜在的侧信道泄露风险。实验结果表明，本文所提出的方法能够准确识别出AES、SM4、LED、PRESENT和IDEA密码核设计中潜在的侧信道泄露风险，并可评估掩码与故障感染防御机制的有效性。
- 硬件安全 /
- 侧信道安全验证 /
- 属性检查 /
- 信息流分析 /
- 安全评估
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

HTML全文

图 1 密码侧信道安全建模与形式化验证方法

下载: 全尺寸图片幻灯片

图 2 一个密码核设计中信息流动分析案例

下载: 全尺寸图片幻灯片

图 3 AND-2安全模型部分真值表与电路结构

下载: 全尺寸图片幻灯片

图 4 密码核设计侧信道安全模型建立过程

下载: 全尺寸图片幻灯片

图 5 故障属性提取过程

下载: 全尺寸图片幻灯片

图 6 侧信道安全验证方法

下载: 全尺寸图片幻灯片

图 7 AES时间侧信道安全验证结果

下载: 全尺寸图片幻灯片

图 8 RSM掩码防护安全验证结果

下载: 全尺寸图片幻灯片

图 9 故障属性断言和故障传播模型初始化示例

下载: 全尺寸图片幻灯片

图 10 AES行移位感染防护的故障注入风险安全验证结果

下载: 全尺寸图片幻灯片

表 1 密码核设计侧信道安全模型分类

侧信道安全模型种类	属性标签释义	标签状态释义	标签流动含义
时间侧信道模型	跟踪标签	$ {S}_{\text{t}}=1 $，信号S为敏感信息	敏感信息的流动
能量侧信道模型	敏感标签	$ {S}_{\text{t}}=1 $，信号S为敏感信息	与敏感信息有关的翻转
故障传播模型	故障标签	$ {S}_{\text{t}}=1 $，信号S发生翻转故障	故障信息的传播路径

下载: 导出CSV

表 2 分组密码核设计时间侧信道安全验证结果

	属性断言	验证结果	时间侧信道风险	验证时间
AES	$ \text{assume}Kin\_ t=\text{128'hff}···\text{fff};\text{assert}Dvld\_ t=\text{1'b0;} $	验证成功	不存在时间侧信道风险	9.1s
SM4	$ \text{assume}Kin\_ t=\text{128'hff}···\text{fff};\text{assert}S\_ Dvld\_ t=\text{1'b0;} $	验证成功	不存在时间侧信道风险	14.7s
LED	$ \text{assume}Kin\_ t=\text{64'hff}···\text{fff};\text{assert}L\_ Dvld\_ t=\text{1'b0;} $	验证成功	不存在时间侧信道风险	7.2s
PRESENT	$ \text{assume}Kin\_ t=\text{80'hff}···\text{fff};\text{assert}P\_ Dvld\_ t=\text{1'b0;} $	验证成功	不存在时间侧信道风险	5.4s
IDEA	$ \text{assume}Kin\_ t=\text{128'hff}···\text{fff};\text{assert}I\_ Dvld\_ t=\text{1'b1;} $	验证成功	存在时间侧信道风险	17.4s

下载: 导出CSV

表 3 分组密码核设计能量侧信道安全验证结果

设计模块		可控属性		密钥-能耗非线性耦合属性		密钥-能耗可区分耦合属性		验证时间
设计模块		属性断言与验证结果		属性断言与验证结果		属性断言与验证结果		验证时间
AES	字节代替	$ \begin{aligned}&\text{assume}Din\_ t=\text{128'hff}\cdots\text{f};\\& \text{assert}sb\_ t!=0;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ sb\_ t \gt =2;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ sb\_ t!=HW\_ sin\_ t;\end{aligned} $	验证通过	26.5 s
	列混淆	$ \begin{aligned}&\text{assume}Din\_ t=\text{128'hff}\cdots\text{f};\\& \text{assert}mix\_ t!=0\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ mix\_ t \gt =2;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ mix\_ t!=HW\_ sr\_ t;\end{aligned} $	验证通过
	行移位	$ \begin{aligned}&\text{assume}Din\_ t=\text{128'hff}\cdots\text{f};\\& \text{assert}sr\_ t!=0\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ sr\_ t \gt =2;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ sr\_ t!=HW\_ sb\_ t;\end{aligned} $	验证未通过
	密钥扩展	$ \begin{aligned}&\text{assume}Din\_ t=\text{128'hff}\cdots\text{f};\\& \text{assert}ke\_ t!=0\end{aligned} $	验证未通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ ke\_ t \gt =2;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ ke\_ t!=HW\_ akin\_ t;\end{aligned} $	验证通过
SM4	S盒	$ \begin{aligned}&\text{assume}Din\_ t=\text{128'hff}\cdots\text{f};\\& \text{assert}s\_ t!=0\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ s\_ t \gt =2;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ s\_ t!=HW\_ xor\_ t;\end{aligned} $	验证通过	45.1 s
	L移位	$ \begin{aligned}\text{assume}Din\_ t&=\text{128'hff}\cdots\text{f};\\& \text{assert}L\_ t!=0\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ L\_ t \gt =2;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ L\_ t!=HW\_ s\_ t;\end{aligned} $	验证通过
	密钥扩展	$ \begin{aligned}&\text{assume}Din\_ t=\text{128'hff}\cdots\text{f};\\& \text{assert}k\_ t!=0\end{aligned} $	验证未通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ k\_ t \gt =2;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{128'h80}\cdots0;\\& \text{assert}HW\_ k\_ t!=HW\_ skin\_ t;\end{aligned} $	验证通过
LED	Sub- Cell	$ \begin{aligned}&\text{assume}Din\_ t=\text{64'hff}\cdots\text{f};\\& \text{assert}sub\_ t!=0\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{64'h80}\cdots0;\\& \text{assert}HW\_ sub\_ t \gt =2;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=64\text{'h80}\cdots0;\\&\text{assert}HW\_ sub\_ t! =HW\_ Lin\_ t;\end{aligned} $	验证通过	19.7 s
PRE- SENT	S-box	$ \begin{aligned}&\text{assume}Din\_ t=\text{64hff}\cdots\text{f};\\& \text{assert}S\_ t!=0\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{80'h80}\cdots0;\\& \text{assert}HW\_ S\_ t \gt =2;\end{aligned} $	验证通过	$ \begin{aligned}&\text{assume}Kin\_ t=\text{80'h80}\cdots0;\\&\text{assert}HW\_ S\_ t!=HW\_ Pin\_ t;\end{aligned} $	验证通过	15.4 s

下载: 导出CSV

表 4 含有故障感染防御机制的密码核设计故障注入风险安全验证实验结果

	故障感染防御方案	Yosys验证结果	安全性分析	验证时间
文献[20]	对行移位变换的原始路径进行交叉变换	验证通过	轮输出故障满足故障属性，存在被攻击者利用的风险	13.1 s
文献[21]	通过多字节扩散改变原始故障传播路径	验证通过	轮输出故障满足故障属性，存在被攻击者利用的风险	15.3 s
文献[22]	设计中增加虚拟轮计算，混淆迭代结果	验证未通过	轮输出故障不满足故障属性，有效防护故障注入分析	32.7 s

下载: 导出CSV

表 5 与现有侧信道安全评估方法对比

	文献[10]	文献[6]	文献[11]	文献[12,13]	文献[7]	文献[9]	文献[17,18]	本方法
研究对象	时间侧信道	能量侧信道			故障侧信道			时间、能量与故障侧信道
建模方式	测量时间	信号翻转统计			推导故障传播路径	/		信息流分析
分析方法	信息熵	功能属性验证	KL散度	深度学习	差分分析	信息熵	功能属性验证	侧信道安全属性验证
不依赖大量数据仿真	×	√	×	×	/	×	√	√
支持侧信道防护评估	×	×	×	×	×	√	×	√

下载: 导出CSV

参考文献(22)

[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.