Emerging Trends in Network Design and Verification
Explore the evolution of network design from manual configurations to custom networks and software-defined solutions. Discover the challenges facing current networks and the potential for optimizing network performance through innovative approaches like P4 and SDNs. Delve into the intersection of digital hardware design and network automation, with a focus on formal methods that enhance testing, verification, and synthesis processes.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
VERIFICATION, SYNTHESIS, AND THE CREATIVE HABIT: COURSE REVIEW George Varghese 1
Problem with Networks today Shortest Path D S Manual Configurations: Managers override default shortest paths for security, load balancing, and economic reasons Data Plane + Control Plane: Vendor-specific knobs in both Problem: Manually programming individual routers to implement global policy leads to cloud failures 2
Networks Tomorrow Online services latency, cost sensitive Merchant Silicon Build your own router Rise of Data centers Software defined Networks (SDNs) Custom networks Program custom design routing P4 (next generation SDN) redefine hardware forwarding at runtime Opportunity to custom design networks to optimize goal. Potential simplifications but hard to get right
Digital Hardware Design as Inspiration? Specification Specification Testbench & Vectors Functional Description (RTL) Policy Language, Semantics Testing Functional Verification Logical Synthesis Verification Synthesis Static Timing Performance verification? Network Topology Design Static checking (local checks) Place & Route Design Rule Checking (DRC) Layout vs Schematic (LVS) Parasitic Extraction Wiring Checkers Manufacture & Validate Dynamic checkers/ debuggers Interference estimation? Electronic Design Automation (McKeown SIGCOMM 2012) Network Design Automation (NDA)?
This Courses Slice of NDA Specification Policy Language, Semantics Testing Verification Synthesis Won t discuss debugging, very little of run-time verification. Mostly interested in where formal methods can help
This Courses Slice of NDA Specification CTL, NoD, Klee Assert Policy Language, Semantics Propane ATPG Testing Data Plane: Anteater, VeriFlow, HSA, Atomic Predicates, Control Plane: BatFish, rcc, ERA Verification (e.g. reachabilty) Synthesis (e.g. forwarding) Did: Propane Missing: One big switch, NetKAT, FlowLog Didn t discuss debugging, very little of run-time verification. Focus on applications of formal methods
Road Map of Course Introduction to Networking & Formal Methods Data Plane Verification One counterexample All counterexamples Optimizations Adding Functionality Data Plane Testing Control Plane Testing and Synthesis
Formal Methods Need to have: Examples: a modelling language for networks state machines, Datalog, HSA, ERA a specification language for correctness CTL, NoD, NetPlumber a system, data structures to encode program and data and a solver Hassel + Difference of Cubes, Atomic Predicates + BDDs
Beware the Black Box Run time in seconds Model Checker SMT All Solutions NoD HSA Stanford Unreach 12.2 0.1 2.1 0.1 Stanford Reachable 13.7 1121 5.9 0.9 Stanford Loop 11.7 290 3.9 0.2 Cloud Time out Time out 15.7 - Cloud 2 8.5 Time out 4.8 - Atomic Predicates and use of Symmetries does even better
Verification Tasks [Fayazbakhsh 15] Program types: ????????????: ?????? ??? ??? ?????????: ??? ?????? ????????? DP tasks for fixed snapshot of FIBS ? ?: ??????: (?,????????? ?,? ) CP verifiers for fixed configuration ? (Batfish) ?,?: (?,?????????(????????????(?,?),?))) CP verifiers for CP only as in ARC ?: (???????????? ?,? )
Introduction to Formal Methods Data Plane Verification One counterexample All counterexamples Optimizations Adding Functionality Control Plane Testing and Synthesis DATA PLANE VERIFICATION: IF ONE COUNTEREXAMPLE SUFFICES
Historically: Encode networks using existing verification engines [Xie05] Theoretical reachability algorithm [AlShaer09]: Model checking approach [Mai11]: SAT Based Anteater If 1 counterexample + small networks, reusing existing tools works fine. Only clever encoding
Introduction to Formal Methods Data Plane Verification One counterexample All counterexamples Optimizations Adding Functionality Data Plane Testing Control Plane Testing and Synthesi DATA PLANE VERIFICATION: ALL COUNTEREXAMPLES
Why all examples? Easier to see which rule caused counterexample. Easier to do incremental verification However, we have now gone from SAT to AllSAT which modern SAT solvers are not optimized for. Fortunately, we can exploit the domain structure to do quite well.
All Solutions: Header Space [Kazemian 12] Step 1 - Model a packet, based on its header bits, as a point in {0,1}L space the Header Space Two abstractions: 1. All layers collapsed into a flat sequence of bits 2. Wildcards ignore header bits irrelevant to forwarding Two technical ideas: 1. Ternary Algebra 2. Difference of cubes Header 0xxxx0101xxx Data 01110011 1 L
Introduction to Formal Methods Data Plane Verification One counterexample All counterexamples Optimizations Adding Functionality Data Plane Testing Control Plane Testing & Synthesis DATA PLANE VERIFICATION: OPTIMIZATIONS
Scaling to Large Networks Exploit: Incrementality Only small parts of program change on rule change Equivalence Classes Number of header equivalence classes is small Symmetries Many rules and boxes are repeated (redundancy) [NetPlumber] [Atomic Predicates] [Plotkin 15]
Exploiting incrementality: NetPlumber [Kazemian 13] S ... ... ... ... ? ... ... ... ... VERIFYING CHANGES BY SDN CONTROLLERS BEFORE THEY TAKE EFFECT 18
Atomic Predicates Intuition [Yang 13] From run-time compression via Difference of cubes to precomputed compression via Ai Computes pairwise intersection of router and ACL guards to generate Ai using BDDs Then rewrites forwarding rules using a simple set of integer labels for each Symbolic propagation propagating sets of integers. Fast. No rule matching, less space Analog to MPLS versus IP forwarding!
Exploiting Symmetry [Plotkin15] Symmetry Modularity Can exploit regularities in rules and topology (not headers): Symmetry Theorem: Can reduce fat tree to thin tree using a simulation and verify reachability cheaply in latter Modularity Theorem: reuse of parts of switching network
Introduction to Formal Methods Data Plane Verification One counterexample All counterexamples Optimizations Adding Functionality Data Plane Testing Control Plane Verification Control Plane Testing Synthesis, Semantics DATA PLANE VERIFICATION: ADDING FUNCTIONALITY
Improving Functionality Support for dynamic networks and imperfect specifications (NOD) HSA only static specifications, static routers Support for Quantities (Sung09) HSA only verifies Boolean properties. Did not do Support for Stateful boxes HSA does not handle stateful boxes like NAT etc. Work by Berkeley and CMU. Did not do.
Dynamic Networks: Network Optimized Datalog [Lopes15] Classical model checking provides languages based on temporal logic to specify a variety of properties Header Space hard codes some properties Classical verification tools compute only 1 solution Datalog computes all but was inefficient. Had to redo Datalog engine. Datalog allows some dynamism. But for more have to model control plane a la Batfish Datalog nearly as fast as HSA but much more expressive Included in Z3. Being used to check Azure configurations
Introduction to Formal Methods Data Plane Verification Data Plane Testing Control Plane Testing and Synthesis DATA PLANE TESTING
Symbolic Execution Methods Want to push program to as many states as possible: maximize coverage Random (Fuzz testing) useful but can do better. Idea: Encode program as a decision tree. Try to cover all paths in decision tree. Conjunction of symbolic predicates for each path. Cover finding concrete solution via SMT.
ATPG vs Klee [Zheng 13] Monitor the data plane by sending test packets. Maximum rule coverage (like Klee: rules lines) Minimize number of packets required (like Klee: packets test cases) Constraints on terminal ports and headers of test packets (unlike Klee) Once error is detected, localize it (unlike Klee more like tomography)
Software Data Plane Verification [Dobrescu 14] Verifies actual code of Click software router. Checks for new physical bugs (e.g., crash freedom, loops) using symbolic testing. No path explosion: since router is a pipeline only compose potentially buggy path fragments Use verified data structures (no pointers). Tradeoff verification ease with runtime cost. Found bugs: e.g., IP option + fragmentation.
Introduction to Formal Methods Data Plane Verification Data Plane Testing Control Plane Testing and Synthesis CONTROL PLANE TESTING
Earlier Control Plane Work BGP Loops Possible [Govindan, Griffin-Wilfong] Sufficient Conditions for Avoiding Loops [Gao-Rexford] Route redistribution can cause loops [Le 2008] But based on human analysis and proofs. We studied tools for automated analysis
Cellular Protocol Testing [Li et al] Cellular Control Plan but tests for protocol and implementation bugs not config bugs Modest checking via SPIN to suggest buggy use cases and experiments with phones and Qualcomm debugger to confirm Bugs in feature interaction (e.g., 3G to 4G) Config bugs in later papers! Similar to IP.
Static Checking BGP Configs: RCC [Feamster 05] Checks BGP configs for path visibility, validity Example, route reflector configuration bugs Route r (not visible to all) Route s (visible to all)
Testing Across Announcements [ERA] Batfish:symbolic simulation of 1 environment ERA looks for route reachability and computes a maximal announcement that finds bugs Seems to work to find an interesting set of bugs (backup equivalence, valley free etc) Bugs correspond almost 1-1 with data plane bugs (loops, blackholes) but for announcements
Config Synthesis [Propane] New language for route preferences based on ordered regular expressions Regular expression state machine crossproduct with topology encode transitions with communities, LPs Regret freedom encodes choices that are oblivious to any failure. May be too strong.
Config Verification [Minesweeper] Encodes stable path problem in SAT for routes and usual data plane reachability in SAT Uses a graph to encode the network to model redistribution, output & input filters etc. Optimizations like slicing and transferring prefix matching in CP to inequalities in DP. Scales but only 1 counterexample on failure
Research ideas? from research in real networks via exemplars 10* P1 1* P2 PREFIX MATCH 10010 IP Router 01A1A2 P1 . . . EXACT MATCH 01A1A2 MAC Bridge 5 P1,Pop 5 . . . INDEXED LOOKUP 5, 6 MPLS Switch ESSENTIAL INSIGHT FOR OPENFLOW. USE SAME INSIGHT IN HSA FOR UNDERSTANDING EXISTING PROTOCOLS. SIMILARLY MPLS ATOMIC PREDICATES 36
Research ideas? from PL and Hardware Verification via exemplars Earlier Exemplar Network Verification Ternary Simulation, Symbolic Execution (Dill 01, Hardware) Header Space Analysis (HSA) Certified Development of an OS Sel4 [Klein 09] Correct by construction BGP Configs [Propane] Static Checkers for Programs [Lint] Static Checking for BGP (Feamster rcc ) Exploit Symmetry in Model Checking [Sistla] Exploit Symmetry in Data Center Verification (Plotkin15) Can choose either analysis of existing (e.g., Veriflow) or clean slate Approaches based on synthesis. Both have a place
Exemplars: Food for thought? What are Network Verification analogs of: Abstract Interpretation (replacing complex state by a simple state) CEGAR (counterexample driven refinement) Interpolants Strong typing in Language Design Wiring checkers in Chip Design
Scaling? Exploit Domain Structure Technique Structure exploited Header Space (HSA) Limited negation, no loops, small equivalence classes Net Plumber Network Graph, rule dependencies structure ATPG (Testing) Network graph limits size of state space compared to KLEE Symmetry Exploiting Known symmetries because of design (vs on logical structures) Scope for Interdisciplinary work between PL, Hardware CAD, Verification Community and Networking Researchers
No Specifications? Use Beliefs Paper Example Beliefs Bugs as Deviant Behavior [Engler 01] Dereferencing Pointer P that could be NULL is a bug Routing Config Checker (RCC) [Feamster rcc] Routes from a Peer should not be re-advertised to another peer Network Optimized Datalog [NOD] Customer VMs should not be able to access router ports Batifsh Control Plane Testing Equal cost routes should have equivalent reachabiliyt
Dont know how Leverage code SMT: Z3 BDD packages: (BuDDy) Model checking: SPIN, nuSmv/nuXmv Network Specific verification: Hassel, Veriflow, NoD, Atomic Predicates Datasets: Stanford, Cloud (NoD), Internet2 Symbolic Test Generation: KLEE, DART, SAGE Proof Assistants: Coq, Isabelle Known to be available for download
Lessons Summarized 1. What research? Via exemplars from PL/HW 2. What research? Via exemplars from networks 3. Scaling? Exploit domain structure 4. Lack of specifications? Use Beliefs 5. Don t know how? Leverage available code 6. Network Design Automation? Learn from EDA
Be Creative 1. Know your creative DNA. Build Teams 2. Harness your memory. Connect. Metaphor. 3. Ask Na ve Questions. 4. Scratch for ideas at the start. 5. Find a spine 6. Accidents will happen. Be open to new outcomes. 7. Use skill and persistence to finish the work!
What made me happy 1. Each of your insights during discussions 2. Your performance in the test 3. The idea of using verification for business processes 4. Many of your other ideas. Will try and return with your finals.
Conclusion Inflection Point: Rise of services, data centers, Software Defined Networks Ideas: Creatively adapt Verification ideas to domain Intellectual Opportunity: Rethink existing techniques exploiting domain structure Systems Opportunity Change way large operational networks are built Lot more than Verification and Formal Methods (have to add debugging, run-time checks etc.) but EDA suggests this is an Essential foundation 45
