### Abstract

Modern networks achieve robustness and scalability by maintaining states on their nodes. These nodes are referred to as middleboxes and are essential for network functionality. However, the presence of middleboxes drastically complicates the task of network verification. Previous work showed that the problem is undecidable in general and EXPSPACE-complete when abstracting away the order of packet arrival. We describe a new algorithm for conservatively checking isolation properties of stateful networks. The asymptotic complexity of the algorithm is polynomial in the size of the network, albeit being exponential in the maximal number of queries of the local state that a middlebox can do, which is often small. Our algorithm is sound, i.e., it can never miss a violation of safety but may fail to verify some properties. The algorithm performs on-the fly abstract interpretation by (1) abstracting away the order of packet processing and the number of times each packet arrives, (2) abstracting away correlations between states of different middleboxes and channel contents, and (3) representing middlebox states by their effect on each packet separately, rather than taking into account the entire state space. We show that the abstractions do not lose precision when middleboxes may reset in any state. This is encouraging since many real middleboxes reset, e.g., after some session timeout is reached or due to hardware failure.

Original language | English (US) |
---|---|

Title of host publication | Static Analysis - 25th International Symposium, SAS 2018, Proceedings |

Editors | Andreas Podelski |

Publisher | Springer-Verlag |

Pages | 86-106 |

Number of pages | 21 |

ISBN (Print) | 9783319997247 |

DOIs | |

State | Published - Jan 1 2018 |

Event | 25th International Static Analysis Symposium, SAS 2018 - Freiburg, Germany Duration: Aug 29 2018 → Aug 31 2018 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 11002 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 25th International Static Analysis Symposium, SAS 2018 |
---|---|

Country | Germany |

City | Freiburg |

Period | 8/29/18 → 8/31/18 |

### Fingerprint

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Static Analysis - 25th International Symposium, SAS 2018, Proceedings*(pp. 86-106). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11002 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-99725-4_8

**Abstract Interpretation of Stateful Networks.** / Alpernas, Kalev; Manevich, Roman; Panda, Aurojit; Sagiv, Mooly; Shenker, Scott; Shoham, Sharon; Velner, Yaron.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Static Analysis - 25th International Symposium, SAS 2018, Proceedings.*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11002 LNCS, Springer-Verlag, pp. 86-106, 25th International Static Analysis Symposium, SAS 2018, Freiburg, Germany, 8/29/18. https://doi.org/10.1007/978-3-319-99725-4_8

}

TY - GEN

T1 - Abstract Interpretation of Stateful Networks

AU - Alpernas, Kalev

AU - Manevich, Roman

AU - Panda, Aurojit

AU - Sagiv, Mooly

AU - Shenker, Scott

AU - Shoham, Sharon

AU - Velner, Yaron

PY - 2018/1/1

Y1 - 2018/1/1

N2 - Modern networks achieve robustness and scalability by maintaining states on their nodes. These nodes are referred to as middleboxes and are essential for network functionality. However, the presence of middleboxes drastically complicates the task of network verification. Previous work showed that the problem is undecidable in general and EXPSPACE-complete when abstracting away the order of packet arrival. We describe a new algorithm for conservatively checking isolation properties of stateful networks. The asymptotic complexity of the algorithm is polynomial in the size of the network, albeit being exponential in the maximal number of queries of the local state that a middlebox can do, which is often small. Our algorithm is sound, i.e., it can never miss a violation of safety but may fail to verify some properties. The algorithm performs on-the fly abstract interpretation by (1) abstracting away the order of packet processing and the number of times each packet arrives, (2) abstracting away correlations between states of different middleboxes and channel contents, and (3) representing middlebox states by their effect on each packet separately, rather than taking into account the entire state space. We show that the abstractions do not lose precision when middleboxes may reset in any state. This is encouraging since many real middleboxes reset, e.g., after some session timeout is reached or due to hardware failure.

AB - Modern networks achieve robustness and scalability by maintaining states on their nodes. These nodes are referred to as middleboxes and are essential for network functionality. However, the presence of middleboxes drastically complicates the task of network verification. Previous work showed that the problem is undecidable in general and EXPSPACE-complete when abstracting away the order of packet arrival. We describe a new algorithm for conservatively checking isolation properties of stateful networks. The asymptotic complexity of the algorithm is polynomial in the size of the network, albeit being exponential in the maximal number of queries of the local state that a middlebox can do, which is often small. Our algorithm is sound, i.e., it can never miss a violation of safety but may fail to verify some properties. The algorithm performs on-the fly abstract interpretation by (1) abstracting away the order of packet processing and the number of times each packet arrives, (2) abstracting away correlations between states of different middleboxes and channel contents, and (3) representing middlebox states by their effect on each packet separately, rather than taking into account the entire state space. We show that the abstractions do not lose precision when middleboxes may reset in any state. This is encouraging since many real middleboxes reset, e.g., after some session timeout is reached or due to hardware failure.

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

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

U2 - 10.1007/978-3-319-99725-4_8

DO - 10.1007/978-3-319-99725-4_8

M3 - Conference contribution

SN - 9783319997247

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 86

EP - 106

BT - Static Analysis - 25th International Symposium, SAS 2018, Proceedings

A2 - Podelski, Andreas

PB - Springer-Verlag

ER -