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

来源：系统工程与电子技术杂志2021年第3期北京时间：

作者：毕兴, 唐朝京

单位：1. 国防科技大学前沿交叉学科学院, 湖南 长沙 410073；2. 国防科技大学电子科学学院, 湖南 长沙 410073

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

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