Security protocol code analysis method combining model learning and symbolic execution
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 securit...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
POSTS&TELECOM PRESS Co., LTD
2021-10-01
|
| Series: | 网络与信息安全学报 |
| Subjects: | |
| Online Access: | http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2096-109x.2021067 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841529805395197952 |
|---|---|
| author | Xieli ZHANG Yuefei ZHU Chunxiang GU Xi CHEN |
| author_facet | Xieli ZHANG Yuefei ZHU Chunxiang GU Xi CHEN |
| author_sort | Xieli ZHANG |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-8bf41f354ab9434d886f029ec356fcbd |
| institution | Kabale University |
| issn | 2096-109X |
| language | English |
| publishDate | 2021-10-01 |
| publisher | POSTS&TELECOM PRESS Co., LTD |
| record_format | Article |
| series | 网络与信息安全学报 |
| spelling | doaj-art-8bf41f354ab9434d886f029ec356fcbd2025-01-15T03:15:14ZengPOSTS&TELECOM PRESS Co., LTD网络与信息安全学报2096-109X2021-10-0179310459568829Security protocol code analysis method combining model learning and symbolic executionXieli ZHANGYuefei ZHUChunxiang GUXi CHENSymbolic 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.http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2096-109x.2021067model learningsymbolic executionsecurity protocol codestate-driver |
| spellingShingle | Xieli ZHANG Yuefei ZHU Chunxiang GU Xi CHEN Security protocol code analysis method combining model learning and symbolic execution 网络与信息安全学报 model learning symbolic execution security protocol code state-driver |
| title | Security protocol code analysis method combining model learning and symbolic execution |
| title_full | Security protocol code analysis method combining model learning and symbolic execution |
| title_fullStr | Security protocol code analysis method combining model learning and symbolic execution |
| title_full_unstemmed | Security protocol code analysis method combining model learning and symbolic execution |
| title_short | Security protocol code analysis method combining model learning and symbolic execution |
| title_sort | security protocol code analysis method combining model learning and symbolic execution |
| topic | model learning symbolic execution security protocol code state-driver |
| url | http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2096-109x.2021067 |
| work_keys_str_mv | AT xielizhang securityprotocolcodeanalysismethodcombiningmodellearningandsymbolicexecution AT yuefeizhu securityprotocolcodeanalysismethodcombiningmodellearningandsymbolicexecution AT chunxianggu securityprotocolcodeanalysismethodcombiningmodellearningandsymbolicexecution AT xichen securityprotocolcodeanalysismethodcombiningmodellearningandsymbolicexecution |