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

Security analysis of TLS protocol implementations based on model checking

作　　者：毕兴 唐朝京[2] BI Xing;TANG Chaojing(College of Advanced Interdisciplinary Studies, National University of Defense Technology, Changsha 410073, China;College of Electronic Science and Technology, National University of Defense Technology, Changsha 410073, China)

机构地区：[1]国防科技大学前沿交叉学科学院,湖南长沙410073 [2]国防科技大学电子科学学院,湖南长沙410073

出　　处：《系统工程与电子技术》2021年第3期839-846,共8页Systems Engineering and Electronics

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

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

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]