FMitF: Track II: Symbolic Network Simulator

网络程序，如网络协议和应用程序，在互联网上扮演着重要的角色。然而，它们的正确性很难测试，因为它们的行为取决于它们的网络环境，但所有可能的网络环境的空间是惊人的大。符号执行作为一种强大的程序分析技术，可以利用空间中的等价类系统而有效地探索大空间。然而，一个显着的障碍，在使用符号执行测试网络程序是大量的努力，仪表和修改网络程序，以模拟他们的符号网络环境。该项目提供了一个强大的和通用的符号网络环境的平台，使网络程序可以更有效地和更容易地测试使用符号执行的各种目的，如寻找低概率的错误，并测量最坏情况下的性能。这个项目开发的符号网络环境，利用一个良好的发展和广泛使用的网络模拟器，NS-3。具体来说，这个项目扩展了NS-3，并开发了一个符号网络模拟器，称为SymNS-3，象征性地测试网络程序在各种符号网络环境。SymNS-3被设计为易于用途：NS-3的应用程序接口（API）将被扩展，这样测试人员可以通过在模拟脚本中调用API来轻松灵活地定义定制的符号网络环境，而不需要费力地对NS-3模拟器进行仪器化。SymNS-3的设计也是高效的：多个NS-3核心组件将被重新设计，以指数级地减少探索的程序执行路径的数量，同时仍然生成正确的模拟结果。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.