FMitF: Track II: Symbolic Network Simulator

FMITF：轨道 II：符号网络模拟器

• 批准号: 1918204
• 负责人: Lisong Xu
• 金额: $ 9.99万
• 依托单位: University of Nebraska-Lincoln
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-11-01 至 2022-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1918204&HistoricalAwards=false
• 关键词: FMitF; Track; II; Symbolic; Network

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.

网络协议和应用程序等网络程序在Internet上扮演着至关重要的角色。然而，它们的正确性很难测试，因为它们的行为依赖于它们的网络环境，但所有可能的网络环境的空间都大得令人望而却步。符号执行作为一种强大的程序分析技术，可以通过利用空间中案例的等价类来系统而有效地探索大空间。然而，使用符号执行来测试网络程序的一个重要障碍是插装和修改网络程序以对其符号网络环境建模的大量工作。该项目提供了一个强大而通用的符号网络环境平台，以便可以更高效、更容易地使用符号执行来测试各种目的的网络程序，例如用于查找低概率错误和测量最坏情况的性能。本项目利用开发成熟、应用广泛的网络模拟器NS-3来开发符号网络环境。具体地说，本项目对NS-3进行了扩展，开发了一个符号网络模拟器Symns-3，用于在各种符号网络环境中对网络程序进行符号测试。Symns-3易于使用：将扩展NS-3的应用程序接口(API)，以便测试员只需在模拟脚本中调用API即可轻松灵活地定义定制的符号网络环境，而无需费力地为NS-3模拟器插入指令。Symns-3还被设计为高效的：将重新设计多个NS-3核心组件，以指数级减少探索的程序执行路径的数量，同时仍能生成正确的模拟结果。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Efficient Protocol Testing Under Temporal Uncertain Event Using Discrete-event Network Simulations

使用离散事件网络模拟在时间不确定事件下进行高效协议测试

• DOI: 10.1145/3490028
• 发表时间: 2022
• 期刊: ACM Transactions on Modeling and Computer Simulation
• 影响因子: 0.9
• 作者: Vu, Minh;Xu, Lisong;Elbaum, Sebastian;Sun, Wei;Qiao, Kevin
• 通讯作者: Qiao, Kevin

Symbolic ns-3 for Efficient Exhaustive Testing: Design, Implementation, and Simulations

用于高效详尽测试的符号 ns-3：设计、实现和模拟

• DOI: 10.1145/3532577.3532604
• 发表时间: 2022
• 期刊: WNS3: Workshop on ns-3
• 作者: Shao, Jianfei;Vu, Minh;Zhang, Mingrui;Jayswal, Asmita;Xu, Lisong
• 通讯作者: Xu, Lisong

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