Dissertation defense next Wednesday

Ph.D. dissertation defense
Ph.D. dissertation defense

Wei Sun's Ph.D. dissertation defense, "Automated Testing Of Network Protocol Implementations Under Packet Dynamics," will be next Wednesday, Nov. 22 at 10 a.m. in room 112 of the Schorr Center.

Committee Members: Dr. Lisong Xu (Advisor) and Dr. Sebastian Elbaum (Co-Advisor)
Dr. Massimiliano Pierobon and Dr. Wei Qiao

Abstract:
Network protocols are an essential component of the Internet, and they must be implemented correctly. However, the implementations of network protocols are difficult to test, especially under the large space of potential behaviors introduced by packet dynamics. This is because there are a prohibitively large number of packet dynamics possibilities, and many faults are revealed only in low-probability corner cases, such as those with a specific packet delay, packet ordering, packet loss, or with a certain number of packets. 

In this effort, we first propose a symbolic execution approach that leverages an advanced technique from the software engineering community called symbolic execution to find the equivalence classes of packet dynamics that lead to exactly the same behavior, in order to efficiently check the large space of potential behaviors introduced by packet dynamics. Our proposed symbolic execution approach avoids redundantly testing equivalent behaviors, and instead spends testing resources on packet dynamics that lead to distinct and potentially buggy behaviors. Our experiments show that the symbolic execution approach can achieve significantly higher packet dynamics coverage than the commonly used random testing approach. However, the symbolic execution approach does not scale well due to the path explosion problem. To address this issue, we propose two unique domain-specific heuristics driven by network protocol properties instead of general code properties, in order to improve the cost-effectiveness of the symbolic execution approach. Our experiment results show that our proposed domain-specific heuristics significantly improve the cost-effectiveness of the symbolic execution approach for transport protocols, detecting three times as many faults as the one without the heuristics when the testing budget is in the range of minutes and hours. 

Considering that random testing is widely used in the industry, due to its simplicity and low cost, to better understand and improve current random testing in the context of packet dynamics, we conduct an extensive study on the fault-detection capabilities of different models of random packet dynamics. We find that different models have quite different fault-detection capabilities and some limitations exist in the common realistic models. Our study recommends the inclusion of some unlikely models when testing the correctness of protocol implementations as they may help to quickly detect the otherwise hard-to-detect and potentially consequential faults.

The last contribution of this research is to improve current TCP congestion control testing. Current common testing practices on congestion control algorithms are inefficient in detecting potential issues due to the prohibitively large space of network environments. To solve the challenge, we propose an automated and efficient approach based on feedback-directed random testing, called ACT. For a congestion control algorithm, ACT automatically tests the algorithm without requiring expert knowledge as manual testing, and efficiently tests different algorithm behaviors as directed by the algorithm state space. Our Linux experiments show that ACT can test much more different congestion control algorithm behaviors than both traditional manual testing and undirected random parameter selection. Additionally, we propose a novel scalable testing method, called SCCT. Different from ACT that randomly tests the whole TCP system and looks for congestion control related faults in any part of TCP, SCCT systematically tests only the code of a congestion control algorithm and looks for the faults only in the congestion control part of TCP. Impressively, both ACT and SCCT successfully detect multiple faults in Linux congestion control algorithms that have not been reported before. The Linux kernel developers have already fixed some faults based on our findings.