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

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

doi:10.11959/j.issn.2096-109x.2021067

您当前的位置：

首页 >

文章列表页 >

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

专栏Ⅱ：机器学习及安全应用 | 更新时间：2024-06-03

- 模型学习与符号执行结合的安全协议代码分析技术
- Security protocol code analysis method combining model learning and symbolic execution
- 网络与信息安全学报 2021年7卷第5期页码：93-104
- 作者机构：
  
  1. 数学工程与先进计算国家重点实验室，河南郑州 450001
  2. 网络密码技术河南省重点实验室，河南郑州 450002
- 作者简介：
  
  [ "张协力（1992− ），男，陕西兴平人，数学工程与先进计算国家重点实验室博士生，主要研究方向为网络安全协议" ]
  [ "祝跃飞（1962− ），男，浙江兰溪人，博士，数学工程与先进计算国家重点实验室教授、博士生导师，主要研究方向为网络安全、密码学" ]
  [ "顾纯祥（1976− ），男，安徽霍山人，博士，数学工程与先进计算国家重点实验室教授，主要研究方向为网络安全、密码学" ]
  [ "陈熹（1988− ），男，湖北建始人，硕士，数学工程与先进计算国家重点实验室讲师，主要研究方向为网络安全、密码学" ]
- 基金信息：
  
  国家重点研发计划;The National Key R＆D Program of China(2019QY1302)
- DOI：10.11959/j.issn.2096-109x.2021067
  中图分类号： TP311
- 网络首发：2021-10，
  
  纸质出版：2021-10-15
- 稿件说明：
移动端阅览
张协力, 祝跃飞, 顾纯祥, 等. 模型学习与符号执行结合的安全协议代码分析技术[J]. 网络与信息安全学报, 2021,7(5):93-104.

Xieli ZHANG, Yuefei ZHU, Chunxiang GU, et al. Security protocol code analysis method combining model learning and symbolic execution[J]. Chinese Journal of Network and Information Security, 2021, 7(5): 93-104.
张协力, 祝跃飞, 顾纯祥, 等. 模型学习与符号执行结合的安全协议代码分析技术[J]. 网络与信息安全学报, 2021,7(5):93-104. DOI： 10.11959/j.issn.2096-109x.2021067.

Xieli ZHANG, Yuefei ZHU, Chunxiang GU, et al. Security protocol code analysis method combining model learning and symbolic execution[J]. Chinese Journal of Network and Information Security, 2021, 7(5): 93-104. DOI： 10.11959/j.issn.2096-109x.2021067.

摘要

符号执行技术从理论上可以全面分析程序执行空间，但对安全协议这样的大型程序，路径空间爆炸和约束求解困难的局限性导致其在实践上不可行。结合安全协议程序自身特点，提出用模型学习得到的协议状态机信息指导安全协议代码符号执行思路；同时，通过将协议代码中的密码学逻辑与协议交互逻辑相分离，避免了因密码逻辑的复杂性导致路径约束无法求解的问题。在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.

关键词

Keywords

references

FITERĂU-BROŞTEAN P , . Model learning and model checking of SSH implementations [C ] // Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software . 2017 .

ANGLUIN D . Learning regular sets from queries and counterexamples [J ] . Information and Computation , 1987 , 75 ( 2 ): 87 - 106 .

GUO J , GU C , CHEN X , et al . Model learning and model checking of IPSec implementations for internet of things [J ] . IEEE Access , 2019 , 7 : 171322 - 171332 .

FITERAU-BROSTEAN P , JONSSON B , MERGET R , et al . Analysis of DTLS implementations using protocol state fuzzing [C ] // 29th {USENIX} Security Symposium ({USENIX} Security 20) . 2020 : 2523 - 2540 .

CHAU S Y , CHOWDHURY O , HOQUE E , et al . Symcerts:practical symbolic execution for exposing noncompliance in X.509 certificate validation implementations [C ] // 2017 IEEE Symposium on Security and Privacy (SP) . 2017 : 503 - 520 .

CORIN R , MANZANO F A . Efficient symbolic execution for analysing cryptographic protocol implementations [C ] // International Symposium on Engineering Secure Software and Systems . 2011 : 58 - 72 .

VANHOEF M , PIESSENS F . Symbolic execution of security protocol implementations:handling cryptographic primitives [C ] // 12th{USENIX} Workshop on Offensive Technologies ({WOOT} 18) . 2018 .

CHAU S Y , YAHYAZADEH M , CHOWDHURY O , et al . Analyzing semantic correctness with symbolic execution:a case study on pkcs# 1 v1.5 signature verification [C ] // Network and Distributed Systems Security (NDSS) Symposium 2019 . 2019 .

孟博 , 鲁金钿 , 王德军 , 等 . 安全协议实施安全性分析综述 [J ] . 山东大学学报:理学版 , 2018 , 53 ( 1 ): 1 - 18 .

MENG B , LU J T , WANG D J , et al . Survey of security analysis of security protocol implementations [J ] . Journal of Shandong University (Natural Science) , 2018 , 53 ( 1 ): 1 - 18 .

AICHERNIG B K , MOSTOWSKI W , MOUSAVI M R , et al . Model learning and model-based testing [M ] . Machine Learning for Dynamic Software Analysis : Potentials and Limits . 2018 : 74 - 100 .

JERO S , HOQUE M E , CHOFFNES D R , et al . Automated attack discovery in TCP congestion control using a model-guided approach [C ] // NDSS . 2018 .

JERO S , LEE H , NITA-ROTARU C , . Leveraging state information for automated attack discovery in transport protocol implementations [C ] // 2015 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks . 2015 : 1 - 12 .

WALLS R J , BRUN Y , LIBERATORE M , et al . Discovering specification violations in networked software systems [C ] // 2015 IEEE 26th International Symposium on Software Reliability Engineering (ISSRE) . 2015 : 496 - 506 .

SONG J S , CADAR C , PIETZUCH P . SymbexNet:testing network protocol implementations with symbolic execution and rule-based specifications [J ] . IEEE Transactions on Software Engineering , 2014 , 40 ( 7 ): 695 - 709 .

ALSHMRANY K , CORDEIRO L . Finding security vulnerabilities in network protocol implementations [J ] . arXiv preprint arXiv:2001.09592 , 2020 .

谢肖飞 , 李晓红 , 陈翔 , 等 . 基于符号执行与模糊测试的混合测试方法 [J ] . 软件学报 , 2019 , 30 ( 10 ): 3071 - 3089 .

XIE X F , LI X H , CHEN X , et al . Hybrid testing based on symbolic execution and fuzzing [J ] . Journal of Software , 2019 , 30 ( 10 ): 3071 - 3089 .

CHO C Y , BABIC D , POOSANKAM P , et al . MACE:model-inference-assisted concolic exploration for protocol and vulnerability discovery [C ] // USENIX Security Symposium . 2011 :139.

YLONEN T , LONVICK C . The secure shell (SSH) protocol architecture [S ] . RFC4251,Internet Engineering Task Force , 2006 .

浏览量

576

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于符号执行和N-scope复杂度的代码混淆度量方法

分支混淆中的条件异常代码构造研究

基于函数语义分析的软件补丁比对技术

基于符号执行的Android原生代码控制流图提取方法