A runtime verification system for Software Defined Networks.

Authors

Altukhov V.S., Chemeritskiy E.V., Podymov V.V., Zakharov V.A.

Abstract

We present a software toolset VERMONT (VERifying MONiTor) for runtime checking the consistency of Software Defined Network (SDN) configurations with formally specified invariants of Packet Forwarding Policies (PFPs). One of the main task of network engineering is to provide such a loading of SDN switches with forwarding rules as to guarantee its compliance with the PFP. VERMONT provides some automation to the solution of this task. Being installed in line with the control plane it 1) observes state changes of a network by intercepting the exchange of messages and commands between network switches and SDN controller, 2) builds an adequate formal model of a whole network, and 3) checks every event, such as installation, deletion, or modification of rules, port and switch up and down events, against a set of PFP invariants. Before retransmitting a network updating command to a switch VERMONT anticipates the result of its execution and checks the requirements of PFP. If a violation of some PFP invariant is detected then VERMONT blocks the change, alerts a network administrator, and gives some additional information to elucidate a possible source of an error. In this paper we discuss both mathematical and engineering issues of our toolset. We begin with defining a formal model of SDN and a formal language for PFP specification. After presenting the main algorithms used in VERMONT for SDN model building, model checking, and model modification, we describe the structure of VERMONT and the functionality of its components. Finally, we demonstrate the results of our experiments on the application of VERMONT to a real-life network.

Text of article

Keywords

runtime verification, formal specification, model checking, software defined network, controller, switch, packet forwarding relation, Binary Decision Diagram, network update

Edition

Proceedings of the International Conference "Tools & Methods of Program Analysis", TMPA-2014, 2014, Kostroma, KSTU, pp. 19-28.

Research Group

Theoretical Computer Science

All publications during 2014

All publications