Some complexity results for stateful network verification

Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner

Research output: Contribution to journalArticle

Abstract

In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behaviour depends on a mutable internal state. Firewalls and load balancers are typical examples of stateful middleboxes. This work addresses the complexity of verifying safety properties, such as isolation, in networks with finite-state middleboxes. Unfortunately, we show that even in the absence of forwarding loops, reasoning about such networks is undecidable due to interactions between middleboxes connected by unbounded ordered channels. We therefore abstract away channel ordering. This abstraction is sound for safety, and makes the problem decidable. Specifically, safety checking becomes EXPSPACE-complete in the number of hosts and middleboxes in the network. To tackle the high complexity, we identify two useful subclasses of finite-state middleboxes which admit better complexities. The simplest class includes, e.g., firewalls and permits polynomial-time verification. The second class includes, e.g., cache servers and learning switches, and makes the safety problem coNP-complete. Finally, we implement a tool for verifying the correctness of stateful networks.

Original languageEnglish (US)
JournalFormal Methods in System Design
DOIs
StateAccepted/In press - Jan 1 2019

Fingerprint

Safety
Firewall
Servers
Switches
Polynomials
Acoustic waves
Cache
Isolation
Correctness
Switch
Polynomial time
Server
Reasoning
Traffic
Internal
Interaction
Class

Keywords

  • Channel systems
  • Complexity bounds
  • Middleboxes
  • Petri nets
  • Safety verification
  • Stateful networks

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture

Cite this

Alpernas, K., Panda, A., Rabinovich, A., Sagiv, M., Shenker, S., Shoham, S., & Velner, Y. (Accepted/In press). Some complexity results for stateful network verification. Formal Methods in System Design. https://doi.org/10.1007/s10703-018-00330-9

Some complexity results for stateful network verification. / Alpernas, Kalev; Panda, Aurojit; Rabinovich, Alexander; Sagiv, Mooly; Shenker, Scott; Shoham, Sharon; Velner, Yaron.

In: Formal Methods in System Design, 01.01.2019.

Research output: Contribution to journalArticle

Alpernas, K, Panda, A, Rabinovich, A, Sagiv, M, Shenker, S, Shoham, S & Velner, Y 2019, 'Some complexity results for stateful network verification', Formal Methods in System Design. https://doi.org/10.1007/s10703-018-00330-9
Alpernas K, Panda A, Rabinovich A, Sagiv M, Shenker S, Shoham S et al. Some complexity results for stateful network verification. Formal Methods in System Design. 2019 Jan 1. https://doi.org/10.1007/s10703-018-00330-9
Alpernas, Kalev ; Panda, Aurojit ; Rabinovich, Alexander ; Sagiv, Mooly ; Shenker, Scott ; Shoham, Sharon ; Velner, Yaron. / Some complexity results for stateful network verification. In: Formal Methods in System Design. 2019.
@article{641edbafee7346ddb1de6fb822e8e330,
title = "Some complexity results for stateful network verification",
abstract = "In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behaviour depends on a mutable internal state. Firewalls and load balancers are typical examples of stateful middleboxes. This work addresses the complexity of verifying safety properties, such as isolation, in networks with finite-state middleboxes. Unfortunately, we show that even in the absence of forwarding loops, reasoning about such networks is undecidable due to interactions between middleboxes connected by unbounded ordered channels. We therefore abstract away channel ordering. This abstraction is sound for safety, and makes the problem decidable. Specifically, safety checking becomes EXPSPACE-complete in the number of hosts and middleboxes in the network. To tackle the high complexity, we identify two useful subclasses of finite-state middleboxes which admit better complexities. The simplest class includes, e.g., firewalls and permits polynomial-time verification. The second class includes, e.g., cache servers and learning switches, and makes the safety problem coNP-complete. Finally, we implement a tool for verifying the correctness of stateful networks.",
keywords = "Channel systems, Complexity bounds, Middleboxes, Petri nets, Safety verification, Stateful networks",
author = "Kalev Alpernas and Aurojit Panda and Alexander Rabinovich and Mooly Sagiv and Scott Shenker and Sharon Shoham and Yaron Velner",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/s10703-018-00330-9",
language = "English (US)",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer Netherlands",

}

TY - JOUR

T1 - Some complexity results for stateful network verification

AU - Alpernas, Kalev

AU - Panda, Aurojit

AU - Rabinovich, Alexander

AU - Sagiv, Mooly

AU - Shenker, Scott

AU - Shoham, Sharon

AU - Velner, Yaron

PY - 2019/1/1

Y1 - 2019/1/1

N2 - In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behaviour depends on a mutable internal state. Firewalls and load balancers are typical examples of stateful middleboxes. This work addresses the complexity of verifying safety properties, such as isolation, in networks with finite-state middleboxes. Unfortunately, we show that even in the absence of forwarding loops, reasoning about such networks is undecidable due to interactions between middleboxes connected by unbounded ordered channels. We therefore abstract away channel ordering. This abstraction is sound for safety, and makes the problem decidable. Specifically, safety checking becomes EXPSPACE-complete in the number of hosts and middleboxes in the network. To tackle the high complexity, we identify two useful subclasses of finite-state middleboxes which admit better complexities. The simplest class includes, e.g., firewalls and permits polynomial-time verification. The second class includes, e.g., cache servers and learning switches, and makes the safety problem coNP-complete. Finally, we implement a tool for verifying the correctness of stateful networks.

AB - In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behaviour depends on a mutable internal state. Firewalls and load balancers are typical examples of stateful middleboxes. This work addresses the complexity of verifying safety properties, such as isolation, in networks with finite-state middleboxes. Unfortunately, we show that even in the absence of forwarding loops, reasoning about such networks is undecidable due to interactions between middleboxes connected by unbounded ordered channels. We therefore abstract away channel ordering. This abstraction is sound for safety, and makes the problem decidable. Specifically, safety checking becomes EXPSPACE-complete in the number of hosts and middleboxes in the network. To tackle the high complexity, we identify two useful subclasses of finite-state middleboxes which admit better complexities. The simplest class includes, e.g., firewalls and permits polynomial-time verification. The second class includes, e.g., cache servers and learning switches, and makes the safety problem coNP-complete. Finally, we implement a tool for verifying the correctness of stateful networks.

KW - Channel systems

KW - Complexity bounds

KW - Middleboxes

KW - Petri nets

KW - Safety verification

KW - Stateful networks

UR - http://www.scopus.com/inward/record.url?scp=85059783642&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85059783642&partnerID=8YFLogxK

U2 - 10.1007/s10703-018-00330-9

DO - 10.1007/s10703-018-00330-9

M3 - Article

AN - SCOPUS:85059783642

JO - Formal Methods in System Design

JF - Formal Methods in System Design

SN - 0925-9856

ER -