Blogs (9) >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Thu 3 Nov 2016 16:55 - 17:20 at Matterhorn 1 - Program Modeling and Learning Chair(s): Ondřej Lhoták

Internet Service Providers (ISPs) use the Border Gateway Protocol (BGP) to announce and exchange routes for de- livering packets through the internet. ISPs must carefully configure their BGP routers to ensure traffic is routed reli- ably and securely. Correctly configuring BGP routers has proven challenging in practice, and misconfiguration has led to worldwide outages and traffic hijacks. This paper presents Bagpipe, a system that enables ISPs to declaratively express BGP policies and that automatically verifies that router configurations implement such policies. The novel initial network reduction soundly reduces policy verification to a search for counterexamples in a finite space. An SMT-based symbolic execution engine performs this search efficiently. Bagpipe reduces the size of its search space using predicate abstraction and parallelizes its search using symbolic variable hoisting. Bagpipe's policy specification language is expressive: we expressed policies inferred from real AS configurations, policies from the literature, and policies for 10 Juniper TechLibrary configuration scenarios. Bagpipe is efficient: we ran it on three ASes with a total of over 240,000 lines of Cisco and Juniper BGP configuration. Bagpipe is effective: it revealed 19 policy violations without issuing any false positives.

Thu 3 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:40 - 17:20
Program Modeling and LearningOOPSLA at Matterhorn 1
Chair(s): Ondřej Lhoták University of Waterloo
15:40
25m
Talk
Computing Repair Alternatives for Malformed Programs using Constraint Attribute GrammarsAEC
OOPSLA
Friedrich Steimann Fernuniversität, Jörg Hagemann Fernuniversität in Hagen, Bastian Ulke Fernuniversität in Hagen
DOI Media Attached
16:05
25m
Talk
Probabilistic Model for Code with Decision Trees
OOPSLA
Veselin Raychev ETH Zurich, Switzerland, Pavol Bielik , Martin Vechev ETH Zurich
DOI
16:30
25m
Talk
Ringer: Web Automation by DemonstrationAEC
OOPSLA
Shaon Barman UC Berkeley, Sarah E. Chasins University of California, Berkeley, Rastislav Bodík University of Washington, USA, Sumit Gulwani Microsoft Research
DOI Media Attached
16:55
25m
Talk
Scalable Verification of Border Gateway Protocol Configurations with an SMT SolverAEC
OOPSLA
Konstantin Weitz University of Washington, Doug Woos University of Washington, Emina Torlak University of Washington, Michael D. Ernst University of Washington, Arvind Krishnamurthy University of Washington, Zachary Tatlock University of Washington, Seattle
DOI Media Attached