ParDiff: Practical Static Differential Analysis of Network Protocol ParsersOOPSLA 2024 Distinguished Paper Award
This program is tentative and subject to change.
Countless devices 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 those that hide in message parsers but do not cause crashes. 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 representing protocol format specifications from programs, and (2) then leverages bisimulation and SMT solvers to find fine-grained, semantic inconsistencies between them. We have extensively evaluated our approach using 14 network protocols, each with two different implementations. The results show that ParDiff exhibits higher precision in discovering bugs in protocol parsers compared to both differential symbolic execution and differential fuzzing tools. To date, we have detected 41 logical bugs with 25 confirmed by developers. The baseline DPIFuzz can only detect 3 of them in the same time budget and can only detect 25 of them even with 720× time cost.
This program is tentative and subject to change.
Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:20 | Static Analysis and Program Verification 1OOPSLA 2024 at IBR East Chair(s): Di Wang Peking University | ||
10:40 20mTalk | Cocoon: Static Information Flow Control in Rust OOPSLA 2024 Ada Lamba Ohio State University, Max Taylor Ohio State University, Vincent Beardsley Ohio State University, Jacob Bambeck Ohio State University, Michael D. Bond Ohio State University, Zhiqiang Lin The Ohio State University | ||
11:00 20mTalk | Computing Precise Control Interface Specifications OOPSLA 2024 Eric Campbell Cornell University, Hossein Hojjat Tehran Institute for Advanced Studies (TeIAS), Nate Foster Cornell University and Jane Street DOI | ||
11:20 20mTalk | FlowCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic Fractional Permissions OOPSLA 2024 Zhengyao Lin Carnegie Mellon University, Joshua Gancher Northeastern University, Bryan Parno Carnegie Mellon University DOI | ||
11:40 20mTalk | ParDiff: Practical Static Differential Analysis of Network Protocol ParsersOOPSLA 2024 Distinguished Paper Award OOPSLA 2024 Mingwei Zheng Purdue University, Qingkai Shi Nanjing University, Xuwei Liu Purdue University, USA, Xiangzhe Xu Purdue University, Le Yu , Congyu Liu Purdue University, Guannan Wei Inria/ENS; Tufts University, Xiangyu Zhang Purdue University | ||
12:00 20mTalk | Sound and partially-complete static analysis of data-races in GPU programs OOPSLA 2024 Dennis Liew University of Massachusetts Boston, Tiago Cogumbreiro University of Massachusetts Boston, Julien Lange Royal Holloway, University of London DOI |