Tata Institute of Fundamental Research
Network Verification -- When Clarke Meets Cerf
STCS Seminar
Speaker:
George Varghese (University of California Los Angeles
Department of Computer Science
4531C Boulter Hall
CA 90095
United States of America)
Organiser:
Piyush Srivastava
Date:
Thursday, 28 Dec 2017, 16:00 to 17:00
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
Surveys reveal that network outages are prevalent, and that many outages take hours to resolve, resulting in significant lost revenue. Many bugs are caused by errors in configuration files which are programmed using arcane, low-level languages, akin to machine code. Taking our cue from program and hardware verification, we suggest fresh approaches.
I will first describe a geometric model of network forwarding called Header Space. While header space analysis is similar to finite state machine verification, we exploit domain-specific structure to scale better than off-the shelf model checkers. Next, I show how to exploit physical symmetry to scale network verification for large data centers. While Emerson and Sistla showed how to exploit symmetry for model checking in 1996, they exploited symmetry on the logical Kripke structure.
While header space models allow us to verify the forwarding tables in routers, there are also routing protocols such as BGP that build the forwarding tables. We show to go from headerspace verification to what we call control space verification to proactively catch latent bugs in BGP configurations. I will end
with a vision for what we call Network Design Automation to build a suite of tools for networks inspired by the Electronic Design Automation Industry.
(With collaborators at CMU, Edinburgh, MSR, Stanford, and UCLA.)
| Speaker: | George Varghese (University of California Los Angeles Department of Computer Science 4531C Boulter Hall CA 90095 United States of America) |
| Organiser: | Piyush Srivastava |
| Date: | Thursday, 28 Dec 2017, 16:00 to 17:00 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
Surveys reveal that network outages are prevalent, and that many outages take hours to resolve, resulting in significant lost revenue. Many bugs are caused by errors in configuration files which are programmed using arcane, low-level languages, akin to machine code. Taking our cue from program and hardware verification, we suggest fresh approaches.
I will first describe a geometric model of network forwarding called Header Space. While header space analysis is similar to finite state machine verification, we exploit domain-specific structure to scale better than off-the shelf model checkers. Next, I show how to exploit physical symmetry to scale network verification for large data centers. While Emerson and Sistla showed how to exploit symmetry for model checking in 1996, they exploited symmetry on the logical Kripke structure.
While header space models allow us to verify the forwarding tables in routers, there are also routing protocols such as BGP that build the forwarding tables. We show to go from headerspace verification to what we call control space verification to proactively catch latent bugs in BGP configurations. I will end
with a vision for what we call Network Design Automation to build a suite of tools for networks inspired by the Electronic Design Automation Industry.
(With collaborators at CMU, Edinburgh, MSR, Stanford, and UCLA.)
I will first describe a geometric model of network forwarding called Header Space. While header space analysis is similar to finite state machine verification, we exploit domain-specific structure to scale better than off-the shelf model checkers. Next, I show how to exploit physical symmetry to scale network verification for large data centers. While Emerson and Sistla showed how to exploit symmetry for model checking in 1996, they exploited symmetry on the logical Kripke structure.
While header space models allow us to verify the forwarding tables in routers, there are also routing protocols such as BGP that build the forwarding tables. We show to go from headerspace verification to what we call control space verification to proactively catch latent bugs in BGP configurations. I will end
with a vision for what we call Network Design Automation to build a suite of tools for networks inspired by the Electronic Design Automation Industry.
(With collaborators at CMU, Edinburgh, MSR, Stanford, and UCLA.)