Systematically and Scalably Testing Network Programs

through Symbolic Exploration of Packet Dynamics


Network programs including the implementations of network protocols and network applications are difficult to test, especially under the large space of behavior defined by packet dynamics such as packet delay, jitter, reordering, and loss. This is because there are a prohibitively large number of packet dynamics possibilities, and many bugs are revealed only in corner cases with low probabilities. Approaches using test-bed experiments with random packet dynamics are very unlikely to explore the behaviors revealing such bugs, and approaches using implementation-level model checking often fail to capture the timeliness and dynamics not present in the code of network protocols and applications.

The goal of this project is to design and implement symbolic representations and methods for packet dynamics and the underlying network. These representations and methods will enable the use of emerging test case generation techniques based on symbolic execution for a systematic exploration of network protocol and application implementations. The approach will assist in targeting low-probability bugs or extreme-case performance by leveraging symbolic execution capabilities of focusing on distinct input classes, in our context for packet dynamics and network states, avoiding redundantly testing equivalent packet dynamics, and instead spending testing resources on packet dynamics leading to distinct and potentially buggy behavior.

Selected Publications:

Supported by