Journal of Jilin University(Engineering and Technology Edition) ›› 2019, Vol. 49 ›› Issue (4): 1301-1306.doi: 10.13229/j.cnki.jdxbgxb20180418

Previous Articles    

Formal verification method for cryptographic software security based on Hoare logic

Kun XIAO()   

  1. School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu 611731, China
  • Received:2018-05-01 Online:2019-07-01 Published:2019-07-16

RICH HTML

 4   

PDF (PC)

178

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

CLC Number: 

  • TP393

Fig.1

Formal verification flow chart of cryptography software security"

Table 1

Analysis of the degree of defect in"

密码软件

缺陷类型

密码软件缺陷个数/个占总数的百分比/%
严重不安全2016.6
不可用4537.5
影响计算机运行3529.2
安全性降级108.3
存在不安全隐患54.2
其他问题54.2

Fig.2

Cryptographic software security verification results accuracy rate comparison"

Fig.3

Efficiency of cryptography software security verification under the proposed method"

Fig.4

Cryptographic software security verification efficiency in reference[5]"

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.
[1] JIN Shun-fu,WANG Bao-shuai,HAO Shan-shan,JIA Xiao-guang,HUO Zhan-qiang. Synchronous sleeping based energy saving strategy of reservation virtual machines in cloud data centers and its performance research [J]. Journal of Jilin University(Engineering and Technology Edition), 2018, 48(6): 1859-1866.
[2] ZHAO Dong,SUN Ming-yu,ZHU Jin-long,YU Fan-hua,LIU Guang-jie,CHEN Hui-ling. Improved moth-flame optimization method based on combination of particle swarm optimization and simplex method [J]. Journal of Jilin University(Engineering and Technology Edition), 2018, 48(6): 1867-1872.
[3] HUANG Hui, FENG Xi-an, WEI Yan, XU Chi, CHEN Hui-ling. An intelligent system based on enhanced kernel extreme learning machine for choosing the second major [J]. 吉林大学学报(工学版), 2018, 48(4): 1224-1230.
[4] FU Wen-bo, ZHANG Jie, CHEN Yong-le. Network topology discovery algorithm against routing spoofing attack in Internet of things [J]. 吉林大学学报(工学版), 2018, 48(4): 1231-1236.
[5] ZHANG Wei-wei, HE Jia-feng, GAO Guo-wang, REN Li-li, SHEN Xuan-jing. Wireless Mesh network routing and channel allocation union optimization algorithm based on game theory [J]. 吉林大学学报(工学版), 2018, 48(3): 887-892.
[6] CAI Zhen-nao, LYU Xin-en, CHEN Hui-ling. Prediction model of somatization disorder based on an oppositional bacterial foraging optimization based support vector machine [J]. 吉林大学学报(工学版), 2018, 48(3): 936-942.
[7] HAN Jia-wei, LIU Yan-heng, SUN Xin, SONG Li-jun. Identity-based encryption scheme based on cloud and quantum keys [J]. 吉林大学学报(工学版), 2018, 48(2): 551-557.
[8] DONG Jian-feng, ZHANG Yu-feng, DAI Zhi-qiang. Improved recommendation algorithm based on DPM model [J]. 吉林大学学报(工学版), 2018, 48(2): 596-604.
[9] ZHANG Wei-wei, HE Jia-feng, GAO Guo-wang, REN Li-li, SHEN Xuan-jing. Routing and channel allocation union optimization in hybrid wireless mesh network [J]. 吉林大学学报(工学版), 2018, 48(1): 268-273.
[10] SHI Wen-xiao, SUN Hao-ran, WANG Shao-bo. Joint channel allocation and routing algorithm in wireless mesh network [J]. 吉林大学学报(工学版), 2017, 47(6): 1918-1925.
[11] LIU Lei, LIU Li-juan, WU Xin-wei, ZHANG Peng. Compiler testing method based on ECP metamorphic relation [J]. 吉林大学学报(工学版), 2017, 47(4): 1262-1267.
[12] DONG Li-yan, WANG Yue-qun, HE Jia-nan, SUN Ming-hui, LI Yong-li. Collaborative filtering recommendation algorithm based on time decay [J]. 吉林大学学报(工学版), 2017, 47(4): 1268-1272.
[13] YU Bin-bin, WU Xin-yu, CHU Jian-feng, HU Liang. Signature protocol for wireless sensor network based on group key agreement [J]. 吉林大学学报(工学版), 2017, 47(3): 924-929.
[14] ZHAO Dong, ZANG Xue-bai, ZHAO Hong-wei. Random forest prediction method based on optimization of fruit fly [J]. 吉林大学学报(工学版), 2017, 47(2): 609-614.
[15] DONG Ying, ZHOU Zhan-ying, SU Zhen-zhen, XU Yang, QIAN Zhi-hong. Cross-layer MAC protocol based on routing information for WSN [J]. 吉林大学学报(工学版), 2017, 47(2): 647-654.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
Copyright © Journal of Jilin University(Engineering and Technology Edition), All Rights Reserved.
Tel: +86-431-85095297　Fax: +86-431-85094074　E-mail: xbgxb@jlu.edu.cn
Powered by Beijing Magtech Co. Ltd