 chains. 5.2.4 Verification of Service Function Chaining The traditional approach to detecting configuration errors is to apply network verification. Unfortunately, current network verification techniques focus on verifying the flow table rules in Layer 2 and Layer 3 devices against basic invariants such as loop freeness and no blackholing [74, 110]. These approaches assume a simple stateless forwarding model where the action solely depends on a match on the header fields of each packet. However, many NFs are stateful; the handling of a packet depends not only on the current packet but also on previously encountered packets, in some cases, on the content of packets. For example, a firewall, discussed earlier, allows packets from external hosts only if it has previously seen an outgoing packet from internal host for that connection. One way to extend verification to NFs is using test packets to probe the NF and determine the set of invariants that are satisfied or vio- lated given the NF's current state. These active probing techniques can detect problems after they are deployed, but we still need static veri- fication to capture the problems before the deployment. In addition, these techniques require access to the source code but, due to propri- etary reasons, most NFs are closed source. An alternate approach is 5.2 Service Function Chaining not to rely on the source code. Further, to enable Telcos to continue to provide carrier-grade high availability and reliability, it will be crucial to verify the correctness of NFs and service chains before deployment and not after. Performing verification for NFs and their service chains introduces several interesting challenges. First, NFs maintain state about each flow and perform different actions based on the states. The states also vary largely depending on the type of NF being verified. Existing verification tools fail to support it because they are built on the OpenFlow type of forwarding abstraction, where all packets of a flow are handled the same using a match-ac