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!
|
| Summary: | 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. |
|---|---|
| ISSN: | 2096-109X |