Ph.D. Thesis Defense: Minh Vu
Wednesday, November 24, 2021
8:30 AM (CST)
Zoom: https://unl.zoom.us/j/92461084500
Meeting ID: 924 6108 4500
"Network Protocol Implementation Testing and Verification under Packet Dynamics"
Network protocols are sets of rules that define how data is transferred between network devices. These protocols must work properly because they are the core components of many Internet services. Bugs in these protocols can cause severe consequences, ranging from security invulnerability to network outages. Unfortunately, correctness testing of network protocols is very challenging due to the large space of inputs defined by packet dynamics such as packet delay, duplication, reordering, and loss. Software testing and verification techniques have advanced significantly in recent years, but these techniques are generally only effective on specific types of programs. Current works applying these techniques to network protocol implementations are still limited and thus incapable of comprehensively checking complex implementations such as the Internet Transmission Control Protocol (TCP). Our proposed work aims to address the scalability of these techniques following two approaches. In the first approach, we focus on testing network protocols. Testing is a cost-effective way to check common cases and demonstrate how the implementations work. The challenge is to check all possible behaviors which grow exponentially under packet dynamics. Our work leverages powerful and popular methods in the software testing and verification community, such as symbolic execution and random testing. We propose novel techniques to improve the efficiency of the testing methods for checking the correctness of network protocols by several orders of magnitude. In the second approach, we focus on the verification of real-world TCP implementations through exhaustive symbolic execution. TCP implementations are presented in billions of devices, and thus the topic of guaranteeing their correctness has received many interests in the networking community. Exhaustive symbolic execution can explore all execution paths through a program and verify the correctness in each of the paths. However, the total number of execution paths is usually an exponential function of the number of variables, which severely limits the state space defined by the number of packets and the ranges of network parameters we can check. Our proposed technique is capable of verifying the correctness properties of TCP implementations up to a much larger state space than existing techniques
Committee:
Dr. Lisong Xu, Chair
Dr. Witawas Srisa-an
Dr. Sebastian Elbaum
Dr. Bo Deng