Abstract Interpretation of Distributed Network Control Planes
Duration: 30 mins 19 secs
Share this media item:
Embed this media item:
Embed this media item:
About this item
Description: |
Gupta, A
Tuesday 11th May 2021 - 18:00 to 18:30 |
---|
Created: | 2021-05-17 13:01 |
---|---|
Collection: | Verified software: from theory to practice |
Publisher: | Isaac Newton Institute for Mathematical Sciences |
Copyright: | Gupta, A |
Language: | eng (English) |
Abstract: | The control plane of most computer networks runs distributed routing protocols that determine if and how traffic is forwarded. Errors in the configuration of network control planes frequently knock down critical online services, leading to financial losses for service providers and significant hardship for users. Validation and verification can help find network configuration errors but existing techniques scale poorly on large industrial networks. We explore the use of abstract interpretation for verifying configurations, and build a tool called ShapeShifter for reachability analysis. On a suite of 127 production networks from a large cloud provider, ShapeShifter accurately predicts reachability for all destinations for 95% of the networks and for most destinations for the remaining 5%. We also use abstract interpretation to facilitate a new "hijacking" analysis for the border gateway protocol (BGP), a globally-deployed routing protocol. (This is joint work with Ryan Beckett, Ratul Mahajan, and Dave Walker.) |
---|
Available Formats
Format | Quality | Bitrate | Size | |||
---|---|---|---|---|---|---|
MPEG-4 Video | 640x360 | 737.78 kbits/sec | 163.82 MB | View | Download | |
WebM | 640x360 | 282.01 kbits/sec | 62.65 MB | View | Download | |
iPod Video | 480x270 | 484.82 kbits/sec | 107.65 MB | View | Download | |
MP3 | 44100 Hz | 249.79 kbits/sec | 55.53 MB | Listen | Download | |
Auto * | (Allows browser to choose a format it supports) |