Formal verification method for cryptographic software security based on Hoare logic

被引：0

作者：

Xiao K. ^{[1
]}

机构：

[1] School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu

来源：

Jilin Daxue Xuebao (Gongxueban)/Journal of Jilin University (Engineering and Technology Edition) | 2019年 / 49卷 / 04期

关键词：

Cipher software; Computer systems architecture; Hoare logic; Safety verification;

D O I：

10.13229/j.cnki.jdxbgxb20180418

中图分类号：

学科分类号：

摘要：

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. © 2019, Jilin University Press. All right reserved.

引用

页码：1301 / 1306

页数：5

共 10 条

[1] Li Y., Guo J., Yang Y., Et al., Formal modeling of railway signal safety critical software, Journal of the China Railway Society, 39, 9, pp. 74-80, (2017)
[2] Lyu Y.-J., Xu W.-J., Liu Y., Et al., Design of intelligent watt-hour meter software recording and comparing system based on cryptography, Power System Technology, 40, 11, pp. 3604-3608, (2016)
[3] Yang F., Yang G.-W., Hao Y.-J., Security analysis of semi-quantum cryptography protocols by model checking, Journal of University of Electronic Science and Technology of China, 46, 5, pp. 716-721, (2017)
[4] Huan Z.-Q., Ni H., Hu L.-L., Et al., Application security detection based on Android access permission mechanism, Computer Engineering and Design, 37, 1, pp. 42-45, (2016)
[5] Chen H., Qing S.-H., Android malware detection method based on combined algorithm, Telecommunications Science, 32, 10, pp. 15-21, (2016)
[6] Jia L., Gao Y., Wang Y.-H., Safety enhancement method for solid state thermal mechanical discriminator, Journal of Detection & Control, 39, 3, pp. 92-96, (2017)
[7] Wei Q.-F., Yang Z.-M., Hu X.-D., Et al., A remote login-focused brute-force attack detection methods based on network flow characteristics, Journal of Southwest University(Natural Science), 39, 7, pp. 149-154, (2017)
[8] Wang N.-P., Security evaluation against differential cryptanalysis for four-block CLEFIA-like transform cluster, Acta Electronica Sinica, 45, 10, pp. 2528-2532, (2017)
[9] Chen M.-L., Lin J.-M., Bai W., Development and preliminary validation of Hydrogen safety analysis code CYCAS, Atomic Energy Science and Technology, 50, 2, pp. 295-300, (2016)
[10] Su S., Li Z.-Q., Gu K., Et al., Cloud security based malware detection in advanced metering infrastructure, Automation of Electric Power Systems, 41, 5, pp. 134-138, (2017)

← 1 →