Verifying protocol plugins

The Internet is subject to an issue called "protocol ossification". That is, due to deployment slowness of new network protocols in computer networks, such networks lose in flexibility. To solve this issue, researchers proposed a major paradigm shift with pluginized protocols, such as PQUIC and xBGP. They implement the core protocol functionalities and offer a flexible, vendor-neutral API. This interface allows network engineers to rewrite the protocol behavior using extensions called plugins. However, they raise security issues since these plugins have full control on the protocol. To counter that, PQUIC authors proposed a theoretical distributed system called Secure Plugin Management System (SPMS). It allows to validate that plugins respect safety properties and distribute trust proofs among networked peers. This work proposes a practical design and prototype implementation of the SPMS. It also introduces the verification of a new property, called side effects, on PQUIC plugins. This property ensures that plugins only modify connection data for which they have the right to do so.