基于模型检测的TLS协议实现库安全性分析

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

Abstract

Abstract:

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.

Key words: security protocol analysis, transport layer security (TLS), finite state machine, model checking

CLC Number:

TP393.08

Xing BI, Chaojing TANG. Security analysis of TLS protocol implementations based on model checking[J]. Systems Engineering and Electronics, 2021, 43(3): 839-846.

Figures/Tables 6

Fig.1

Fig.2

Table 1

Fig.3

Fig.4

Table 2

References 27

1	RESCORLA E. The transport layer security (TLS) protocol version 1.3[EB/OL].[2020-3-10]. https://tools.ietf.org/html/rfc8446.
2	ALFARDAN N J, PATERSON K G. Lucky thirteen: breaking the TLS and DTLS record protocols[C]//Proc.of the IEEE Symposium on Security and Privacy, 2013: 526-540.
3	YAU A K L, PATERSON K G, MITCHELL C J. Padding oracle attacks on CBC-mode encryption with secret and random IVs[C]//Proc.of the International Workshop on Fast Software Encryption, 2005: 299-319.
4	MÖLLER B, DUONG T, KOTOWICZ K. This POODLE bites: exploiting the SSL 3.0 fallback[EB/OL].[2020-3-10]. https://www.openssl.org/~bodo/ssl-poodle.pdf.
5	CIMATTI A, CLARKE E, GIUNCHIGLIA E, et al. Nusmv 2: an opensource tool for symbolic model checking[C]//Proc.of the International Conference on Computer Aided Verification, 2002: 359-364.
6	BEURDOUCHE B, BHARGAVAN K, DELIGNAT-LAVAUD A, et al. A messy state of the union: taming the composite state machines of TLS[C]//Proc.of the IEEE Symposium on Security and Privacy, 2015: 535-552.
7	BEURDOUCHE B, DELIGNAT-LAVAUD A, KOBEISSI N, et al. FLEXTLS: a tool for testing TLS implementations[C]//Proc.of the 9th USENIX Conference on Offensive Technologies, 2015.
8	申莹珠, 顾纯祥, 陈熹, 等. 基于模型学习的OpenVPN系统脆弱性分析[J]. 软件学报, 2019, 30 (12): 3750- 3764.
	SHEN Y Z , GU C X , CHEN X , et al. Vulnerability analysis of OpenVPN system based on model learning[J]. Journal of Software, 2019, 30 (12): 3750- 3764.
9	申莹珠, 顾纯祥, 陈熹. 基于模型学习的网络安全协议脆弱性分析系统[J]. 信息工程大学学报, 2019, 20 (1): 111- 115.
	SHEN Y Z , GU C X , CHEN X . Network security protocol vulnerability analysis system based on model learning[J]. Journal of Information Engineering University, 2019, 20 (1): 111- 115.
