Peregrine: A Language-Agnostic Packet Processing Intermediate Representation with Formal Guarantees

Overview & Synopsis

Many different programmable network devices and domain-specific languages (DSLs) for programming them have been developed in recent years. However, the affiliated compiler infrastructure for each DSL has not kept up, leading to unreliable compilation results and ultimately a poor experience for developers. In response to this fragmented ecosystem, we propose an intermediate representation, Peregrine, to consolidate the common compiler functionalities within this domain into a shared, open-source infrastructure. We designed Peregrine to provide formal guarantees from the beginning, rather than adding them in a later step. The language comes with a formal semantics, along with an equivalence checker written and proven correct in Rocq. Experimental results show that Peregrine is general enough to express multiple applications written in various state-of-the-art network programming languages. The equivalence checker designed in Peregrine can be used for validating the correctness of a range of untrusted compiler passes, as well as for other surprising use cases such as certifying the correctness of packet classification algorithms within a reasonable amount of time.