Why are my packets being dropped? Why does my Internet connection keep resetting? Programmers developing software have access to a panoply of tools including compilers, debuggers, static and dynamic checkers. Unfortunately, network operators have access to only crude tools such as TraceRoute and Ping. These tools have remained unchanged for decades while networks have grown increasingly complicated: load balancers spread traffic using unknown hash functions, and firewalls interdict messages based on cryptic rules that human operators enter, sometimes incorrectly. In a world of services accessed from tablets and mobile devices, network failures are a debilitating source of operational expenditures.
On the surface, networks with their collections of routers, switches, network interface cards, and cabling do not resemble code. But one can view the entire network as a "program" that takes packets from the input edges of the network and outputs packets to the output edge after possibly rewriting the packet. The forwarding table at routers can, for instance, be viewed as a large Switch statement across destination addresses.
This lens has led several researchers to frame a new agenda for networks, sometimes called network verification. They ask: what are the equivalents of compilers, debuggers, and static checkers for networks? Early work has already produced static reachability checkers of impressive speed and scale, algorithms to synthesize network firewalls from policy specifications, automatic network testers, and debuggers.
Some of the research has gone beyond opportunistic application of ideas from programming languages to a new merging of two streams of thought. For example, network verification often seeks all headers that reach a destination (more analogous to allSAT than SAT), extends notions in software testing of covering every line or function to covering every link and router queue, and finesses the problem of global time in debugging using notions of causality.
The following paper is exciting because it takes existing static checking of networks to a new level by checking the real code in the forwarding path of a Click router using classical software verification tools, and not just a model of router software as was used in previous work. It also proves absolute properties and can discover all possible bugs.
The reader may wonder why software routers are interesting when the forwarding path of the vast majority of routers used today is implemented in inscrutable hardware chips. One answer is there has been a resurgence in software networking on virtual machines in public clouds such as Azure and EC2. Second, the simplifications exploited in the paper are based on code structured as pipelines, which is the way almost all real routers are built. Thus, in principle, their ideas could be applied to hardware routers as well. Third, there is a new movement toward designing flexible routers using a pipeline-based language called P4 that has similarities to Click. Could the techniques in this paper be useful to verify P4 programs?
The following paper is exciting because it takes existing static checking of networks to a new level by checking the real code in the forwarding path of a Click router using classical software verification tools.
Verification experts may cry foul because control flow is restricted and the data structures used are merely arrays with no dynamic pointer allocation. Have the authors merely defined the complexities of verification away? The authors rightly argue their contribution is in pointing out that small limitations in the way router forwarding software (and possibly hardware) is written can make it possible to efficiently verify router behavior, and they argue the cost of such restrictions—such as using slightly less efficient lookup tables—is small. The techniques in this paper can be combined with other techniques to verify entire networks at a more realistic level of abstraction than was considered previously.
Others may argue the results do not produce the copious amount of bugs found in prior work. However, I find it heartening the bugs they found in Click were in the interaction of obscure cases in seemingly orthogonal features such as fragmentation and IP options. Such bugs often lurk in the rarely used pathways of the execution, are difficult to flush out using conventional testing techniques, and can sometimes surface later in expensive live-site incidents.
Impressive strides have been made in applying programming languages techniques to find bugs in large complex code including bug finding for Linux and formal verification for seL4. While this work can be regarded as an experimental rocket launch, it gives us hope that someday we will reach the moon.
Join the Discussion (0)
Become a Member or Sign In to Post a Comment