基于Hoare逻辑的密码软件安全性形式化验证方法

doi:10.13229/j.cnki.jdxbgxb20180418

摘要/Abstract

摘要：

为了解决密码软件安全性验证效率和准确率低的问题，提出了基于Hoare逻辑的密码软件安全性形式化验证方法。首先对密码软件的主要性质进行描述，然后通过密码软件运行时随机向量的分析，得到密码软件运行的矩阵表达式，再将其进行线性变换，计算密码软件运行时数据的方差和协方差矩阵，获得密码软件运行时数据矩阵的主成分空间，并对密码软件运行的主成分进行分析；最后，利用密码软件的逻辑模型和软件运行的状态集合对密码软件安全形式化验证的流程进行分析，建立密码软件的运行模型并设置安全属性，并将密码软件运行时出现的故障进行标记和处理，得到密码软件运行的安全结果，从而实现密码软件安全性形式化的验证。实验结果表明，采用该方法对密码软件的安全性进行验证具有较高的效率，且能够准确地验证密码软件的安全。

关键词: 计算机系统结构, 霍尔逻辑, 密码软件, 安全性验证

Abstract:

In order to solve the problem of low efficiency and low accuracy of cryptographic software security verification, a formal cryptographic software security verification method based on Hoare logic is proposed. The main properties of the cryptographic software are described. Through the analysis of the random vector of the cryptographic software runtime, the matrix expression of the cryptographic software is obtained, which is linearly transformed, and the variance and covariance matrix of the cryptographic software runtime data are calculated to obtain the cryptographic software. The principal component space of the runtime data matrix, and analyzes the principal components of the cryptographic software operation; analyzes the cryptographic software security formal verification process by using the logic model of the cryptographic software and the state set of the software operation, and establishes the running model of the cryptographic software. And set the security attributes, mark and process the faults that occur when the cryptographic software is running, obtain the security results of the cryptographic software running, and realize the formal verification of the cryptographic software security. The experimental results show that the method has high efficiency when verifying the security of cryptographic software, and can accurately verify the security of cryptographic software.

Key words: computer systems architecture, Hoare logic, cipher software, safety verification

中图分类号:

TP393

肖堃. 基于Hoare逻辑的密码软件安全性形式化验证方法[J]. 吉林大学学报(工学版), 2019, 49(4): 1301-1306.

Kun XIAO. Formal verification method for cryptographic software security based on Hoare logic[J]. Journal of Jilin University(Engineering and Technology Edition), 2019, 49(4): 1301-1306.

图/表 5

图1

表1

图2

图3

图4

参考文献 10

1	李耀, 郭进, 杨扬,等. 铁路信号安全关键软件形式化建模[J]. 铁道学报, 2017, 39(9): 74-80.
	LiYao,GuoJin,YangYang,et al.Formal modeling of railway signal safety critical software[J]. Journal of the China Railway Society, 2017, 39(9): 74-80.
2	吕英杰, 徐文静, 刘鹰,等. 基于密码技术的智能电能表软件备案与比对系统设计[J]. 电网技术, 2016, 40(11): 3604-3608.
	Ying-jieLyu ,XuWen-jing,LiuYing,et al.Design of intelligent watt-hour meter software recording and comparing system based on cryptography[J]. Power System Technology, 2016, 40(11): 3604-3608.
3	杨帆, 杨国武, 郝玉洁. 基于模型检测的半量子密码协议的安全性分析[J]. 电子科技大学学报, 2017, 46(5): 716-721.
	YangFan,YangGuo-wu,HaoYu-jie.Security analysis of semi-quantum cryptography protocols by model checking[J]. Journal of University of Electronic Science and Technology of China, 2017, 46(5): 716-721.
4	桓自强, 倪宏, 胡琳琳,等. 基于Android权限机制的应用安全检测方法[J]. 计算机工程与设计, 2016, 37(1): 42-45.
	HuanZi-qiang,NiHong,HuLin-lin,et al.Application security detection based on Android access permission mechanism[J]. Computer Engineering and Design, 2016, 37(1): 42-45.
5	陈昊, 卿斯汉. 基于组合式算法的Android恶意软件检测方法[J]. 电信科学, 2016, 32(10): 15-21.
	ChenHao,Si-hanQing .Android malware detection method based on combined algorithm[J]. Telecommunications Science, 2016, 32(10): 15-21.
6	贾乐, 高杨, 王宇航. 固态热机械密码鉴别器的安全性增强方法[J]. 探测与控制学报, 2017, 39(3):92-96.
	JiaLe, GaoYang, WangYu-hang. Safety enhancement method for solid state thermal mechanical discriminator[J]. Journal of Detection & Control, 2017, 39(3): 92-96.
