FMitF: Track I: Automated Learning of Quantitative Network Models (ALOFT)

Computer networks are critical for distributed software systems, and their failure can lead to major disruptions. Tools for verifying networked behavior can help catch bugs and improve trust, but there is a fundamental challenge that limits the applicability of formal methods in networking: the need for precise models of the devices, topologies, and systems being verified. This project will develop new techniques that enable automatic construction of such models, which will enable broader use of formal verification in networking, ensuring that networks satisfy specified correct properties and are aligned with the intents of human operators. The project will also pursue education and outreach efforts to share results with the broader community and will seek to transition the fundamental research into practice through collaborations with industrial partners. Despite many recent successes of verification in networking, many important properties remain challenging to formally reason about. One challenge is the lack of models that automatically evolve as changes are made to network devices, configuration, and topology. Another challenge is the lack of models that capture essential quantitative properties such as latency and reliability. This project will further the vision of automated inference of models and provide efficient techniques for quantitative model learning that do not require access to source code or handcrafted models of network behavior. At the core of the development will be a unique integration of new closed-box learning algorithms and symbolic techniques crucial to tame the scale of network models. The outcomes will be a new generation of formal verification techniques based on closed-box learning and grounded in applications in networking. 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.