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

作者：毕兴; 唐朝京

来源：系统工程与电子技术, 2020, 1-9.

• 安全协议分析
• TLS
• 有限状态机
• 模型检测 security protocol analysis
• finite state machine
• model checking

安全传输层协议(transport layer security,TLS)作为当前主流的安全协议，对互联网安全至关。TLS协议的实现库作为TLS协议的应用载体，是协议规范与代码实现的结合点，许多规范层已经证明安全的协议，其实现库仍被发现存在漏洞，然而传统的模糊测试方法大多用于发现协议实现库的内存漏洞，而无法找到其中的逻辑漏洞。本文基于模型检测的方法，通过对协议实现库的有限状态机提取，提取TLS协议实现库的状态机模型，建立协议安全属性模型，寻找协议实现中可能存在的异常行为，实现对协议实现库的自动化和系统化的分析。本文对利用测试用例生成的协议实现库状态机进行安全属性建模，利用NuSMV工具，对提取...

• 单位
  国防科学技术大学