毕 兴,唐朝京

(国防科技大学电子科学学院,湖南 长沙 410073)

0 引 言

传输层安全(transport layer security,TLS)协议用于为网络提供安全及数据完整性保障。作为最广泛使用的安全协议之一,其安全性引起了业界的高度关注,各类研究者及攻击者对其进行了细致深入的分析,它经历了从密码学攻击[1-3]到协议实现库漏洞[4-6]等一系列安全威胁。其中TLS协议实现库作为TLS协议的应用载体,也被看作一个实施网络攻击的重点。因此,对其安全性的分析,有着重大而现实的意义。

传统的TLS协议实现库安全性分析大多立足于程序分析的角度,重在寻找实现库的软件脆弱性,该方法无法发现协议实现中存在的逻辑缺陷。另一方面,通过对协议规范的形式化安全分析又不足以保证其实现库的安全性。

为了描述TLS或一般安全协议的实现库,可以使用有限状态机指定发送和接收的消息的可能序列。使用状态机学习技术,能够仅依赖于黑盒测试,不需要知道协议规范,就可以从协议实现库中提取状态机。通过分析这些状态机,可以发现协议的状态迁移中存在的逻辑错误。

协议状态机学习可以分为被动式学习和主动式学习。文献[7]提出了第一个多项式复杂度的摩尔状态机学习算法,称作L*算法。它是最经典的状态机学习算法,用来推断最小化的确定的有限状态机。被动式学习技术通过观测网络中的流量来推断协议的状态机,文献[8]通过被动学习的模型对网络进行了模糊测试。文献[9]通过状态机模型形式化分析了银行卡的安全性。……