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

NeTS：小型：通过数据包动态的符号探索系统地、可扩展地测试网络程序

• 批准号: 1526253
• 负责人: Lisong Xu
• 金额: $ 49.98万
• 依托单位: University of Nebraska-Lincoln
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-10-01 至 2019-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1526253&HistoricalAwards=false
• 关键词: NeTS; Small; Systematically; Scalably; Testing

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.

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

项目成果

Efficient Correctness Testing of Linux Network Stack under Packet Dynamics

• DOI: 10.1109/icc40277.2020.9149060
• 发表时间: 2020-06
• 期刊: ICC 2020 - 2020 IEEE International Conference on Communications (ICC)
• 作者: Minh Vu;Phuong Ha;Lisong Xu