“Using Symbolic Execution To Analyze The Hardware TCP Protocol”

As the demand for high performance and flexible networking capabilities increases, the shift from software to hardware implementations of state networking functions (such as TCP) is becoming increasingly important. This transition not only enhances processing efficiency in modern networking environments where data transmission rates are rising, but it also reduces the inherent CPU overhead found in software implementations, allowing hardware devices to handle network traffic more efficiently. However, validating the correctness of these hardware designs poses significant challenges due to the complex timing requirements and the vast input space associated with packet-level properties. The verification of packet-level properties requires coverage of various complex situations arising from network state changes, including packet order, delays, and losses, all of which manifest particularly complex behavior under the fine-grained clock cycles of hardware systems. Moreover, state networking functions exhibit strong temporal dependencies; in high-frequency hardware designs, the time span for each property can extend to millions of clock cycles. Exhaustively testing every potential combination of packet behaviors leads to an exponentially growing input space, making it difficult for traditional testing methods to effectively cover all possible behavioral scenarios. To address this issue, this paper proposes a testing method based on symbolic execution, aimed at systematically exploring the correctness of hardware state networking functions over long time sequences and within a vast number of clock cycles. This approach symbolically represents key input variables (such as packet delays and retransmission counts) as constraints, allowing a smaller set of test inputs to cover a broader state space, thereby effectively improving the verification coverage of packet-level properties. At the same time, symbolic execution can significantly reduce testing time through refined path control and automated analysis, avoiding the redundant calculations associated with traditional exhaustive methods, especially in addressing complex networking scenarios like packet loss, out-of-order delivery, and timing windows. Our testing framework not only increases coverage but also further reduces the consumption of testing resources, identifying potential issues in the design under various states and providing an innovative solution for efficiently validating hardware state networking functions.

Committee Members:
Dr. Lisong Xu, Advisor
Dr. Witty Srisa-an, Co-advisor
Dr. Bhuvana Gopal
Dr. Rahul Purandare