NeTS: Small: Systematically and Scalably Testing Network Programs through Symbolic Exploration of Packet Dynamics

网络协议和应用程序是Internet的重要组成部分，必须正确实施它们，才能使Internet节点(例如台式PC、笔记本电脑、智能手机、传感器和路由器)能够正确地相互通信。然而，它们的实现的正确性很难测试，特别是在数据包动态引入的潜在行为的大空间下。这是因为存在大量令人望而却步的分组动态可能性，并且许多错误仅在低概率的角落情况下被发现，例如具有特定分组延迟、分组数量、分组排序或分组丢失和复制的情况。本项目的目标是设计和实现数据包动态和底层网络的符号表示法和方法。这些表示和方法将使得能够使用基于符号执行的新兴测试用例生成技术来系统地探索网络协议和应用实现。该方法将利用符号执行能力来关注不同的输入类，在我们的上下文中针对数据包动态和网络状态，避免冗余地测试等价行为，而是将测试资源花费在导致不同的和潜在的错误行为的数据包动态上。首先，开发常见类型的Internet数据包动态的符号表示法，例如独立和相关的数据包延迟以及数据包丢失率。其次，设计分布式符号驱动程序，为测试中的网络程序提供使用符号包动态在网络上进行通信的假象。第三，设计了一类混合符号和随机包动力学模型的执行方法，用于测试具有大量包的网络程序。第四，对提出的技术和工具进行评估。这些任务将提供新的见解，以了解关键网络协议和应用程序的正确性，以及哪些类型的表示和方法在检测不同类型的错误时更有效。关键的潜在更广泛的影响是检测关键网络协议和应用程序中的错误，这些错误可能在计算机科学界之外产生共鸣。此外，网络和软件工程界成员的共同努力是罕见的，但如本提案所示，在将最新的验证方法应用于关键网络基础设施以及将网络时机和规模问题推向软件测试议程的前沿方面，显然可能是有益的。从这一角度来看，这项提案的交叉性质以及调查人员有良好记录的预期副产品(学生、数据、工具、顶级场所的论文)将在两个社区产生影响和产生协同效应。调查人员将举行研讨会，与专业人员和学生的系统和软件工程小组讨论该项目的挑战和结果。他们还将继续通过这个项目积极招收和培养本科生、女生和少数民族学生。

Network protocols and applications are an essential component of the Internet, and they must be implemented correctly so that Internet nodes (e.g., desktop PCs, laptops, smartphones, sensors, and routers) can correctly communicate with one another. However, the correctness of their implementations is difficult to test, especially under the large space of potential behavior introduced by packet dynamics. This is because there are a prohibitively large number of packet dynamics possibilities, and many bugs are revealed only in low probability corner cases, such as those with specific packet delay, number of packets, packet ordering, or packet loss and duplication. 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 leverage symbolic execution capabilities of focusing on distinct input classes, in our context for packet dynamics and network states, avoiding redundantly testing equivalent behavior, and instead spending testing resources on packet dynamics leading to distinct and potentially buggy behavior.The proposed research consists of four research tasks. First, develop symbolic representations of common types of Internet packet dynamics, such as independent and dependent packet delays, and packet loss rates. Second, design distributed symbolic drivers that provide a network program under test with the illusion of communicating over a network with symbolic packet dynamics. Third, design a class of execution methods with mixed symbolic and random packet dynamics models for testing a network program with a large number of packets. Fourth, evaluate the proposed techniques and tools. The tasks will provide new insights into the correctness of vital network protocols and applications, and what type of representations and methods are more effective at detecting different types of bugs.The key potential broader impact is the detection of bugs in critical network protocols and applications, which may resonate well outside the computer science community. In addition, joined efforts by members of the networking and the software engineering communities are rare, but as shown in this proposal could be clearly beneficial in bringing the latest validation methodologies to bear in critical networking infrastructure, and in pushing to the forefront of the software testing agenda the networking timing and scale issues. From that perspective, the cross-cutting nature of this proposal and the expected byproducts for which the investigators have a strong record (students, data, tools, papers in top venues) will impact and generate synergy across both communities. The investigators will hold seminars to discuss with the systems and software engineering groups of professional and students the challenges and results of the project. They will also continue actively recruiting and training undergraduate, female, and minority students through this project.