Congestion control algorithms, such as RENO and CUBIC, are vital for the Internet. However, numerous bugs have been discovered and reported in the Congestion Control Algorithm Implementations (CCAIs), even in those that have been extensively tested and used on the Internet for years, such as Linux RENO and Linux CUBIC. Some of these bugs have potentially severe impacts on the performance and stability of the Internet. Unfortunately, current CCAI testing and verification methods are inadequate for proving the absence of bugs, require substantial verification expertise, or are not scalable to a large number of acknowledgment packets (ACKs) that trigger CCAI actions. To address all these shortcomings, we propose an ACK Scalable Method, called ASM. Our experiments with two representative loss-based CCAIs, Linux RENO and CUBIC, demonstrate the promising performance of the proposed ASM even with tens of thousands of ACKs.

The significant impact of TCP congestion control on the Internet highlights the importance of testing congestion control algorithm implementations (CCAIs) in various network environments. Many CCAI testing problems can be solved by exploring the numerical state space of CCAIs, which is defined by a group of numerical (and nonnumerical) state variables of the CCAIs. However, the current practices for automated numerical state space exploration are either limited by the approximate abstract CCAI models or inefficient due to the large space of network environment parameters and the complicated relation between the CCAI states and network environment parameters. In this paper, we propose an automated numerical state space exploration method, called ACT, which leverages the model-agnostic feature of random testing and greatly improves its efficiency by guiding random testing under the feedback iteratively obtained in a test. Our experiments on five representative Linux TCP CCAIs show that ACT can more efficiently explore a large numerical state space than manual testing, undirected random testing, and symbolic execution based testing, while without requiring an abstract CCAI model. ACT detects multiple design and implementation bugs of these Linux TCP CCAIs, including some new bugs not reported before.

The packet time information at their receivers carries useful network information and is used by various networking applications and protocols. However it is challenging to accurately measure the packet time information in a cloud network due to various software and hardware factors at their receivers, such as virtual machine (VM) scheduling. In order to mitigate the impact of those receiver factors, we propose a novel packet timestamping mechanism to measure the inter-packet gaps just before they arrive at their receiver using an external clock server, which periodically sends packets to the receiver. We demonstrate the application of the proposed timestamping mechanism using an improved available bandwidth estimation method, which leverages two types of packet time information: the original packet time information measured using the local receiver clock, and the additional inter-packet gap information measured using the external clock server. Both our experiment results and analysis show that the additional information can greatly improve the available bandwidth estimation accuracy in a cloud network even with heavy VM scheduling at the cost of little additional traffic overhead.

The correctness of network protocol implementations is difficult to test mainly because of the temporal uncertain nature of network events. In order to test the correctness of a network protocol implementation using network simulators, we need to systematically simulate the behavior of the network protocol under all possible cases of temporal uncertain events, which is very time consuming. The recently proposed Symbolic Execution based Interval Branching (SEIB) simulates a group of uncertain cases together in a single simulation branch, and thus is more efficient than brute force testing. In this paper, we argue that the efficiency of SEIB could be further exponentially improved by eliminating unnecessary comparisons of the event timestamps. Specifically, we summarize and present three general types of unnecessary comparisons when SEIB is applied to a general network simulator, and then correspondingly propose three novel techniques to eliminate them. Our extensive simulations show that our techniques can improve the efficiency of SEIB by several orders of magnitude, such as from days to minutes.

Realistic network environments are commonly emulated by Internet application developers to test both the performance and the correctness of their applications. In this paper, we argue that emulating just realistic network environments may be inadequate for detecting hard-to-detect faults that have very low occurrence probabilities but potentially high impact if exposed in the real world. Specifically, we conduct extensive experiments to study the correctness testing capabilities of realistic and unlikely network environments. Our results show that small investments in emulating unlikely network environments may help in quickly detecting otherwise hard-to-detect faults.

New TCP congestion control algorithms are being developed and deployed in the Internet. However, it is challenging to test their correctness mainly due to the scalability problem caused by the extremely large number of test inputs. In this paper, we propose a scalable testing method, called SCCT, which tackles the scalability problem using two techniques. 1) SCCT tests only the congestion control algorithms of TCP at the interface level instead of the whole TCP at the packet level. 2) SCCT exercises an equivalence class of test inputs simultaneously using symbolic execution, instead of a single test input at a time. Both techniques can improve the scalability by many orders of magnitude. Our Linux TCP experiments on seven congestion control algorithms show that SCCT is scalable and quickly detects multiple Linux bugs that have not been reported before.

The majority of Internet traffic is transferred by transport protocols. The correctness of these transport protocol implementations is hard to validate as their behaviors depend not only on their protocols but also on their network environments that can introduce dynamic packet delay and loss. Random testing, widely used in industry due to its simplicity and low cost, struggles to detect packet delay related faults which occur with low probability. Symbolic execution based testing is promising at detecting such low probability faults, but it requires large testing budgets as it attempts to cover a prohibitively large input space of packet dynamics. To improve its cost-effectiveness, we propose two domain-specific heuristic techniques, called packet retransmission based priority and network state based priority, which are motivated by two common transport protocol properties. In our experiments using the Linux TFTP programs, our techniques improve the cost-effectiveness of symbolic execution based testing for transport protocols, detecting three times as many faults when the budget is in the range of minutes and hours.

Network programs are difficult to test, especially under the large space of network program behavior defined by packet dynamics such as packet delay and packet loss. It is unlikely for common approaches using testbeds with random packet dynamics to cover the prohibitively large number of packet dynamics possibilities in a limited time. In this paper, we leverage symbolic execution to find the equivalence classes of packet dynamics which lead to exactly the same network program behavior, in order to efficiently check the large space of network program behavior. Specifically, we propose and develop a network program test platform, called Symbolic Packet Dynamics (SPD), to automatically and transparently test unmodified network programs for low- probability bugs and extreme-case performance under packet dynamics. SPD uses symbolic representation of packet dynamics, instead of random packet dynamics. Our experiments show that SPD can achieve significantly much higher packet dynamics coverage than random packet dynamics within the same amount of time, and thus it is much easier and takes much shorter time for SPD to detect low-probability bugs and extreme-case performance.