SHSA: A method of network verification with stateful header space analysis

With the emergence of hybrid software-defined network (SDN) that contains switches and all kinds of middleboxes, there are a lot of obvious problems that have been brought up in verifying data plane consistency. However, recent study in network verification neglected the dynamic data plane verification induced by stateful middleboxes. To handle this limitation, we propose a new method, Stateful Header Space Analysis (SHSA), to verify reachability and detect loops in hybrid software-defined network with stateful middleboxes. Moreover, we optimize the validation process on the base of header space analysis (HSA) and enhance the scalability of our verification algorithm. To validate the applicability of SHSA, we implement four kinds of stateful middleboxes by Open vSwitch and simulate the hybrid network. The experimental results indicate that our method could verify the dynamic data plane accurately. Compared the time cost between SHSA and HSA in Stanford University's backbone network, results show that the efficiency of our method is 30 percent higher than the latter approximately.