系统工程与电子技术 ›› 2021, Vol. 43 ›› Issue (3): 839-846.doi: 10.12305/j.issn.1001-506X.2021.03.30

• 通信与网络 • 上一篇    下一篇

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

毕兴1(), 唐朝京2()   

  1. 1. 国防科技大学前沿交叉学科学院, 湖南 长沙 410073
    2. 国防科技大学电子科学学院, 湖南 长沙 410073
  • 收稿日期:2020-03-18 出版日期:2021-03-01 发布日期:2021-03-16
  • 作者简介:毕兴(1989-), 男, 研究实习员, 硕士, 主要研究方向为通信网信息安全、协议分析。E-mail:xing_bi@hotmail.com|唐朝京(1962-), 男, 教授, 博士, 主要研究方向为信息安全、软件漏洞分析和电磁防护。E-mail:cjtang@nudt.edu.cn

Security analysis of TLS protocol implementations based on model checking

Xing BI1(), Chaojing TANG2()   

  1. 1. College of Advanced Interdisciplinary Studies, National University of Defense Technology, Changsha 410073, China
    2. College of Electronic Science and Technology, National University of Defense Technology, Changsha 410073, China
  • Received:2020-03-18 Online:2021-03-01 Published:2021-03-16

摘要:

针对传统模糊测试方法虽能发现传输层安全性(transport layer security, TLS)协议实现库内存漏洞, 但无法找到其中逻辑漏洞的问题,基于模型检测的方法, 提取TLS协议实现库的状态机模型, 建立协议安全属性模型, 寻找协议实现中可能存在的异常行为, 实现对协议实现库的自动化和系统化的分析。对利用测试用例生成的协议实现库状态机进行安全属性建模, 利用NuSMV工具, 对提取的模型进行模型检测。实验结果证明所提方法能够有效分析TLS协议实现库的状态机模型, 找到协议实现库存在的逻辑漏洞及与规范不一致的缺陷。

关键词: 安全协议分析, 传输层安全性, 有限状态机, 模型检测

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

中图分类号: