FMitF: Track I: Petr4: Formal Foundations for Programmable Networks

Cornell University, Ithaca NY

Investigators

Abstract

Most networks today achieve robustness not by adhering to precise formal specifications but by building implementations that tolerate modest deviations from correct behavior. But as networks have grown in scale and complexity, the frequency of faults caused by these deviations has increased, leading to new interest in techniques for formally specifying and verifying network behavior. The goal of the Petr4 ("petra") project is to build a new foundation for networking by developing a precise, formal semantics for the programs that execute on network devices such as Internet routers. The project's novelties are in applying programming language-based techniques to an emerging area and building verified software tools, such as a compiler that generates code guaranteed to correctly implement the semantics of a given source program. The project's impacts are in developing open-source software, pursuing technology transfer with industry partners, and designing material for an outreach workshop aimed at undergraduates from under-represented groups. At a technical level, the project will focus on four distinct research thrusts: (1) Developing a formal semantics for the P4 Programming Language, realized as a set of mathematical definitions and an accompanying reference implementation; (2) Building a verified compiler from P4 to eBPF, the language used to express custom packet-processing in the Linux kernel; (3) Investigating new control-plane APIs that are rich enough to capture key invariants and facilitate correct composition of control applications; and (4) Developing a library of executable protocol implementations that can be assembled into a modular Internet router. The project will be guided by an interdisciplinary research team with expertise in both formal methods and networking, and seeks to not only develop a new foundation for networking, but also serve as a catalyst for follow-on efforts that target higher layers of the networking stack. 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.