Security protocol code vulnerability mining method based on state machine consistency detection

Abstract

The invention relates to a security protocol code vulnerability mining method based on state machine consistency detection, and belongs to the technical field of information security, and the method comprises the steps: carrying out the interaction with a device carrying a target security protocol in a mode of transmitting a test case, and deducing a state machine model of the security protocol through a learning machine; translating the state machine model into a formalized model, comparing the formalized model with a set formalized verification criterion, searching for the situation that theformalized model is inconsistent with the criterion in the state machine model, and giving out a counter example for debugging personnel to refer to. According to the method, a formal verification means is utilized to automatically detect the compliance condition of the protocol state machine, the conventional manual screening is fundamentally replaced, the analysis efficiency of the protocol state machine is improved, the accuracy is high, false detection is not likely to happen, the professional requirement of debugging personnel is lowered, the universality of the analysis method is enhanced, and even problems which are difficult to find by manual analysis can be found.

Description

technical field [0001] The invention belongs to the technical field of information security, and in particular relates to a security protocol code vulnerability mining method based on state machine consistency detection. Background technique [0002] In recent years, with the continuous development of global informatization, a large number of network security protocols have been applied to secure and confidential communications, aiming to provide secure communication guarantees for people's production and life. The information security situation is becoming more and more serious, and the vulnerability analysis of network security protocols has become a hot spot in the field of information security. At present, among many network security problems, some loopholes are caused by incorrect implementation of relevant protocol specifications, such as OpenSSL Early CCS loopholes, OpenSSH user enumeration loopholes, etc. These subtle logic loopholes are often difficult to find, but ...

AI Technical Summary

Problems solved by technology

[0009] The purpose of this invention is to provide a security protocol code vulnerability mining method based on state machine consistency detection, which is used to solve the problem of low efficiency and error proneness of existing methods. Detection and problems requiring high professionalism of debuggers

Images