Security analysis of TLS protocol implementations based on model checking

被引：0

作者：

Bi X. ^{[1
]}

Tang C. ^{[2
]}

机构：

[1] College of Advanced Interdisciplinary Studies, National University of Defense Technology, Changsha

[2] College of Electronic Science and Technology, National University of Defense Technology, Changsha

来源：

Xi Tong Gong Cheng Yu Dian Zi Ji Shu/Systems Engineering and Electronics | 2021年 / 43卷 / 03期

关键词：

Finite state machine; Model checking; Security protocol analysis; Transport layer security (TLS);

D O I：

10.12305/j.issn.1001-506X.2021.03.30

中图分类号：

学科分类号：

摘要：

In view of the problem that the traditional fuzzy testing method can find the memory vulnerability of the transport layer security (TLS) protocol implementation, but it can not find the logic loophole, based on the method of model detection, the state machine model of TLS protocol implementation is extracted, establishes the protocol security attribute model is establised, the possible abnormal behavior in the protocol implementation is looked, and the automation and system analysis of the protocol implementation is realized. The security attribute of the state machine for the protocol implementation generated by test cases is modeled, and the extracted model is checked by using the NuSMV tool. The experiment results show that the proposed method can effectively analyze the state machine model of TLS protocol implementation, and find the logic loopholes and the defects inconsistent with the specification. © 2021, Editorial Office of Systems Engineering and Electronics. All right reserved.

引用

页码：839 / 846

页数：7

共 27 条

[11]

HUSSAIN S, CHOWDHURY O, MEHNAZ S, Et al., LTEInspector: a systematic approach for adversarial testing of 4G LTE, Proc. of the Network and Distributed Systems Security Symposium, (2018)

[12]

AICHERNIG B K, MOSTOWSKI W, MOUSAVI M R, Et al., Model learning and model-based testing, Machine Learning for Dynamic Software Analysis: Potentials and Limits, pp. 74-100, (2018)

[13]

HSU Y, SHU G, LEE D., A model-based approach to security flaw detection of network protocol implementations, Proc. of the International Conference on Network Protocols, pp. 114-123, (2008)

[14]

VAN A J, DE R I J E J J, ALPAR G G., Improving mobile ad hoc networks in realtime situations, (2018)

[15]

DANIEL L A, POLL E, DE R J., Inferring OpenVPN state machines using protocol state fuzzing, Proc. of the IEEE 3rd European Symposium on Security and Privacy Workshops, pp. 11-19, (2018)

[16]

STONE C M, CHOTHIA T, RUITER J D., Extending automated protocol state learning for the 802. 11 4-way handshake, Proc. of the European Symposium on Research in Computer Security, pp. 325-345, (2018)

[17]

SIVAKORN S, ARGYROS G, PEI K, Et al., HVLearn: automated black-box analysis of hostname verification in SSL/TLS implementations, Proc. of the Symposium on Security and Privacy, pp. 521-538, (2017)

[18]

MARALLO G., Identifying software and protocol vulnerabilities in WPA2 implementations through fuzzing, (2019)

[19]

BJORNER N, MOURA L D., Satisfiability modulo theories: introduction and applications, Communications of the ACM, 54, 9, pp. 69-77, (2011)

[20]

BORISOV N, BRUMLEY D J, WANG H J, Et al., A generic application-level protocol analyzer and its language, Proc. of the 14th Annual Network Distributed System Security Symposium, (2007)

← 1 2 3 →