VeriCon: Towards Verifying Controller Programs in Software-Defined Networks
VeriCon: Towards Verifying Controller Programs in Software-Defined Networks
复制标题
DOI：
10.1145/2666356.2594317
复制
发表时间：
2014-06-01
影响因子：
--
通讯作者：
Valadarsky, Asaf
中科院分区：
文献类型：
--
作者：
Ball, Thomas;Bjorner, Nikolaj;Valadarsky, Asaf
软件定义网络（SDN）是用于操作和管理计算机网络的新范例。SDN通过独立于网络硬件运行的“控制器”软件实现对网络设备的逻辑集中控制，并且可以被视为网络操作系统。网络运营商可以在控制器上运行内部和第三方SDN程序（通常称为应用程序）。例如，在一个实施例中，指定路由和访问控制策略。SDN开辟了应用形式化方法来证明计算机网络正确性的可能性。事实上，最近已经投入了大量的精力来应用有限状态模型检查来检查SDN程序的行为是否正确。然而，一般来说，将这些方法扩展到大型网络具有挑战性，而且它们无法保证不出现错误。我们提出VeriCon，这是第一个用于验证SDN程序在所有可接受的拓扑结构上以及所有可能的（无限）网络事件序列上都是正确的系统。VeriCon或者确认控制器程序在所有可接受的网络拓扑上的正确性，或者输出一个具体的反例。VeriCon使用一阶逻辑来指定可接受的网络拓扑和所需的网络范围的不变量，然后使用Z3实现经典的Floor-Hoare-Dijkstra演绎验证。我们的初步经验表明，VeriCon能够快速验证正确性，或识别错误，为一个简单的核心SDN程序的大剧目。VeriCon是组合的，从某种意义上说，它验证任何单个网络事件w.r.t.执行的正确性。指定的不变量，因此可以扩展以处理大型程序。为了减轻程序员指定归纳不变量的负担，VeriCon包括一个单独的推断不变量的程序，这是有效的简单的控制器程序。我们认为VeriCon是通往实用机制的第一步，用于验证SDN程序的网络范围不变量。
Software-defined networking (SDN) is a new paradigm for operating and managing computer networks. SDN enables logically-centralized control over network devices through a "controller" software that operates independently from the network hardware, and can be viewed as the network operating system. Network operators can run both inhouse and third-party SDN programs (often called applications) on top of the controller, e. g., to specify routing and access control policies. SDN opens up the possibility of applying formal methods to prove the correctness of computer networks. Indeed, recently much effort has been invested in applying finite state model checking to check that SDN programs behave correctly. However, in general, scaling these methods to large networks is challenging and, moreover, they cannot guarantee the absence of errors.We present VeriCon, the first system for verifying that an SDN program is correct on all admissible topologies and for all possible (infinite) sequences of network events. VeriCon either confirms the correctness of the controller program on all admissible network topologies or outputs a concrete counterexample. VeriCon uses first-order logic to specify admissible network topologies and desired network-wide invariants, and then implements classical Floyd-Hoare-Dijkstra deductive verification using Z3. Our preliminary experience indicates that VeriCon is able to rapidly verify correctness, or identify bugs, for a large repertoire of simple core SDN programs. VeriCon is compositional, in the sense that it verifies the correctness of execution of any single network event w.r.t. the specified invariant, and can thus scale to handle large programs. To relieve the burden of specifying inductive invariants from the programmer, VeriCon includes a separate procedure for inferring invariants, which is shown to be effective on simple controller programs. We view VeriCon as a first step en route to practical mechanisms for verifying network-wide invariants of SDN programs.