基于Hoare逻辑的密码软件安全性形式化验证方法
|
摘要
为了解决密码软件安全性验证效率和准确率低的问题,提出了基于Hoare逻辑的密码软件安全性形式化验证方法。首先对密码软件的主要性质进行描述,然后通过密码软件运行时随机向量的分析,得到密码软件运行的矩阵表达式,再将其进行线性变换,计算密码软件运行时数据的方差和协方差矩阵,获得密码软件运行时数据矩阵的主成分空间,并对密码软件运行的主成分进行分析;最后,利用密码软件的逻辑模型和软件运行的状态集合对密码软件安全形式化验证的流程进行分析,建立密码软件的运行模型并设置安全属性,并将密码软件运行时出现的故障进行标记和处理,得到密码软件运行的安全结果,从而实现密码软件安全性形式化的验证。实验结果表明,采用该方法对密码软件的安全性进行验证具有较高的效率,且能够准确地验证密码软件的安全。
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.
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.
引文
[1]李耀,郭进,杨扬,等.铁路信号安全关键软件形式化建模[J].铁道学报,2017,39(9):74-80.Li Yao,Guo Jin,Yang Yang,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.Lyu Ying-jie,Xu Wen-jing,Liu Ying,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.Yang Fan,Yang Guo-wu,Hao Yu-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.Huan Zi-qiang,Ni Hong,Hu Lin-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.Chen Hao,Qing Si-han.Android malware detection method based on combined algorithm[J].Telecommunications Science,2016,32(10):15-21.
[6]贾乐,高杨,王宇航.固态热机械密码鉴别器的安全性增强方法[J].探测与控制学报,2017,39(3):92-96.Jia Le,Gao Yang,Wang Yu-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.Wei Qin-fang,Yang Zi-ming,Hu Xiang-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.Wang Nian-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.Chen Mei-lan,Lin Ji-ming,Bai Wei.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.Su Sheng,Li Zhi-qiang,Gu Ke,et al.Cloud security based malware detection in advanced metering infrastructure[J].Automation of Electric Power Systems,2017,41(5):134-138.
[2]吕英杰,徐文静,刘鹰,等.基于密码技术的智能电能表软件备案与比对系统设计[J].电网技术,2016,40(11):3604-3608.Lyu Ying-jie,Xu Wen-jing,Liu Ying,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.Yang Fan,Yang Guo-wu,Hao Yu-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.Huan Zi-qiang,Ni Hong,Hu Lin-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.Chen Hao,Qing Si-han.Android malware detection method based on combined algorithm[J].Telecommunications Science,2016,32(10):15-21.
[6]贾乐,高杨,王宇航.固态热机械密码鉴别器的安全性增强方法[J].探测与控制学报,2017,39(3):92-96.Jia Le,Gao Yang,Wang Yu-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.Wei Qin-fang,Yang Zi-ming,Hu Xiang-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.Wang Nian-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.Chen Mei-lan,Lin Ji-ming,Bai Wei.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.Su Sheng,Li Zhi-qiang,Gu Ke,et al.Cloud security based malware detection in advanced metering infrastructure[J].Automation of Electric Power Systems,2017,41(5):134-138.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |