A (Not) NICE Way to Verify the OpenFlow Switch Specification: Formal Modelling of the OpenFlow Switch Using Alloy

摘要

The introduction of Software Defined Networks (SDNs) is completely changing the way in which networks are built and managed. SDNs decouple data from control plane access, which makes introduction of new network functionalities significantly simpler. The philosophy of OpenFlow is a move towards centralization, where a single controller program manages the logic of switches. While centralized systems are often easier to coordinate, the likelihood of bugs is still high. Despite the existence of an OpenFlow Specification [3], it may still be possible observe unexpected behavior while adhering to this Specification. This can be due to various reasons, such as underspecification of some aspect of the protocol or a contrived sequence of events.