Security protocol code analysis method combining model learning and symbolic execution

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

• model learning
• symbolic execution
• security protocol code
• state-driver