Extracting Protocol Format as State Machine via Controlled Static Loop Analysis

TL;DR

This work addresses the challenge of reverse-engineering protocol message formats by inferring parsing FSMs from protocol implementations using a static analysis. The key idea is to treat each loop iteration in the parser as a FSM state and to merge multiple concrete paths into path sets to avoid path explosion, enabling fixed-point convergence to a compact, accurate FSM. The StateLifter framework demonstrates high precision and recall (over $90\%$) with rapid inference (about $5$ minutes) across ten benchmarks, and significantly improves protocol fuzzing coverage (up to $3.3\times$) while revealing zero-day vulnerabilities. The approach offers a practical, scalable alternative to trace-based and dynamic techniques, with strong implications for automated protocol verification and security testing.

Abstract

Reverse engineering of protocol message formats is critical for many security applications. Mainstream techniques use dynamic analysis and inherit its low-coverage problem -- the inferred message formats only reflect the features of their inputs. To achieve high coverage, we choose to use static analysis to infer message formats from the implementation of protocol parsers. In this work, we focus on a class of extremely challenging protocols whose formats are described via constraint-enhanced regular expressions and parsed using finite-state machines. Such state machines are often implemented as complicated parsing loops, which are inherently difficult to analyze via conventional static analysis. Our new technique extracts a state machine by regarding each loop iteration as a state and the dependency between loop iterations as state transitions. To achieve high, i.e., path-sensitive, precision but avoid path explosion, the analysis is controlled to merge as many paths as possible based on carefully-designed rules. The evaluation results show that we can infer a state machine and, thus, the message formats, in five minutes with over 90% precision and recall, far better than state of the art. We also applied the state machines to enhance protocol fuzzers, which are improved by 20% to 230% in terms of coverage and detect ten more zero-days compared to baselines.

Figures (18)

• Figure 1: Example to illustrate the insight of our approach.
• Figure 2: (a) Implementation of the FSM in Figure \ref{['fig:insight']}(a). (b) The FSM inferred by the state-of-the-art static analysis, i.e., Proteus. (c) The FSM that represents the message format inferred by AutoFormat. (d) The FSM that represents the message format inferred by Tupni. (e) The FSM inferred by our approach, which is exactly the same as the compressed FSM in Figure \ref{['fig:insight']}(b).
• Figure 3: Basic steps of our approach.
• Figure 5: Violation of SR3.
• Figure 6: Language of target programs.

Theorems & Definitions (13)

• Definition 2.1
• Theorem 1: Convergence
• proof
• Theorem 2: Soundness and Completeness
• proof
• Lemma 1: Soundness of $(S, \mathbb{E}_S)$
• proof
• Lemma 2: Soundness of $(S, \mathbb{E}_S, S')$
• proof
• Lemma 3: Soundness of FSM