Loading...
Please wait, while we are loading the content...
Similar Documents
SymNet: static checking for stateful networks
| Content Provider | ACM Digital Library |
|---|---|
| Author | Popovici, Matei Stoenescu, Radu Negreanu, Lorina Raiciu, Costin |
| Abstract | Today's networks deploy many stateful procesing boxes ranging from NATs to firewalls and application optimizers: these boxes operate on packet flows, rather than individual packets. As more and more middleboxes are deployed, understanding their composition is becoming increasingly difficult. Static checking of network configurations is a promising approach to help understand whether a network is configured properly, but existing tools are limited as they only support stateless processing. We propose to use symbolic execution---a technique prevalent in compilers---to check network properties more general than basic reachability. The key idea is to track the possible values for specified fields in the packet as it travels through a network. Each middlebox or router will impose constraints on certain fields of the packet via forwarding actions, packet modifications and filtering. The symbolic approach also allows us to model middlebox per-flow state in a scalable way. We have implemented this technique in a tool we call SymNet and conducted preliminary evaluation. Early results show SymNet scales well and models basic stateful middleboxes, opening the possibility of analyzing complex stateful middlebox behaviours. |
| Starting Page | 31 |
| Ending Page | 36 |
| Page Count | 6 |
| File Format | |
| ISBN | 9781450325745 |
| DOI | 10.1145/2535828.2535835 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2013-12-09 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Stateful middleboxes Static analysis Symbolic execution |
| Content Type | Text |
| Resource Type | Article |
