摘要

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