ng packet matches a flow pattern f1, the internal state is in S1 and a predicate P(f, S1) is satisfied, then the packet is sent out with possible transformation Fwd(f1, S1) and the internal state is transited to Upd(f,,11). In our running example code, each frontend incoming packet would be checked to determine whether the flow was seen before (in the address/port translation mapping), which is the predicate of flow and states in the match field; the first packet of each new flow triggers address and port translation (stored in a dictionary), which is a state transition; and sendp() is an action on packets. 3.5.1.4 Model Extraction Overview In the following, we sketch a white box modeling approach based on our existing work. In this approach, we assume that the source code of the NF program is known and propose a modeling framework called Lancet. An NF program is assumed to have a processing loop and packet input/output functions, and an NF model is predefined like a stateful match action table. This work is published as NFactor [57]. The process is shown in Figure 3.8. It takes three steps as follows: 1) It first conducts backward slicing from packet output function to get packet slice and from state variable assignment statements to get state slice. 2) It then symbolically executes the union of both slices and get mul- tiple execution paths. For scalability, we need to constrain the value of some variables. 3.5 NF Modeling Program Packet slice Program Exec. Path 1 Exec. Path 2 State slice Step 1: Slice program Step 2: Execution paths Verification Sym. Exec. Match Action State State mode = HASH Match Action f[output]:=hash(f) State State REQ=(dst->SRV), RES=(src->SRV), cache={) Path 1 Cache TEREQ (Ecache f[output]:=SRV fEREQ fecache f:=cache[f], f[output]:=CLT Exec. Path 2 fERES f[output]:=CLT cache[f]:=f Step 3: Fill in model Models of LB(hash) and cache Figure 3.8 Source-code-based NF modeling method. (a) Step 1: slice program; (b) Step 2: execution paths; (c) Step 3: fill in model; (d) Step 4: Models of LB(ha