一句话：提出静态差分分析 ParDiff，通过从多个协议实现中提取有限状态机并用互模拟与 SMT 比较，自动发现协议解析器中的语义缺陷。
网络协议实现中的缺陷常常只造成静默数据损坏而非崩溃，因此以内存安全为目标的自动化缺陷发现技术（如 fuzzing）难以奏效。本文提出静态差分分析工具 ParDiff：其核心观察是同一协议常有多个实现，实现之间的语义差异往往暗示缺陷。为克服不同实现风格迥异、难以直接比较的困难，ParDiff 自动从程序中提取有限状态机以刻画协议格式规范，并借助互模拟与 SMT 求解器发现细粒度、语义层面的不一致。作者在 14 个网络协议上进行了广泛评估，结果表明 ParDiff 优于差分符号执行与差分 fuzzing 工具，目前已检测出 41 个缺陷，其中 25 个得到开发者确认。
Countless devices all over the world are connected by networks and communicated via network protocols. Just like common software, protocol implementations suffer from bugs, many of which only cause silent data corruption instead of crashes. Hence, existing automated bug-finding techniques focused on memory safety, such as fuzzing, can hardly detect them. In this work, we propose a static differential analysis called ParDiff to find protocol implementation bugs, especially silent ones hidden in message parsers. Our key observation is that a network protocol often has multiple implementations and any semantic discrepancy between them may indicate bugs. However, different implementations are often written in disparate styles, e.g., using different data structures or written with different control structures, making it challenging to directly compare two implementations of even the same protocol. To exploit this observation and effectively compare multiple protocol implementations, ParDiff (1) automatically extracts finite state machines from programs to represent protocol format specifications, and (2) then leverages bisimulation and SMT solvers to find fine-grained and semantic inconsistencies between them. We have extensively evaluated ParDiff using 14 network protocols. The results show that ParDiff outperforms both differential symbolic execution and differential fuzzing tools. To date, we have detected 41 bugs with 25 confirmed by developers.
@article{paperbot2553,
title = {ParDiff: Practical Static Differential Analysis of Network Protocol Parsers},
author = {Mingwei Zheng and Qingkai Shi and Xuwei Liu and Xiangzhe Xu and Le Yu and Congyu Liu and Guannan Wei and Xiangyu Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649854}
}