10	TSANKOV P, DASHTI M T, BASIN D. SECFUZZ: fuzz-testing security protocols[C]//Proc.of the 7th International Workshop on Automation of Software Test, 2012.
11	HUSSAIN S, CHOWDHURY O, MEHNAZ S, et al. LTEInspector: a systematic approach for adversarial testing of 4G LTE[C]//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[M]. Machine Learning for Dynamic Software Analysis: Potentials and Limits. Cham: Springer, 2018: 74-100.
13	HSU Y, SHU G, LEE D. A model-based approach to security flaw detection of network protocol implementations[C]//Proc.of the International Conference on Network Protocols, 2008: 114-123.
14	VAN A J, DE R I J E J J, ALPÁR G G. Improving mobile ad hoc networks in realtime situations[D]. Nijmegen: Radboud University, 2018.
15	DANIEL L A, POLL E, DE R J. Inferring OpenVPN state machines using protocol state fuzzing[C]//Proc.of the IEEE 3rd European Symposium on Security and Privacy Workshops, 2018: 11-19.
16	STONE C M, CHOTHIA T, RUITER J D. Extending automated protocol state learning for the 802.11 4-way handshake[C]//Proc.of the European Symposium on Research in Computer Security, 2018: 325-345.
17	SIVAKORN S, ARGYROS G, PEI K, et al. HVLearn: automated black-box analysis of hostname verification in SSL/TLS implementations[C]//Proc.of the Symposium on Security and Privacy, 2017: 521-538.
18	MARALLO G. Identifying software and protocol vulnerabilities in WPA2 implementations through fuzzing[D]. Turin: Polytechnic University of Turin, 2019.
19	BJORNER N , MOURA L D . Satisfiability modulo theories: introduction and applications[J]. Communications of the ACM, 2011, 54 (9): 69- 77. doi: 10.1145/1995376.1995394
20	BORISOV N, BRUMLEY D J, WANG H J, et al. A generic application-level protocol analyzer and its language[C]//Proc.of the 14th Annual Network Distributed System Security Symposium, 2007.
21	HARRIS I G , ALRAHEM T , CHEN A , et al. Security testing of session initiation protocol implementations[J]. The ISC International Journal of Information Security, 2009, 1 (2): 91- 103.
22	NINET T, LEGAY A, MAILLARD R, et al. Model checking the IKEv2 protocol using spin[C]//Proc.of the 17th International Conference on Privacy, Security and Trust, 2019.
23	DRURY J, HÖFNER P, WANG W. Formal models of the OSPF routing protocol[EB/OL].[2020-012-14]. https://arxiv.org/abs/2004.13286.
24	XIE T, WANG S, TU G H, et al. Exploring the insecurity of google account registration protocol via model checking[C]//Proc.of the IEEE Symposium Series on Computational Intelligence, 2019: 3087-3096.
25	ANGLUIN D . Learning regular sets from queries and counterexamples[J]. Information and Computation, 1987, 75 (2): 87- 106. doi: 10.1016/0890-5401(87)90052-6
26	RAFFELT H , STEFFEN B , BERG T , et al. LearnLib: a framework for extrapolating behavioral models[J]. International Journal on Software Tools for Technology Transfer, 2009, 11 (5): 393- 407. doi: 10.1007/s10009-009-0111-8
27	TIAN C , CHEN C , DUAN Z H , et al. Differential testing of certificate validation in SSL/TLS implementations: an RFC-guided approach[J]. ACM Trans.on Software Engineering and Methodology, 2019, 28 (4): 1- 37.

输入输出消息	字母表
客户端握手	ClientHello
客户端证书	ClientCertificate
完成	Finished
客户端密钥交换	KeyEx
新密钥生成	NEWKEYS
更改密码规范	ChangeCipherSpec
异常消息	Unimpl
应用数据	ApplicationData
连接中断	ConnectionClosed
空报文	Empty
无响应	NoRESP
认证成功	SUCCESS
认证失败	FAILURE

属性	待验证属性	关键字	OpenSSL	NSS
安全属性	AuthReq		√	√
安全属性	OpenChannel		√	√
密钥重协商	reAuthReq		×	√
函数属性	属性4	MUST	×	×
	属性5	MUST	√	√
	属性6	MUST	√	√
	属性7	MUST	√	√

[1]	Sen QIAO, Zhiqiu HUANG, Jinyong WANG, Weijian WAN. DFT quantitative analysis method based on statistical model checking [J]. Systems Engineering and Electronics, 2020, 42(2): 480-488.
[2]	CHEN Lu, JIAO Jian, WEI Qianxin. Model-checking oriented unified modeling method based on NuSMV [J]. Systems Engineering and Electronics, 2018, 40(7): 1654-1659.
[3]	BI Xing, TANG Chaojing. Security analysis of TLS implementations based on state machine learning algorithm [J]. Systems Engineering and Electronics, 2018, 40(12): 2810-2815.
[4]	WANG Peng, ZHANG Fan, DONG Lei, HU Jianbo, ZHAO Changxiao. Translation rules of fault extended model to probabilistic checking model [J]. Systems Engineering and Electronics, 2017, 39(11): 2501-2508.
[5]	NING Ning, ZHANG Jun, GAO Xiang-yang, XUE Jing. Formal verification of SDG diagnosability via symbolic model checking [J]. Journal of Systems Engineering and Electronics, 2011, 33(2): 390-394.
[6]	LI Zhen, LIU Bin, LI Xiao-xun, YIN Yong-feng. Verification of safetycritical software requirement based on Petri-net model checking [J]. Journal of Systems Engineering and Electronics, 2011, 33(2): 458-463.
[7]	YAO Li-hong, LI Jun-min. Design of impulsive hybrid controllers for a class of nonlinear hybrid systems [J]. Journal of Systems Engineering and Electronics, 2010, 32(8): 1732-1736.

Security analysis of TLS protocol implementations based on model checking

RichHTML

PDF (PC)

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 6

References 27

Related Articles 7

Recommended Articles

Metrics

Comments