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

针对传统模糊测试方法虽能发现传输层安全性(transport layer security,TLS)协议实现库内存漏洞,但无法找到其中逻辑漏洞的问题,基于模型检测的方法,提取TLS协议实现库的状态机模型,建立协议安全属性模型,寻找协议实现中可能存在的异常行为,实现对协议实现库的自动化和系统化的分析.对利用测试用例生成的...

Security analysis of TLS protocol implementations based on model checking

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.