e code is not known (e.g., proprietary NFs). For example, we use the black box modeling tool to model a stateful firewall pfSense and get results in Figure 3.9. If the firewall is config- ured with an "accept" rule between the trusted zone and untrusted zone, it allows an outgoing SYN to "punch a hole", and all following incoming/outgoing traffic of that flow is allowed; without outgoing SYN, all traffic is dropped. If the firewall is configured with a "deny" rule, all traffic is simply dropped. The outcome of our white box and black box approaches are interchangeable. Transforming a SMAT to a DFA takes two steps: first, extract the state space from the state fields in the match column and the action column; second, each row in the SMAT represents a state transition (or edge) in DFA, and the flow fields in match/action columns represent input and output of that edge. Reversely, to trans- form a DFA to a SMAT, each state transition consists of start/end states and input/output, which can be exactly mapped to the state fields and flow fields in SMAT. Black box NF Probe Detect Packet space Angluin's algorithm */drop */pass */drop SYN_A_B/pass s1: initial, s2: outgoing SYN sent sl: initial (b) DFA accept (c) DFA deny Figure 3.9 Black box NF modeling method. 3 Network Function Virtualization 3.5.3 Modeling Applications With an accurate NF model, several NFV applications can be designed and developed. We list the example applications: NF program genera- tion, stateful network verification, and network policy composition. Verifying correctness of a network's configurations ahead of its actual deployment can avoid runtime errors. There a several stateless or stateful network verification solutions [55, 67, 74, 75] aiming to verify network properties such as reachability and isolation. Our model provides the NF model to support these solutions. We use SFC-Checker [55] as an example. SFC-Checker models each NF as a DFA and composes NF DFAs in a network to check reachabil- ity. Thus, we transform the model into DFA as the f