Thu 18 Jul 2019 10:30 - 10:50 at Mancy - Domain Specific Languages Chair(s): Sebastian Erdweg

The P4 programming language offers high-level, declarative abstractions that bring the flexibility of software to the domain of networking. Unfortunately, the main abstraction used to represent packet data in P4 - header types - lacks basic safety guarantees. Over the last few years, experience with an increasing number of P4 programs has shown the risks of the unsafe approach, which often leads to subtle software bugs.

This paper proposes SafeP4, a domain-specific language for programmable data planes in which all packet data is guaranteed to have a well-defined meaning and satisfy essential safety guarantees. We equip SafeP4 with a formal semantics and a static type system that statically guarantees header validity - a major source of safety bugs according to our analysis of real-world P4 programs. Statically ensuring header validity is challenging because the set of valid headers can be modified at runtime, making it a dynamic program property. Our type system achieves static safety by using a form of path-sensitive reasoning that tracks dynamic information from conditional statements, routing tables, and the control plane. Our empirical evaluation shows that SafeP4’s type system can effectively eliminate common failures in many real-world programs.

Thu 18 Jul

ecoop-2019-papers
10:30 - 12:10: Research Papers - Domain Specific Languages at Mancy
Chair(s): Sebastian ErdwegJGU Mainz
ecoop-2019-papers10:30 - 10:50
Research paper
Matthias Eichholz, Eric CampbellCornell University, Nate FosterCornell University, Guido SalvaneschiTU Darmstadt, Mira MeziniTU Darmstadt, Germany
DOI
ecoop-2019-papers10:50 - 11:10
Research paper
Yossi GilTechnion—Israel Institute of Technology, Ori RothTechnion
DOI
ecoop-2019-papers11:10 - 11:30
Research paper
Kang Hong JinSchool of Information Systems, Singapore Management University, Ferdian Thung, Julia LawallInria/LIP6, Gilles MullerLIP6-INRIA/UPMC, Lingxiao JiangSingapore Management University, David LoSingapore Management University
DOI
ecoop-2019-papers11:30 - 11:50
Research paper
Amir ShaikhhaUniversity of Oxford, Lionel ParreauxEPFL
DOI
ecoop-2019-papers11:50 - 12:10
Research paper
Dhruv MakwanaUnaffiliated, Neel KrishnaswamiComputer Laboratory, University of Cambridge
DOI Pre-print