模型学习与符号执行结合的安全协议代码分析技术

张协力，祝跃飞，顾纯祥，陈熹

模型学习与符号执行结合的安全协议代码分析技术

张协力1,2，祝跃飞1,2，顾纯祥1,2，陈熹1,2

（1. 数学工程与先进计算国家重点实验室，河南 郑州 450001；2. 网络密码技术河南省重点实验室，河南 郑州 450002）

符号执行技术从理论上可以全面分析程序执行空间，但对安全协议这样的大型程序，路径空间爆炸和约束求解困难的局限性导致其在实践上不可行。结合安全协议程序自身特点，提出用模型学习得到的协议状态机信息指导安全协议代码符号执行思路；同时，通过将协议代码中的密码学逻辑与协议交互逻辑相分离，避免了因密码逻辑的复杂性导致路径约束无法求解的问题。在SSH协议开源项目Dropbear上的成功实践表明了所提方法的可行性；通过与Dropbear自带的模糊测试套件对比，验证了所提方法在代码覆盖率与错误点发现上均具有一定优势。

模型学习；符号执行；安全协议代码；状态驱动

1 引言

安全协议在理论设计和代码实现中都极易出错。针对协议规范的形式化验证方法由于忽略了协议实现细节，无法保证协议实现的安全。而安全协议较大的代码规模和复杂的交互逻辑让协议代码安全审计变得更加困难。研究新的技术和方法来辅助安全协议代码检测是一项挑战性工作。

模型学习和模糊测试两种技术在安全协议程序分析方面取得了许多有价值的研究成果。Paul等[1]通过MAT[2]（minimally adequate teacher）模型学习框架推断得到协议程序状态机信息，然后用模型检测器检测协议程序状态机模型中是否存在与协议规范要求不一致的路径。……