FMitF: Track II: Symbolic Network Simulator

网络协议和应用程序等网络程序在Internet上起着至关重要的作用。然而，它们的正确性很难测试，因为它们的行为依赖于它们的网络环境，而所有可能的网络环境的空间是非常大的。符号执行作为一种强大的程序分析技术，可以利用空间中用例的等价类，系统有效地探索大空间。然而，使用符号执行来测试网络程序的一个重要障碍是，需要花费大量的精力来检测和修改网络程序，以模拟它们的符号网络环境。这个项目提供了一个强大的通用的符号网络环境平台，使得网络程序可以更有效、更容易地使用符号执行进行各种目的的测试，例如寻找低概率错误，以及测量最坏情况的性能。该项目通过利用一个开发良好且广泛使用的网络模拟器NS-3来开发符号网络环境。具体而言，本项目扩展了NS-3，并开发了一个符号网络模拟器，称为SymNS-3，用于在各种符号网络环境中对网络程序进行符号测试。SymNS-3的设计易于使用：将扩展NS-3的应用程序接口（API），以便测试人员只需在仿真脚本中调用API就可以轻松灵活地定义自定义的符号网络环境，而无需费力地测量NS-3模拟器。SymNS-3的设计也是高效的：多个NS-3核心组件将被重新设计，以便以指数方式减少探索程序执行路径的数量，同时仍然生成正确的模拟结果。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Network programs, such as network protocols and applications, play essential roles on the Internet. However, their correctness is difficult to test, because their behaviors depend on their network environments, but the space of all possible network environments is prohibitively large. Symbolic execution, as a powerful program-analysis technique, can systemically and efficiently explore a large space by leveraging the equivalence classes of cases in the space. However, a significant barrier in using symbolic execution to test network programs is the substantial effort of instrumenting and modifying network programs to model their symbolic network environments. This project provides a powerful and general platform of symbolic network environments so that network programs can be more efficiently and easily tested using symbolic execution for various purposes, such as for finding low-probability bugs, and measuring worst-case performance. This project develops symbolic network environments by leveraging a well-developed and widely used network simulator, NS-3. Specifically, this project extends NS-3 and develops a symbolic network simulator, called SymNS-3, to symbolically test network programs in various symbolic network environments. SymNS-3 is designed to be easy to use: The application program interface (API) of NS-3 will be extended so that a tester can easily and flexibly define a customized symbolic network environment by just calling the APIs in a simulation script without the need to laboriously instrument the NS-3 simulator. SymNS-3 is also designed to be efficient: multiple NS-3 core components will be re-designed in order to exponentially reduce the number of explored program execution paths while still generating the correct simulation results.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.