FMitF: Track I: ComScaN: Composition and Scaling of Network Service Functions

In today's interconnected world, network operators need the ability to rapidly deploy, update, and scale services on-demand. Building such systems is challenging, and assuring their correctness and performance has been elusive. The project team aims to develop a 'green field' approach to support future networks and emerging services in such a manner that scalability is inherent by design and correctness and performance claims can be backed up with mathematical rigor. This is achieved by bringing together and extending recent research advances in the areas of networking systems, programming languages, and software-verification methods. This is intended to provide network operators with the ability to express desired requirements for a diverse range of services, the flexibility to easily adapt those services to keep pace with changing demand and evolving network infrastructure, and the assurance that performance and correctness goals are upheld. The research is expected to produce a viable prototype demonstrating the core ideas along with an ecosystem of open-source software tools, experimental data and, example applications. The learnings from this project will be incorporated into the academic curriculum to equip the workforce with the skills needed to build reliable and performant networking infrastructure. The work is being carried out by attracting, engaging and mentoring a diverse group of budding researchers, with an intentional focus on welcoming and encouraging participation by hitherto under-represented groups in advanced computing research.

In this project the principal investigators advance a green-field approach to enable quantitative performance reasoning of Network Function Virtualization (NFV) scaling. It is designed from the ground up based on formal foundations and principled approaches. At the basis of the proposed framework, referred to as ComScaN, is an extensible, declarative domain-specific language (DSL) framework using a novel actor model. It is designed with flexible and rich built-in language constructs to support ease of specification and separation of concerns. Co-designing with the flexible and extensible actor-based DSL framework, the project team is developing a formal foundation for ComScaN with a suite of semantic models, formal methods and tools for automatic program analysis, verification and synthesis, with the goal to facilitate quantitative performance reasoning of NFV scaling. Quantitative performance reasoning techniques for scaling NFV as well as algorithms for verifying correctness and performance of service function chains (SFCs) and synthesis-based approaches for generating dynamic workloads for testing and evaluation of SFCs are being developed.

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.