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

作者：肖堃

来源：吉林大学学报（工学版）, 2019, 49(04): 1301-1306.

DOI：10.13229/j.cnki.jdxbgxb20180418

• 计算机系统结构
• 霍尔逻辑
• 密码软件
• 安全性验证

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

• 单位
  电子科技大学