网络与信息安全学报 ›› 2021, Vol. 7 ›› Issue (5): 93-104.doi: 10.11959/j.issn.2096-109x.2021067

• 专栏Ⅱ:机器学习及安全应用 • 上一篇    下一篇

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

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

  1. 1 数学工程与先进计算国家重点实验室,河南 郑州 450001
    2 网络密码技术河南省重点实验室,河南 郑州 450002
  • 修回日期:2021-03-29 出版日期:2021-10-15 发布日期:2021-10-01
  • 作者简介:张协力(1992− ),男,陕西兴平人,数学工程与先进计算国家重点实验室博士生,主要研究方向为网络安全协议
    祝跃飞(1962− ),男,浙江兰溪人,博士,数学工程与先进计算国家重点实验室教授、博士生导师,主要研究方向为网络安全、密码学
    顾纯祥(1976− ),男,安徽霍山人,博士,数学工程与先进计算国家重点实验室教授,主要研究方向为网络安全、密码学
    陈熹(1988− ),男,湖北建始人,硕士,数学工程与先进计算国家重点实验室讲师,主要研究方向为网络安全、密码学
  • 基金资助:
    国家重点研发计划(2019QY1302)

Security protocol code analysis method combining model learning and symbolic execution

Xieli ZHANG1,2, Yuefei ZHU1,2, Chunxiang GU1,2, Xi CHEN1,2   

  1. 1 State Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou 450001, China
    2 Henan Key Laboratory of Network Cryptography Technology, Zhengzhou 450002, China
  • Revised:2021-03-29 Online:2021-10-15 Published:2021-10-01
  • Supported by:
    TheNational Key R&D Program of China(2019QY1302)

摘要:

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

关键词: 模型学习, 符号执行, 安全协议代码, 状态驱动

Abstract:

Symbolic execution can comprehensively analyze program execution space in theory, but it is not feasible in practice for large programs like security protocols, due to the explosion of path space and the limitation of difficulty in solving path constraints.According to the characteristics of security protocol program, a method to guide the symbolic execution of security protocol code by using protocol state machine information obtained from model learning was proposed.At the same time, by separating cryptographic logic from protocol interaction logic, the problem that path constraints cannot be solved caused by the complexity of cryptographic logic is avoided.The feasibility of the method is demonstrated by the practice on the SSH open source project Dropbear.Compared with Dropbear's test suite, the proposed method has advantages in code coverage and error point discovery.

Key words: model learning, symbolic execution, security protocol code, state-driver

中图分类号: 

No Suggested Reading articles found!