Download

Abstractions for Model Checking SDN Controllers

Upload
0
Embed
Share
Upload and view presentations on any device and embed the player to your website! --- > >
Upload PPT
Upload PPT

Download this Presentation

carmen

2021-10-12 published at Spiritual/ Inspirational category

Presentation Transcript

1.Abstractions for Model CheckingSDN Controllers Divjyot Sethi, Srinivas Narayana, Prof. Sharad Malik Princeton University
2.Traditional Networking Forwarding data plane Mapping used for forwarding packets. Distributed control plane Logic used to update the mapping. Talk OSPF, RIP, BGP, etc. Swt2 Swt1 Swt3 Challenges: - Difficult to get right. - Inflexible for novel ideas. - No clean abstractions for implementing control.
3.A Fundamental Shift in Network Design Switches programmed by controller by installing rules Controller Swt2 Swt3 Swt1 Talk OSPF, RIP, BGP, etc. Swt2 Swt3 Swt1 Distributed Control Centralized Control General purpose software Centralized control simplifies design and innovation However, an Achilles heel for correctness.
4.Problem: Bugs in Centralized Control? Security leaks: packet sent to an untrusted host. Network loops: packet looping around in network. Link overload and data center outage. Downtime cost: ~$1 million per outage! (www.informationweek.com) AWS service commitment: Amazon EC2 and Amazon availability at least 99.95%
5.Challenges in Verification Large number of packets alive in network. Large buffer state. Large number of rules installed in switches. Large network state. Large topology size. Routing Table Port1: inPkt.src = Host1 Port2: inPkt.src = Host3 Port3: inPkt.src = Hostk Portp: inPkt.src = Hostr Portq: inPkt.src = Hosta outPort(inPkt) = Controller Swt2 Swt3 Swt1 H1 H2 pktc pkt1 pkt4 pkt3 pkt2
6.Overview Existing approaches and problem statement Abstraction on Stateful firewall Experimental case studies Stateful firewall Learning switch Conclusions
7.Overview Existing approaches and problem statement Abstraction on Stateful firewall Experimental case studies Stateful firewall Learning switch Conclusions
8.Verifying Software Defined Networks: Existing Approaches Network state evolves from configuration (switch rules) to configuration as controller updates the rules during transient phase. Controller Updates Controller Updates Configuration 1 Configuration 2 Configuration 3 Transient Phase Transient Phase Category 1: Verify just one configuration - Symbolic simulation[Kazemian et al. NSDI’12] Reduction to SAT [S. Zhang et al. ATVA’12, H. Mai SIGCOMM’ 11] Model Checking [E. Al-Shaer SafeConfig’10] Problem: verifies just one snapshot!
9.Verifying Software Defined Networks: Existing Approaches Category 2: Incremental verification, i.e., verify all snapshots [Kazemian et al. NSDI’13, A. Khurshid et al. NSDI’12] Problem: property may be violated in transient phase! Network state evolves from configuration (switch rules) to configuration as controller updates the rules during transient phase. Controller Updates Controller Updates Configuration 1 Configuration 2 Configuration 3 Transient Phase Transient Phase
10.Verifying Software Defined Networks: Existing Approaches Category 3: Full formal verification of Controller - NICE (M. Canini NSDI’12), FlowLog (T. Nelson HotSDN’13) Problem: handle only a bounded number of packets! Runtime grows exponentially with increasing packets. Can’t guarantee properties like security as checked for small number of packets. Network state evolves from configuration (switch rules) to configuration as controller updates the rules during transient phase. Controller Updates Controller Updates Configuration 1 Configuration 2 Configuration 3 Transient Phase Transient Phase
11.Focus of this Work Full formal verification of Controller using model checking. Extend NICE with abstractions to handle an unbounded number packets. Network state evolves from configuration (switch rules) to configuration as controller updates the rules during transient phase. Controller Updates Controller Updates Configuration 1 Configuration 2 Configuration 3 Transient Phase Transient Phase
12.Overview Existing approaches and problem statement Abstraction on Stateful firewall Experimental case studies Stateful firewall Learning switch Conclusions
13.Stateful Firewall Firewall rules: H1 can contact H2 or H3 H2/H3 can contact H1, only if H1 has already contacted them. If H2/H3 initiates contact first, it must be blocked. Property: If H2 never contacts H1 first, it does not get blocked. S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Host Internet Hosts Firewall Controller H3 p3
14.Abstraction for Unbounded Packets: Data State Abstraction Key insight: properties of interest are per-packet properties. - For example a packet from one host cannot reach another. S1 S2 H1 H2 Controller H3 pktc pkt1 pkt3 pkt2 S1 S2 H1 H2 Controller H3 pktc pkte pkte pkte
15.Abstraction for Large Switch State: Network State Abstraction S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Host Internet Hosts Firewall Controller H3 p3 Routing Table p1: pkt.dst = H1 p2: pkt. dst = H2 p3: pkt. dst = H3 output port(pkt) =
16.Abstraction for Reducing SwitchState: Leveraging Data State Abstraction S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Host Internet Hosts Firewall Controller H3 p3 Abstracted Routing Table p1: pkt.dst = H1 p2: pkt. dst = H2 non-det: pkt. dst != {H1 or H2} output port(pkt) = pktc pktc.src = H1 pktc.dst = H2
17.Overview Existing approaches and problem statement Abstraction on Stateful firewall Experimental case studies Stateful firewall Learning switch Conclusions
18.Stateful Firewall S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Internet Firewall Controller Verified a Murphi model of the firewall with a single host H2. - Found a bug: H2 replies to H1 but still gets blocked! Experiments were done on a 2.40 GHz Intel Core 2 Quad processor, 3.74 GB RAM.
19.Stateful Firewall: Race Condition S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Internet Firewall Controller H1 sends a packet pkt1 to H2 pkt1
20.Stateful Firewall: Race Condition S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Internet Firewall Controller pkt1 Notification Switch S1 notifies the controller.
21.Stateful Firewall: Race Condition S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Internet Firewall Controller Packet is also forwarded by S1, to S2 which sends it to H2 Notification pkt1
22.Stateful Firewall: Race Condition S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Internet Firewall Controller Host H2 replies with packet pkt2. Notification pkt2
23.Stateful Firewall: Race Condition S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Internet Firewall Controller Switch S2 notifies Controller about pkt2. Notification pkt2 Notification
24.Stateful Firewall: Race Condition S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Internet Firewall Controller Notification Notification If notification of S1 reaches after S2, Controller thinks that H2 contacted first and so is an attacker! H2 gets erroneously blocked! Bug detected in 0.13 sec with 482 states
25.Stateful Firewall: Bug Fix S1 S2 H1 H2 p2 p1 p2 p1 Enterprise Internet Firewall Controller S1 waits for Controller to acknowledge notification before forwarding packet pkt1 to H2. - Proved correctness for an unbounded number of packets in this case. Notification pkt1 Correctness proof for the bug free case with unbounded number of packets in 0.19 sec with 613 states
26.Learning Switch Controller Swt2 Swt3 HstA HstB HstC pkt Swt1 1 2 3 When a packet arrives at a switch at an input port: Switch learns its source host is connected to that port. Uses this information to route future packets efficiently.
27.Learning Switch: Bug Controller Swt2 Swt3 HstA HstB HstC Swt1 1 2 3 Switches may learn routing information such that packets get stuck in a loop! Loop was found in 0.1 sec with 159 states explored.
28.Learning Switch: Bug Fix Controller Swt2 Swt3 HstA HstB HstC Swt1 1 2 3 Only route on a spanning tree No packet on this linkas not on spanning tree. Verified for an arbitrary number of packets exchanged between HstA and HstB in 600s with 1.45M.
29.Overview Existing approaches and problem statement Abstraction on Stateful firewall Experimental case studies Stateful firewall Learning switch Conclusions
30.Conclusions We presented abstractions for: Verifying properties for an arbitrary number of packets. Handling large network state. Verified a stateful firewall and a learning switch using these abstractions.
31.Thank You!

Latest Release