Communications of the ACM
Software Dataplane Verification
Credit: iStockPhoto.com
The industry is in the mood for programmable networks, where an operator can dynamically deploy network functions on network devices, akin to how one deploys virtual machines on physical machines in a cloud environment. Such flexibility brings along the threat of unpredictable behavior and performance. What are the minimum restrictions that we need to impose on network functionality such that we are able to verify that a network device behaves and performs as expected, for example, does not crash or enter an infinite loop? We present the result of working iteratively on two tasks: designing a domain-specific verification tool for packet-processing software, while trying to identify a minimal set of restrictions that packet-processing software must satisfy in order to be verification-friendly. Our main insight is that packet-processing software is a good candidate for domain-specific verification, for example, because it typically consists of distinct pieces of code that share limited mutable state; we can leverage this and other properties to sidestep fundamental verification challenges. We apply our ideas on Click packet-processing software; we perform complete and sound verification of an IP router and two simple middleboxes within tens of minutes, whereas a state-of-the-art general-purpose tool fails to complete the same task within several hours.
1. Introduction
What kind of programming interface should a network device expose to its operator? Answering this question involves a fundamental trade-off between flexibility and verifiability: the more flexible the interface we choose, the wider the range of functionality that we can deploy on a network device, but the harder it is to verify that the network device will behave and perform as expected, for example, it will not crash, no matter how we configure it or what traffic it receives.
No entries found