7	魏琴芳, 杨子明, 胡向东,等. 基于流量特征的登录账号密码暴力破解攻击检测方法[J]. 西南大学学报:自然科学版, 2017, 39(7): 149-154.
	WeiQin-fang,YangZi-ming,HuXiang-dong,et al.A remote login-focused brute-force attack detection methods based on network flow characteristics[J]. Journal of Southwest University(Natural Science), 2017, 39(7): 149-154.
8	王念平. 四分组类CLEFIA变换簇抵抗差分密码分析的安全性评估[J]. 电子学报, 2017, 45(10):2528-2532.
	WangNian-ping.Security evaluation against differential cryptanalysis for four-block CLEFIA-like transform cluster[J]. Acta Electronica Sinica, 2017, 45(10): 2528-2532.
9	陈美兰, 林继铭, 白伟. 氢气安全分析软件CYCAS的研发及初步验证[J]. 原子能科学技术, 2016, 50(2): 295-300.
	ChenMei-lan, LinJi-ming, BaiWei. Development and preliminary validation of Hydrogen safety analysis code CYCAS[J]. Atomic Energy Science and Technology, 2016, 50(2): 295-300.
10	苏盛, 李志强, 谷科,等. 基于云安全的高级计量体系恶意软件检测方法[J]. 电力系统自动化, 2017, 41(5): 134-138.
	SuSheng, LiZhi-qiang, GuKe, et al. Cloud security based malware detection in advanced metering infrastructure[J]. Automation of Electric Power Systems, 2017, 41(5): 134-138.

相关文章 15

[1]	余宜诚, 胡亮, 迟令, 初剑峰. 一种改进的适用于多服务器架构的匿名认证协议[J]. 吉林大学学报(工学版), 2018, 48(5): 1586-1592.
[2]	董坚峰, 张玉峰, 戴志强. 改进的基于狄利克雷混合模型的推荐算法[J]. 吉林大学学报(工学版), 2018, 48(2): 596-604.
[3]	赵博, 秦贵和, 赵永哲, 杨文迪. 基于半陷门单向函数的公钥密码[J]. 吉林大学学报(工学版), 2018, 48(1): 259-267.
[4]	刘磊, 刘利娟, 吴新维, 张鹏. 基于ECPMR的编译器测试方法[J]. 吉林大学学报(工学版), 2017, 47(4): 1262-1267.
[5]	董立岩, 王越群, 贺嘉楠, 孙铭会, 李永丽. 基于时间衰减的协同过滤推荐算法[J]. 吉林大学学报(工学版), 2017, 47(4): 1268-1272.
[6]	于斌斌, 武欣雨, 初剑峰, 胡亮. 基于群密钥协商的无线传感器网络签名协议[J]. 吉林大学学报(工学版), 2017, 47(3): 924-929.
[7]	邓昌义, 郭锐锋, 张忆文, 王鸿亮. 基于平衡因子的动态偶发任务低功耗调度算法[J]. 吉林大学学报(工学版), 2017, 47(2): 591-600.
[8]	魏晓辉, 刘智亮, 庄园, 李洪亮, 李翔. 支持大规模流数据在线处理的自适应检查点机制[J]. 吉林大学学报(工学版), 2017, 47(1): 199-207.
[9]	郝娉婷, 胡亮, 姜婧妍, 车喜龙. 基于多管理节点的乐观锁协议[J]. 吉林大学学报(工学版), 2017, 47(1): 227-234.
[10]	魏晓辉, 李翔, 李洪亮, 李聪, 庄园, 于洪梅. 支持大规模流数据处理的弹性在线MapReduce模型及拓扑协议[J]. 吉林大学学报(工学版), 2016, 46(4): 1222-1231.
[11]	车翔玖, 梁森. 一种基于大顶堆的SPIHT改进算法[J]. 吉林大学学报(工学版), 2016, 46(3): 865-869.
[12]	董悦丽, 郭权, 孙斌, 康玲. 药物分子对接动态任务迁移优化[J]. 吉林大学学报(工学版), 2015, 45(4): 1253-1259.
[13]	匡哲君，师唯佳，胡亮. 基于无线传感器网络的角色成员关系剩余能量新算法[J]. 吉林大学学报(工学版), 2015, 45(2): 600-605.
[14]	张忆文，郭锐锋. 实时系统混合任务低功耗调度算法[J]. 吉林大学学报(工学版), 2015, 45(1): 261-266.
[15]	张忆文^{1, 2}, 郭锐锋¹. 制的容错节能调度算法[J]. 吉林大学学报(工学版), 2014, 44(4): 1112-1117.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

密码软件缺陷类型	密码软件缺陷个数/个	占总数的百分比/%
严重不安全	20	16.6
不可用	45	37.5
影响计算机运行	35	29.2
安全性降级	10	8.3
存在不安全隐患	5	4.2
其他问题	5	4.2