摘要
为了解决密码软件安全性验证效率和准确率低的问题,提出了基于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.
作者
肖堃
XIAO Kun(School of Computer Science and Engineering,University of Electronic Science and Technology of China,Chengdu 611731,China)
出处
《吉林大学学报（工学版）》
EI
CAS
CSCD
北大核心
2019年第4期1301-1306,共6页
Journal of Jilin University:Engineering and Technology Edition
基金
国家科技重大专项项目(2014ZX03002001)
关键词
计算机系统结构
霍尔逻辑
密码软件
安全性验证
computer systems architecture
Hoare logic
cipher software
safety verification
