Actor-based model checking for software-defined networks

DOI10.1016/J.JLAMP.2020.100617MaRDI QIDQ1996852zbMATH OpenOpenAlexFDO

Authors Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio, Matteo Sammartino, Alexandra Silva

Publication date 26 February 2021

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2001.10022, https://discovery.ucl.ac.uk/id/eprint/10117568/

zbMATH Keywords

actor-based modellingconcurrencymodel checkingsoftware-defined networksverification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Software-Defined Networking (SDN) is a networking paradigm that has become increasingly popular in the last decade. The unprecedented control over the global behavior of the network it provides opens a range of new opportunities for formal methods and much work has appeared in the last few years on providing bridges between SDN and verification. This article advances this research line and provides a link between SDN and traditional work on formal methods for verification of concurrent and distributed software---actor-based modelling. We show how SDN programs can be seamlessly modelled using emph{actors}, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops. Our model checker for SDN networks is available through an online web interface, that also provides the SDN actor-models for a number of well-known SDN benchmarks.

Recommendations

• SDN-actors: modeling and verification of SDN programs
• Towards model checking real-world software-defined networks
• SAT based verification of network data planes
• NetKAT -- a formal system for the verification of networks
• Model checking data flows in concurrent network updates

Cites work

• A coalgebraic decision procedure for NetKAT
• A Complete Guide to the Future
• A program logic for concurrent objects under fair scheduling
• Constrained dynamic partial order reduction
• Context-sensitive dynamic partial order reduction
• Defining conditional independence using collapses
• Dynamic partial-order reduction for model checking software
• Modeling and efficient verification of wireless ad hoc networks
• Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
• Netkat, semantic foundations for networks
• Peephole Partial Order Reduction
• SDN-actors: modeling and verification of SDN programs
• Statistical model checking for composite actor systems
• Tractable refinement checking for concurrent objects

Cited in

(5)

• SDN-actors: modeling and verification of SDN programs
• From symbolic constraint automata to Promela
• Towards model checking real-world software-defined networks
• Model checking data flows in concurrent network updates
• SAT based verification of network data planes

Describes a project that uses

Uses Software

• PMaude
• ABS
• Syco
• Anteater
• NetKAT
• VeriCon
• VeriFlow
• Kuai

This page was built for publication: Actor-based model checking for software-defined networks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1996852)