We present SymNet, a network static analysis tool based on symbolic execution. SymNet quickly analyzes networks by injecting symbolic packets and tracing their path through the network. Our key novelty is SEFL, a language we designed for network processing that is symbolic-execution friendly. SymNet is easy to use: we have developed parsers that automatically generate SEFL models from router and switch tables, firewall configurations and arbitrary Click modular router configurations. Most of our models are exact and have optimal branching factor. Finally, we built a testing tool that checks SEFL models conform to the real implementation. SymNet can check networks containing routers with hundreds of thousands of prefixes and NATs in seconds, while ensuring packet header memory-safety and capturing network functionality such as dynamic tunneling, stateful processing and encryption. We used SymNet to debug middlebox interactions documented in the literature, to check our department’s network and the Stanford backbone network. Results show that symbolic execution is fast and more accurate than existing static analysis tools.
@PARASPLIT Symbolic execution. We are not the first to propose using symbolic execution to analyze networks. @cite_4 used symbolic execution to check selected Click elements' source code for bugs, aiming to proove crash-freedom and bounded execution. We have shown that using C as modelling language does not scale, and have proposed SEFL and as scalable alternatives.
@cite_4
2155216527
Software dataplanes are emerging as an alternative to traditional hardware switches and routers, promising programmability and short time to market. These advantages are set against the risk of disrupting the network with bugs, unpredictable performance, or security vulnerabilities. We explore the feasibility of verifying software dataplanes to ensure smooth network operation. For general programs, verifiability and performance are competing goals; we argue that software dataplanes are different--we can write them in a way that enables verification and preserves performance. We present a verification tool that takes as input a software dataplane, written in a way that meets a given set of conditions, and (dis)proves that the dataplane satisfies crash-freedom, bounded-execution, and filtering properties. We evaluate our tool on stateless and simple stateful Click pipelines; we perform complete and sound verification of these pipelines within tens of minutes, whereas a state-of-the-art general-purpose tool fails to complete the same task within several hours.