BUZZ: Testing Context-Dependent Policies in Stateful Data Planes

of 11
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Related Documents
BUZZ: Testing Context-Dependent Policies in Stateful Data Planes Seyed K Fayaz, Yoshiaki Tobioka, Sagar Chaki, Vyas Sekar September 25, 2014 CMU-CyLab CyLab Carnegie Mellon University Pittsburgh,
BUZZ: Testing Context-Dependent Policies in Stateful Data Planes Seyed K Fayaz, Yoshiaki Tobioka, Sagar Chaki, Vyas Sekar September 25, 2014 CMU-CyLab CyLab Carnegie Mellon University Pittsburgh, PA 15213 BUZZ: Testing Context-Dependent Policies in Stateful Data Planes Seyed K. Fayaz, Yoshiaki Tobioka, Sagar Chaki +, Vyas Sekar CMU, + SEI Abstract Network operators spend significant effort in ensuring that the network meets their intended policies. While recent work on checking reachability and isolation policies have taken giant strides in this regard, they do not handle context-dependent policies that operators implement via stateful data plane elements. To address this challenge, we present the design and implementation of BUZZ, a testing framework to ensure that a network with stateful data plane elements meets complex context-dependent policies. In designing BUZZ, we address significant challenges in: (1) modeling stateful data plane elements, and (2) tackling the state-space explosion problem in generating test scenarios. We also implement practical heuristics to resolve interference from background traffic and to localize sources of policy violations. We demonstrate the scalability of BUZZ in localizing policy violations on networks with more than 100 nodes. 1 Introduction Many studies highlight the difficulty network administrators face in correctly implementing policies. For instance, one recent survey found that 35% of networks generate more than 100 problem tickets per month and nearly one-fourth of these problem tickets take multiple engineer-hours to resolve [14]. Anecdotal evidence suggests that operators go to great lengths to debug networks; e.g., creating shadow configurations of entire infrastructures for testing [25]. This challenge has inspired several projects, including work on statically checking networks [34, 35, 36], formal foundations of networks [17, 31, 41], creating correctby-construction controllers [19], verifying software data planes [26], automatic test packet generation [55], and debugging control plane software [24, 49]. However, these efforts largely focus on forwarding-centric properties (e.g., loops, black holes) and layer 2/3 data plane functions (i.e., simple switches, routers, ACLs). While checking reachability properties involving switch configurations is clearly useful, real networks are more complex on two dimensions: Stateful and higher-layer network functions: Networks rely on a variety of data plane middleboxes and switches [50]. We use the term DPFs to collectively refer to such data plane functions, including: (i) stateless L2/L3 elements; and (ii) stateful middleboxes (henceforth called stateful DPFs) that operate at a higher-layer beyond L2/L3 and whose actions depend on the history of traffic; e.g., a proxy operates over HTTP requests and may send cached responses. Context-dependent policies: Operators use stateful DPFs to implement advanced policies beyond simple forwarding and access control rules. A simple policy is service chaining, i.e., HTTP traffic going through a sequence of a firewall, IPS, and proxy before exiting the network. Complex policies involve context-dependent information; e.g., a host generating too many failed connections may be flagged as anomalous and rerouted for detailed analysis [10, 18]. Unfortunately, such stateful operations and their attendant context-dependent policies fall outside the scope of the aforementioned network verification and testing tools. Our goal is to address this key missing piece to take us closer to the CAD-for-networks vision [39]. In this paper, we present the design and implementation of BUZZ, 1 a framework for testing if a network with stateful DPFs meets specified context-dependent policies. At a high level, BUZZ is a model-based tester [52]. Specifically, given an intended behavioral specification of the network (i.e., all stateful and stateless DPFs and their interconnections) BUZZ generates test traces that exercise specific policies, and then injects them into the real network to see if the observed behavior matches the intended policy. We make key contributions in addressing two related challenges to make this vision practical: Data plane modeling ( 5): While, conceptually, a stateful DPF is a giant finite state machine operating on raw IP packets, it is intractable to enumerate all possible states for all possible input packet sequences. To make DPF models tractable, BUZZ uses two key ideas. First, instead of modeling a DPF s operations as a giant FSM, we model each DPF as a FSM ensemble that mirrors the conceptual separation across functions inside the actual DPF s implementation; e.g., a proxy keeps a separate TCP state machine for each client and server. Second, rather than viewing DPFs as operating on low-level packets, we model their inputoutput behaviors in terms of a new notion of BDUs (BUZZ Data Units), which are abstract data units that succinctly capture higher-layer semantics spanning multiple low-level IP packets and also explicitly model the impact of stateful/context-dependent DPF actions. For instance, a full HTTP response can be represented by a single BDU packet, instead of many low-level packets. Similarly, BDUs allows our DPF models to expose hidden behaviors [29]. 1 BUZZ explores space ; e.g., Buzz Aldrin and Buzz Lightyear. 1 Test traffic generation ( 6): For reasonably interactive testing, new test cases must be generated in seconds. Unfortunately, even if we address the above modeling challenge, we run into scalability issues while trying to exercise a policy-specific sequence of effects due to the well-known state-space explosion problem [21]. To this end, we use a combination of three key ideas. First, we replace exhaustive statespace search with a more efficient symbolic execution based approach. Second, we leverage our BDU abstraction to first generate a high-level plan in terms of BDUs and then translate it into raw test traces. Finally, we engineer domain-specific optimizations (e.g., restricting number of symbolic variables) that allow symbolic execution to scale to large networks. We implement models for various DPFs as FSM ensembles written in C. Our choice of C over a domainspecific language [19, 31, 41] immediately lends BUZZ to a body of tools optimized for symbolic execution of C such as KLEE [22]. We implement our domainspecific optimizations on top of KLEE. We developed a custom translation from BDU sequences generated by KLEE to raw request traces used to test the real network. We prototype the overall test orchestration capabilities atop OpenDaylight [8]. Finally, given that we are performing tests on the actual network, we engineer heuristics leveraging SDN-based monitoring capabilities to rule out side effects from background traffic. We also implement practical heuristics to help localize diagnostic efforts when policy violations are detected ( 7). Our evaluations on a real testbed, shows that BUZZ: can test hundreds of policy scenarios on networks with 100 nodes in tens of seconds; dramatically improves scalability, providing nearly three orders of magnitude reduction in time for test case generation; effectively localizes intentional data/control plane bugs within tens of seconds; and imposes less than 1% overhead in terms of additional traffic even with adversarially interfering traffic. 2 Motivating Scenarios In this section, we use small but realistic network scenarios to: (i) highlight stateful data plane functions and context-dependent Fault&Tolerance& policies used by administrators; (ii) motivate challenges in implementing these policies correctly; and (iii) present limitations of existing work (on L2/3 reachability) in addressing these challenges. Proxy & Department & S 1& Mon & S 2& Internet& Figure 1: Dynamic cache actions. Stateful firewalling: Today s firewalls go beyond the traditional match-then-drop paradigm. A common policy is reflexive firewalling; i.e., the firewall tracks outgoing connections from internal hosts and allows incoming packets for previously established connections. Unfortunately, even this basic stateful processing cannot be handled by existing memoryless static checkers. For instance, ATPG Reachability/Isola2on# [55] and HSA [35] can only check for single packet effects and cannot model connection establishment logic and reflexive rules. H 1# H 2# Department# NAT # S 1# Enterprise# NAT # S 2# S 3# Stateful# FW# Remote## server # Figure 2: Blocking policy is difficult due to NATs. Dynamic policy violations: In Figure 1, we want to monitor outgoing web traffic. The problem here is subtle, as the proxy may send cached responses bypassing the monitor, defeating our goal. Potential fixes to this problem include placing the monitor before the proxy or using FlowTags to explicitly steer cached responses [29]. The key challenge is in identifying such potential policy violations and ensuring that the solution (e.g., using FlowTags) is implemented correctly 2. Specifically, to identify this policy violation, we need to model the stateful behavior of the proxy across connections. Firewalling with Cascaded NATs: Figure 2 shows a scenario where hosts are doubly NAT-ed at the department and the enterprise border. Prior work shows cascaded NATs are notoriously error-prone [20, 42]. Suppose the remote web server s firewall needs to to block host H 1 but allow H 2. Even this seemingly easy access control policy is difficult to check with existing L2/L3 reachability tools Dynamic#policy# because the hosts are hidden behind NATs; e.g., HSA/ATPG models them as black-boxes. H 1# H 2# H 3# Light# IPS # S 1# S 2# Heavy# IPS # Internet# Figure 3: Dynamic triggers. Multi-stage triggers: Figure 3 shows two intrusion prevention systems (IPS) used in sequence. The intended policy is to use the light-weight IPS (L-IPS) in the common case and only subject suspicious hosts flagged by the L-IPS (e.g., when a host generates scans) to the 2 BUZZ was partly motivated by the failure of existing tools to validate that our FlowTags implementation fixes the problem. 2 more expensive H-IPS. Such multi-stage detection is useful; e.g., to minimize latency and/or reduce H-IPS load. Again, it is difficult to check that this multi-stage operation works correctly using existing static checkers and reachability verifiers [35,55], because they ignore hidden state inside the IPSes and triggered sequence of intended actions (i.e., the context). Test packet generation (e.g., [55]) Static verification (e.g., [34, 35, 36, 38]) Verifying data plane software (e.g., [26]) Stateful Contextual Active data planes policies testing No No Yes No No No Yes No No Table 1: Strawman solutions (rows) vs. requirements from the motivating scenarios (columns). Strawman solutions: The above scenarios imply three key requirements: (1) capturing stateful data plane behaviors (e.g., stateful firewalls); (2) capturing contextual policies (e.g., LIPS-HIPS); and (3) active testing to reveal subtle traffic-dependent bugs that may not be directly visible from just looking at the network configuration (e.g., dynamic cache actions or cascaded NATs). Table 1 summarizes if/how some existing solutions address the scenarios described earlier. Across all motivating scenarios, we find that existing tools for checking network policies are inadequate. At a high level, the problem is that many existing tools for network reachability testing explicitly acknowledge these challenges and treat them as being out-of-scope to make their work tractable. While there is some recent work on testing software data planes, the focus is on different types of errors (e.g., crash or CPU cycles/packet) rather than the network-wide policy violations we consider here. Our overarching goal is to bring the benefits that these aforementioned efforts have provided for reachability correctness to the types of stateful network processing and contextual policies introduced by the above scenarios. 3 Problem Formulation Our high-level goal is to help network administrators test that the data plane implements the intended policies. In this section, we begin by formally defining our intended data plane semantics, and what we mean by a policy. In addition to helping us precisely define our goals, the formalism sheds light on the key technical components and challenges underlying any solution for testing stateful data planes for the given context-dependent policies. 3.1 Preliminaries First, we define the semantics of a DPF and the network. DPF: Let P denote the set of packets. 3 Formally, a 3 Packets are located [35,46], so that the DPF can identify and use DPF is a 4-tuple (S,I,E,δ) where: (i) S is a finite set of states; (ii) I S is the initial state; (iii) E is the set of network edges; and (iv) δ : S P S P E Σ is the transition relation. Here, Σ is a set of effects that capture the response of a DPF to a packet. Each α Σ provides contextual information that the administrator cares about. Each α is annotated with the specific DPF generating the effect and its relevant states; e.g., in Figure 3 we can have α 1 = LIPS : H 1,Alarm,SendToHIPS when the LIPS raises an alarm and redirects traffic from H 1 to the H- IPS, and α 2 = LIPS : H 1,OK,SendToInternet when the LIPS decides that the traffic from H 1 was OK to send to the Internet. Using effects, administrators can define high level policy intents rather than worry about lowlevel DPF states. Note that this DPF definition is general and it encompasses stateful DPFs from the previous section and stateless L2-L3 devices. Network: Formally, a network data plane net is a pair (N,τ) where N = {DPF 1,...,DPF N } is a set of DPFs and τ is the topology map. Informally, if τ(e) = DPF i then packets sent out on edge e are received by DPF i. 4 We assume that the graph has well-defined sources (with no incoming edges), and one more sinks (with no outgoing edges). The data plane state of net is a tuple σ = (s 1,...,s N ), where s i is a state of DPF i. 3.2 Processing semantics To simplify the semantics of packet processing, we assume packets are processed in a lock-step (i.e., onepacket-per-dpf-at-time) fashion and do not model (a) batching or queuing effects inside the network (hence no re-ordering and packet loss); (b) parallel processing effects inside DPFs; and (c) the simultaneous processing of different packets across DPFs. Let σ = (s 1,...,s i,...,s N ) and σ = (s 1,...,s i,...,s N) be two states of net. First, we define a single-hop network state transition from (σ,i,π) to (σ,i,π ) labeled by effect α, denoted (σ,i,π) α (σ,i,π ) if δ i (s i,π) = (s i,π,e,α), with DPF i = τ(e). A single-hop network state transition represents processing of one packet by DPF i while the state of all DPFs other than DPF i remains unchanged. For example, when the L-IPS rejects a connection from a user, it increments a variable tracking the number of failed connections. Similarly, when the stateful firewall sees a new three-way handshake completed, it updates the state for this session to connected. Next, we define the end-to-end state transitions that a packet π in entering the network induces. Suppose π in traverses a path of length n through the sequence of DPFs DPF i1,...,dpf in and ends up in DPF in+1 (note the incoming network interface information in its processing logic. 4 We assume each edge is mapped to unique incoming/outgoing physical network ports on two different DPFs. 3 that the sequence of traversed DPFs may be different for different packets). Then the end-to-end transition is a 4-tuple (σ 1,π in, α 1,...,α n,σ n+1 ) such that there exists a sequence of packets π 1,...,π n+1 with π 1 = π in, and a sequence of network states σ 2,...,σ n 1 such that 1 k n: (σ k,i k,π k ) α k (σ k+1,i k+1,π k+1 ). That is, the injection of packet π in into DPF i1 when the network is in state σ 1 causes the sequence of effects α 1,...,α n and the network to move to state σ n+1, through the above intermediate states, while the packet ends up in DPF in+1. For instance, when the L-IPS is already in the toomanyconn-1 state for a particular user and the user sends another connection attempt, then the L-IPS will transition to the toomanyconn state and then the packet will be redirected to the H-IPS. Let E2ESem(net) denote the end-to-end network semantics or the set of feasible transitions on the network net for a single input packet. Trace semantics: Next, we define the semantics of processing of an input packet trace Π = π1 in,...,πin m. We use α to denote the vector of DPF effects associated with this trace; i.e., the set of effects across all DPFs in the network. The network semantics on a trace Π is a sequence of effect vectors: TraceSem Π = α 1,..., α m where 1 k m: πk in P α k Σ +. This is an acceptable sequence of events iff there exists a sequence σ 1,...,σ m+1 of states of net such that: 1 k m: (σ k,πk in, α k,σ k+1 ) E2ESem(net). 3.3 Problem Definition Given the notion of trace semantics defined above, we can now formally specify our goal in developing BUZZ. At a high-level, we want to test a policy. Formally, a policy is a pair (TraceSpec; TraceSem), where TraceSpec captures a class of traffic of interest, and TraceSem is the vector of effects of the form α 1... α m that we want to observe from a correct network when injected with traffic from that class. Concretely, consider two policies: 1. In Figure 1, we want: Cached web responses to Dept1 should go to the monitor. Then, TraceSpec captures web traffic to/from Dept1 and TraceSem = α 1,α 2, with α 1 = Proxy : Dept1,CachedObject and α 2 = Proxy : Dept1,SendToMon. 2. In Figure 3 we want: If host H 1 contacts more than 10 distinct destinations, then its traffic is sent to H IPS. Then, TraceSpec captures traffic from H 1, and TraceSem = α 1,α 2 where α 1 = L IPS :H 1,Morethan10Scan, and α 2 = L IPS : H 1,SendtoHIPS. Our goal is to check that such a policy is satisfied by the actual network. More specifically, if we have a concrete test trace Π that satisfies TraceSpec Π and should ideally induce the effects TraceSem Π, then the network should exhibit TraceSem Π when Π is injected into it. Admin S1 Intended Behavior Intended Behavior Intended Behavior S2 check L-IPSà H-IPS triggers correctly Test planner (Sec 6) S3 Trace injector Injectors Data plane model (Sec 5) S5 Valida7on Engine (Sec 7) S4 Monitor Regular traffic Figure 4: High-level overview of BUZZ. In practice, generating these concrete test traces is tedious as it requires understanding and dealing with the complex low-level behaviors of DPFs. The goal of BUZZ is to automate this test trace generation. That is, the administrator gives a high-level specification of TraceSpec (e.g., Web traffic from/to Dept1) and TraceSem, and BUZZ generates a concrete test trace, injects it into the network, and checks if it satisfies the policy. Next, we discuss how BUZZ achieves this goal. 4 BUZZ System Overview Figure 4 shows the main components of BUZZ. The input to BUZZ is the administrator s policies (S1). In practice, we envision that administrators will define these policies in a higher-layer language that can then be translated to more formal (TraceSpec; TraceSem) entries. As such, the design of this policy language is outside the scope of this paper. These input policies refer to physical DPFs (e.g., a NAT followed by a firewall), which can be obtained from policies in terms of corresponding logical DPFs [45]. We envision operators populating a set of such policies. 5 Given these, BUZZ processes these one policy a time as we describe next. As we saw in the previous section, the effects depend on the processing semantics of the individual DPFs and the data plane as a whole. Thus, BUZZ needs a model of the entire data plane (i.e., DPFs and the interconnections). Writing the DPF models is a one-time task for each type of DPF and we envision
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks