From Firewalls to Functions and Back

Abstract

Designing and maintaining rewall con gurations is hard also for expert system administrators. Indeed, policies are made of a large number of rules and are written in low-level con guration languages that are speci c to the rewall system in use. To simplify the work of system administrators, some authors of the present paper proposed in previous work a transcompilation pipeline and a tool that (i) extracts the meaning of a real con guration by representing it into a tabular form; (ii) refactors a con guration by removing redundant rules; (iii) ports the policy from a rewall system to another. Here, we extend this pipeline by proposing a new characterization that models rulesets and rewalls as functions from packets to transformations. Transformations specify which packets are accepted by the rewall and how they are translated. Using this functional characterization we propose two new algorithms that simplify the treatment of the pipeline.

-

Firewalls are the fundamental mechanisms for the protection of computer networks. The e ectiveness of a rewall system crucially depends on the correctness of its con guration, since even a small aw may severely impact the security or the functionality of the entire network.

Policies are typically written in low-level con guration languages that are speci c to the rewall system in use and support non-trivial control ow constructs, such as calls and gotos. A con guration usually consists of a large number of rules interacting with each other. Indeed, some rules may shadow others or prevent them to be triggered depending on the order in which they appear in the con guration. This context-dependency makes it hard to understand the effect of a single rule on the overall rewall behaviour. Moreover, when writing a policy, network administrators must also take into account how packets are processed by the network stack of the operating system running on the rewall. The scenario becomes even worse when Network Address Translation (NAT) is considered, since packets can be modi ed while they traverse the rewall by translating IP addresses and performing port redirection.

To simplify the work of system administrators, some of the authors proposed a transcompilation pipeline [ 4 ] and a tool [ 5 ] to (i) decompile real con gurations into abstract speci cations representing the set of the permitted connections; (ii) perform policy refactoring by removing redundant rules thus obtaining minimal and clean con gurations; (iii) automatically port a con guration written for a system into the language of another system. The proposed transcompiling pipeline is made of the following stages: 1. decompile a policy from the source language to an intermediate language; 2. extract the meaning of the policy as a table describing how the accepted packets are translated; 3. compile the semantic table into the target language.

Core of the stage 1 is the intermediate language IFCL equipped with a formal semantics and with all the typical features of rewall languages. IFCL enables the algorithmic manipulation of stage 2, where a SAT-based procedure is used to derive a minimal declarative con guration in a tabular form that shows all accepted packets and their NAT, without overlapping or shadowed rules.

In this paper, we extend the above pipeline by proposing new algorithms for stage 2 and 3. The rst one does not rely on a SAT solver, but on a denotational semantics that directly represents a con guration as a function from packets to packet transformations. These transformations specify whether packets are accepted or not and how they are rewritten by NAT. Furthermore, the new algorithm for stage 3 works with the new functional representation and preserves the translation applied by the original con guration. Di erently from [ 4 ], the algorithm does not rely on tagging packets, thus simplifying the treatment of rewall systems with limited support of this tagging feature, e.g., pf. Exploiting the properties of IFCL, we characterize the target systems on which the new algorithm is granted to work for all con gurations, like iptables. We remark that representing rulesets and rewalls as functions allows us to simplify the treatment of the stages because we resort to a more abstract and handy domain.

The rest of the paper is organized as follows. Section 2 presents our proposal via a small yet realistic example and also compares it to the previous approach of [ 4 ]. Our new algorithms are described in Sections 3 and 4. In Section 5 we present related works and in Section 6 we conclude and discuss some future work. 2

Overview of the Pipeline

We consider as an example the network in Figure 1, where the rewall is connected to the LAN 192:168:0:0=24 with IP 192:168:0:1, and to the Internet using the IP 151:15:185:183. Notice that hosts in the LAN have private addresses that cannot be routed on the Internet, hence NAT must be used to rewrite the source address of outgoing packets and the destination address of incoming packets. Notice also that such hosts cannot communicate directly with each other, messages have to pass through the rewall. We wish to con gure a rewall that satis es the following requirements. (R1) When a packet from the Internet with destination 192.168.0.0/24 : : : 192.168.0.8 port 22 reaches the external IP address of the rewall, it is redirected to the SSH server at 192:168:0:8. (R2) Every LAN host is allowed to access HTTP servers on the Internet. NAT is applied to rewrite the source address of outgoing packets with the public address of the rewall, so that responses from web servers can be routed back. (R3) Connections to the address 8:8:8:8 are not allowed. (R4) All local hosts can connect to the SSH server in the LAN. (R5) The administrator can connect to SSH on the rewall from host 192:168:0:8.

The ipfw rewall con guration in Fig. 3 implements the above requirements. Lines 1 and 2 respectively con gure the NAT module according to requirements (R1) and (R2), while rules in lines 6 and 7 apply NAT. Note that line 8 imposes an additional condition: the rewall communicates with hosts in the Internet only over port 80. Line 5 is for requirement (R3), and line 9 for requirement (R4), besides (R2). Line 10 implements requirement (R5), while line 11 blocks any other tra c. 1 ipfw -q nat 1 config redirect_port tcp 192.168.0.8:22 22 2 ipfw -q nat 2 config ip 151.15.185.183 3 4 ipfw -q add 0010 check - state 5 ipfw -q add 0020 deny tcp from any to 8.8.8.8 6 ipfw -q add 0030 nat 1 tcp from not 192.168.0.0/24 to 151.15.185.183 22 7 ipfw -q add 0040 nat 2 tcp from 192.168.0.0/24 to not 192.168.0.0/24 80 8 ipfw -q add 0050 allow tcp from 151.15.185.183 to not 192.168.0.0/24 80 9 ipfw -q add 0060 allow tcp from any to 192.168.0.8 22 10 ipfw -q add 0070 allow tcp from 192.168.0.8 to 192.168.0.1 22 11 ipfw -q add 0080 deny all from any to any

Before showing the result of the decompilation (stage 1 of our pipeline), we brie y introduce the intermediate language IFCL. A rewall con guration in IFCL consists of a set of rules, with a format common to most of the real rewalls, and a control diagram that describes how packets are processed by the rewall system under consideration. Speci cally, a control diagram is a graph C where every node is associated to a ruleset that is applied to packets reaching that node. Arcs are labeled with predicates that encode the routing decisions performed by the rewall. Intuitively, a packet p is accepted by the rewall if there exists a path from the initial to the nal node of C such that p is accepted (and possibly transformed) by the rulesets associated to the nodes of the path.

A rewall rule consists of a predicate over packets and an action t, called target, de ning how packets matching are processed. We consider the targets: ACCEPT DROP NAT(nd; ns) MARK(m) the packet is accepted the packet is discarded apply NAT marking with tag m In the NAT action, nd and ns specify how to translate the destination and source addresses/ports of a packet and we use ? to denote the identity translation. For instance, nd = n : ? means that the destination address of a packet is translated according to n, while the port is kept unchanged. The MARK action marks a packet with a tag m. Predicates of the rules in a ruleset may select packets based on tags assigned by preceding rules of the rewall. Notice that, since the tag is not part of the network packet, it is lost when the packet leaves the rewall. Here we consider a subset of targets used in [ 4 ] and we restrict the NAT target to addresses only not ranges as in [ 4 ]. We do not lose generality because the initial part of stage 2 normalises the con guration by removing the targets concerning the ow control and because performing NAT towards a range of addresses is rarely used in practice. Additionally, we assume all connections to be new as done in [ 5 ].

Fig. 2a shows Cipfw, the control diagram of ipfw. Guards label the arcs to check whether the source/destination address of packets (in symbols sIP/dIP ) belong to S (the addresses assigned to the rewall). Stage 1 produces the rewall consisting of Cipfw and the assignment to both nodes q0 and q1 of the ruleset (dIP = 8:8:8:8; DROP); dPort sIP 22 22 80

Accepted packets sPort dIP - - - The second stage of our pipeline de nes a function that speci es whether a packet is accepted or not and eventually how it is transformed. In other words, this function is the denotational semantics of the con guration in hand. Table 1a displays the functional meaning of the example in Fig. 3. To obtain it we rst compute the functions associated to the ruleset of each node and then we compose them along the paths of the control diagram. In this speci c example the composition is trivial since the rulesets associated with q0 and q1 are the same.

The last stage of our pipeline compiles the semantics into the target language, here iptables. This stage consists of three steps. In the rst, we consider the control diagram Ciptables in Fig. 2b, where, by construction, the operations over packets are only allowed on speci c nodes, as suggested by the labels in the gure. For transcompiling, we are thus left to associate with the nodes of Ciptables a suitable function, computed from the semantics in Table 1a. Essentially, we project it along the paths of Ciptables, taking care of the actions that iptables prescribes in the traversed nodes.

For example, take node q9: only packets with a source IP address in S can traverse it. Moreover, packets subjected to DNAT will reach q9 with the translated destination address, since DNAT is applied in node q8. Di erently, SNAT will occur later on the path (in node q5 or q11). We build the Table 1b associated with node q9 by transforming each row of Table 1a by applying the speci ed DNATand then keeping only packets with source address in S. The second step discards the rst row of Table 1a since 192:168:0:8 2= S. Instead, ltering out the non-local addresses in the second row yields the rst row of Table 1b. The third row is left unchanged. We select the only local address from the fourth row and we defer the SNAT to the rulesets associated to nodes q5 and q11. Applying the speci ed DNAT to the fth row turns 151:15:185:183 into 192:168:0:8, which is already represented by the rst row of Table 1b.

The third step is straightforward: each row of the tabular representation of the obtained function originates an IFCL rule. In this example, the result for nodes q5 and q11 is (sIP 2 192:168:0:0=24 ^ dIP 2= 192:168:0:0=24 ^ dPort = 80; NAT(? : ?; 151:15:185:183 : ?)) while for q1 and q8 we have (sIP 2= 192:168:0:0=24 ^ dIP = 151:15:185:183 ^ dPort = 22; NAT(192:168:0:8 : ?; ? : ?)) and for nodes q3, q6 and q9 respectively (dIP = 192:168:0:8 ^ dPort = 22; ACCEPT); (sIP 2 192:168:0:0=24 ^ :(dIP 2 192:168:0:0=24 _ dIP 2 8:8:8:8) ^ dPort = 80; ACCEPT); All remaining nodes have an empty ruleset. Eventually, these rules are compiled into the iptables con guration shown in Fig. 4. Note that some target languages may constrain the guard of rules to have a speci c form, more restrictive than the one used by IFCL. Hence, before generating the target con guration, we transform every IFCL rule into an equivalent form, possibly implemented with multiple rules. For example, in an iptables rule you cannot impose an IP address to be anything but 8:8:8:8 or 192:168:0:0=245. You can achieve the same goal by considering the ranges obtained by taking the complement of the union of those sets, as in lines 22-27 of Fig. 4.

The synthesis is similar to the one proposed in [ 4 ], where logical predicates P(p; p~) were assigned to the rulesets. These predicates are true if and only if the packet p is accepted as p~ by the corresponding ruleset. The predicate corresponding to a rewall was, thus, obtained by the composition of predicates 5 You can write something like ! -d 8.8.8.8, 192.168.0.0/24, but it will be interpreted as dIP 2= 192:168:0:0=24 _ dIP 6= 8:8:8:8 i.e. in a really useless requirement. for rulesets in the paths of the control diagram. The table was then produced by computing the model of the rewall predicate using a variant of the bisection method in which every check resulted in a call to the SAT solver. Since we have chosen an handy representation here, the resulting table can be computed directly, hence gaining exibility and avoiding the bottleneck of multiple invocation to the solver. On the contrary, the last stage of the pipeline is very di erent from the one presented in [ 4 ]. Indeed, there one speci c ruleset was produced for each speci c task: ltering the network, performing SNAT and DNAT. The actions to be performed on each packet were known thanks to the tags previously associated by the rewall. Furthermore, the assignment of rulesets to the nodes of the target control diagram was de ned in an ad hoc way for the supported languages (iptables and pf). That approach is not immediately extensible to other systems, especially those with minimal control diagram like ipfw, where some nodes may accomplish all the tasks. Finally, the last translation into the target language was not treated in [ 4 ]. We believe that the new translation algorithm simpli es this last step because we do not need to deal with tagging whose support is very heterogeneous on the various systems. 3

From a Con guration to a Function: Synthesis

We present the algorithm for the second stage of our pipeline. Given an IFCL con guration we compute a synthetic representation of its behaviour as a function on the ongoing tra c: we rst formally de ne the domains on which the resulting function operates, and we then introduce a convenient representation from which we derive the algorithm.

Domains Let P be the set of all network packets. We de ne a semantic function of type P ! T(P) [ f?g that given a packet p 2 P either discards it (returning ?) or accepts it, possibly with some changes due to NAT (returning a transformation t 2 T(P), de ned eld by eld). Below we denote by t(p) the packet obtained by applying the transformation t to the packet p. Furthermore, given two transformations t and t0, we denote by tnt0 (t updates t0) the transformation resulting by rst applying t0 and then t, formally (t n t0)(p) = t(t0(p)) | as we will see later on, n is not standard function composition since it deals only with the outputs, which are accumulated.

The succinct representation we use is based on multi-cubes, which are a generalization of geometric cubes [ 7 ]. In a n-dimensional space, a cube is the cartesian product of n segments, whereas a multi-cube is the product of n unions of segments. Since rewall rules put requirements on packets eld by eld, the set of packets matching them is naturally expressible as a multi-cube. For example, the set of packets satisfying the predicate sIP = 192:168:0:8 ^ sPort = 22 ^ (dIP 2 192:168:0:0=24 _ dIP = 127:0:0:1) ^ dPort 2 f22; 80g can be expressed using the following multi-cube: f22g

(192:168:0:0=24 [ f127:0:0:1g) (f22g [ f80g) Algorithm 1 1: function ruleset synthesis(P : set of packets, R: ruleset, t: transformation) 2: if R = [ ] then return f(P; t)g 3: ( ; target) R0 R 4: (Ps; Pn) split(P , t, ) 5: 0 SP n02Pn ( ruleset synthesis(Pn0 , R0, t) ) 6: if target = ACCEPT then return f(Ps; t)g [ 0 7: else if target = DROP then return f(Ps; ?)g [ 0 8: else if target = NAT(dn; sn) then return f(Ps; trnat(dn; sn) n t)g [ 0 9: else if target = MARK(m) then return ruleset synthesis(Ps, R0, ttag(m) nt) [ 0 We represent a semantic function as a set A of pairs (P; t), where P P is a multi-cube and t is either the transformation associated with every packet in P or it is ?. Note that the projection of A on its rst component is a partition of P. The tables of the above example have rows corresponding to a pair (P; t): the rst four columns are the input (the multi-cube) and the last four are the output (the transformation). For brevity, the rows with output ? are omitted. Algorithms The stage 2 rst computes a semantic function for every ruleset of the control diagram through RULESET SYNTHESIS in Algorithm 1; then, it composes the results in a single table using COMPOSE in Algorithm 2.

Consider rst the recursive algorithm RULESET SYNTHESIS. Its parameters are respectively: a multi-cube P (initially P) representing the set of packets we are interested in; the ruleset R we are analyzing, scanned rule by rule; and the transformation t (initially the identity) already computed for P . Taken a rule (line 3) the set P is split in the two sets Ps and Pn (line 4). The rst is the multi-cube of the packets that verify the rule when transformed by t, thus, the algorithm returns it unchanged. The (complementary) set Pn is instead a disjoint union of non-empty multi-cubes, on which the function is recursively called on (line 5). Lines 6 and 7 are trivial. In line 8 the transformation dictated by the NAT (represented by trnat) updates the accumulated one. Note that, as stated before, n is not the standard function composition. Besides updating the transformation, line 9 calls recursively the function, because MARK does not terminate packet processing. The base case of recursion, when R is empty (line 2), yields the set of packets as it is and the computed transformation over them.

Now we exploit COMPOSE in Algorithm 2 to combine the results returned by the previous algorithm. The underlining idea is to visit the control diagram backward from the nal node to the initial one, thus composing the semantic function of a node q with the result of COMPOSE applied to each successor q0. Consequently, the table assigned to q0 is the combination of the functions of all the following nodes from q0 to qf . More precisely, line 3 computes the packets that are dropped by node q, i.e., the pairs (P; ?). Then, for each successor q0, reachable through an arc labeled with , line 6 propagates the remaining packets Algorithm 2 q0 (q;q0) q 8: return q 1: function compose(q: node) 2: R function assigned to node q 3: q f(P; t) 2 R j t = ?g 4: for node q0 reachable from q with guard on the arc do 5: function assigned to node q0 6: f(P 0; t) j (P; t) 2 R ^ P 0 = (t(P ))g 7: q [ f(P 00; t0 n t) j (P; t) 2 (q;q0) ^ (P 0; t0) 2 q0 ^ P 00 = t 1(P 0 \ t(P ))g that verify after the application of t6. Finally, line 7 composes each propagated pair (P; t), with each pair (P 0; t0) of q0, if there is a nonempty subset P 00 of P included in P 0 after the application of t7. The result of the composition is the pair (P 00; t00), where t00 is the transformation t updated with t0.

The resulting table associated with qi of the control diagram is the synthesis representing the semantic function of the rewall con guration. 4

From a Function to a Con guration: Generation

Here we describe the last stage of our pipeline which compiles the output of the previous stage into the target language. In particular, we focus on an algorithm that computes the functions for the rulesets and assigns them to the nodes of the target control diagram. Note that when a rewall system is not capable of expressing the input semantic function, the algorithm detects it. Moreover, it is granted to compile (if possible) whenever the paths in the target control diagram do not have duplicated NAT labels (e.g., DNAT repeated more than once).

Intuitively, our algorithm projects the table of the system to be compiled onto the paths of the control diagram of the target system. Since the modeled systems constrain the nodes of the control diagram to perform only certain actions, the projection must take into account the permitted actions of the traversed nodes. We represent these constraints by labeling each node with a subset of fSNAT; DNAT; DROPg, as we did in Fig. 2b. Only assignments that meet the constraints are granted to be expressible in the target language.

The tables assigned to nodes are generated incrementally, starting with an empty set and then gradually adding pairs (P; t) implementing the expected behaviour. First, we deal with rows specifying accepted packets, by assigning them to the corresponding path in the target control diagram. For example, the rst line of Table 1a is assigned to the path = qi; q0; q1; q4; q5; q6; qf in Ciptables. Given such a path, we project a pair (P; t) along its nodes, by rst computing the transformations and then the corresponding multi-cubes. As regards the transformation t, we decompose it and we generate a new transformation for each 6 In the Algorithm 2 we abuse the notation, denoting fp 2 P j (p)g with (P ). 7 Note that t is not an invertible function, hence with t 1(P 0 \ t(P )) we denote the preimage of P 0 \ t(P ) w.r.t. t, inside the domain P . node following the labels. For example, a row with target NAT(dn; sn) associated with the path in Ciptables, results in NAT(dn; ? : ?) in q1, NAT(? : ?; sn) in q5 and in id in all the other nodes of . As for the multi-cube P , we assign to each node the result of the application of the predecessor transformation to its corresponding multi-cube. The rst node of the path is assigned to P . In the example above we assign the pair (P; id) to qi and q0, (P; t0) to q1, where t0 is the transformation implementing NAT(dn; ? : ?), and (t0(P ); id) to q4. After repeating this procedure for all the rows of the table, the accepted packets are managed correctly, however the sets of pairs assigned to each node q can be incomplete: some packets may be included in no multi-cubes of q. We call them free packets of q. In other words, we still need to de ne the behaviour of the node for some cases. Next we need to complete the just assigned sets in order to manage the packets discarded by the input semantic function. Given that we do not modify the pairs already added, it is not possible to compromise the previous result. Moreover, since we are left to deal with dropped packets only, every packet that is not already included in a multi-cube should be dropped.

We start from the nodes in the control diagram labeled with DROP, where the choice is trivial: we assign ? to every free packet. Then, we use a recursive procedure to con gure all other nodes to transform their free packets in such a way that they reach some node q? labeled with DROP as free packets of q?. Let P? be the set of multi-cubes containing the packets dropped by the function associated to q (either directly or by passing them to another node that discards them), and assume that q0 is a predecessor of node q reachable through an arch labeled with . The idea is to assign to the free packets of q0 a transformation that maps them inside (P?). We lter P? using because we want to send the packets along the arc pointing to q. For each multi-cube of free packets of q0 we check if it is possible to map some of them inside (P?), updating the table accordingly. In each node, the transformations that we can exploit depend on the labels. If a node is labeled with both SNAT and DNAT, then we can map all the free packets to a single value inside (P?). If we have no labels assigned, we can only apply id, and then, for each multi-cube of free packets, the subset of the dropped ones is computed as the intersection with (P?). The case where only DNAT (resp. SNAT) is assigned to a node is a composition of the previous ones, where for the source addresses (resp. destination addresses) we take the intersection with each multi-cube in (P?), and we map the other addresses to some value inside the same multi-cube. After updating the table of q0 the back-propagation continues recursively. 5

Related Work

In this work we extend the pipeline de ned in [ 4 ], of which the implementation of the rst two phases is described in [ 5 ]. To the best of our knowledge, [ 4 ] and this work are the only approaches in literature to mechanically port rewall policies, while there are other tools for some rewall administration tasks. There are proposals that deal with speci c problems without deriving an abstract representation of the rewall policies, like [ 6 ] for refactoring, FIREMAN [ 11 ] and Margrave policy analyzer [ 10 ] for error correction. Other approaches, like ours, are based on abstract policies: they can be divided into those that start from a real con guration and derive an abstract one to perform analyses, like Fang [ 8,9 ], that can discover anomalies; and those that starting from an abstract policy generate a real con guration, like [ 1,3 ]. All these approaches propose their own high level language with a formal semantics, and de ne a compilation from the real con guration language to the abstract one (cf. our stage 1 and 2) or vice-versa (cf. our stage 3). Instead our approach de nes the compilation in both directions, dealing with real source and target languages. It thus takes from real languages actions both for ltering/rewriting packets (notably NAT and MARK) and for controlling the inspection ow, widely used in practice. NetKat [ 2 ] embraces a di erent approach, proposing linguistic constructs for programming a network as a whole within the SDN paradigm. This approach is orthogonal to ours: we consider real rewall con guration languages as low-level machine languages, and provide the needed tools for supporting legacy systems.

Our approach and that of [ 4,5 ] di er from the other proposals mainly because at the same time it (i) is language-independent; (ii) de nes a formal semantics of rewall behavior; (iii) gives a concise and neat representation of such a behavior; (iv) supports NAT, MARK and targets for changing the control ow; (v) both input and output are real con guration languages. 6

Conclusion

We presented two new algorithms for stages 2 and 3 of the transcompilation pipeline of [ 4 ]. The new algorithm for stage 2 directly represents a con guration as a function (in a tabular form) from packets to transformations, specifying which packets are accepted and how they are re-written by NAT. The second algorithm starts from the functional representation returned by stage 2 and compiles it into another system, preserving all the NAT of the original con guration and not relying on any tag mechanism. Finally, we characterized the properties of the target systems for which the algorithm is granted to work for all input con gurations. In particular, there are cases like ipfw where the algorithm is not granted to work, in the sense that it can fail even when a solution would be possible. This is due to the fact that the control diagram does not impose enough constraints on which nodes can apply SNAT and DNAT. A limit of the proposed approach is that multi-cubes can be split but not merged by the algorithms, causing the synthesis to produce tables with many rows, and, consequently, the compilation to produce long con gurations.

As future work we plan to implement the new algorithms inside the tool proposed in [ 5 ] and to carry out an experimental evaluation to test whether the new functional representation improves the performance of the tool when dealing with real-world con gurations. We also plan to implement and evaluate a procedure for multi-cube merging. Furthermore, we aim at improving the readability of the generated policies by automatically grouping rules and by adding comments that explain their meaning. Finally, it would be very interesting to extend our approach to deal with networks with more than one rewall.

References

1. Ada~o, P. , Bozzato , C. , Dei Rossi , G. , Focardi , R. , Luccio , F.L. : Mignis: A Semantic Based Tool for Firewall Con guration . In: proc. of the 27th IEEE CSF . pp. 351 { 365 ( 2014 )

2. Anderson , C.J. , Foster , N. , Guha , A. , Jeannin , J. , Kozen , D. , Schlesinger , C. , Walker , D. : Netkat: semantic foundations for networks . In: proc. of 41st ACM POPL . pp. 113 { 126 ( 2014 )

3. Bartal , Y. , Mayer , A.J. , Nissim , K. , Wool , A. : Firmato: A novel Firewall Management Toolkit . ACM Transactions on Computer Systems 22 ( 4 ), 381 { 420 ( 2004 )

4. Bodei , C. , Degano , P. , Focardi , R. , Galletta , L. , Tempesta , M. : Transcompiling rewalls . In: Proc. POST 2018 . LNCS ( 2018 )

5. Bodei , C. , Degano , P. , Focardi , R. , Galletta , L. , Tempesta , M. , Veronese , L. : Language-independent synthesis of rewall policies . In: Proc. 3rd IEEE European Symposium on Security and Privacy ( 2018 )

6. Diekmann , C. , Michaelis , J. , Haslbeck , M.P.L. , Carle , G.: Veri ed iptables Firewall Analysis . In: the 15th IFIP Networking Conference . pp. 252 { 260 ( 2016 )

7. Jayaraman , K. , Bj rner , N., Outhred , G. , Kaufman, C.: Automated Analysis and Debugging of Network Connectivity Policies. Tech. rep. , Microsoft ( 2014 )

8. Mayer , A.J. , Wool , A. , Ziskind , E.: Fang : A Firewall Analysis Engine . In: proc. of the 21st IEEE S&P 2000 . pp. 177 { 187 ( 2000 )

9. Mayer , A.J. , Wool , A. , Ziskind , E.: O ine rewall analysis . Int. J. Inf. Sec . 5 ( 3 ), 125 { 144 ( 2006 )

10. Nelson , T. , Barratt , C. , Dougherty , D.J. , Fisler , K. , Krishnamurthi , S.: The Margrave Tool for Firewall Analysis . In: Proc. of LISA 2010 ( 2010 )

11. Yuan , L. , Mai , J. , Su , Z. , Chen , H. , Chuah , C. , Mohapatra , P. : FIREMAN: A Toolkit for FIREwall Modeling and ANalysis . In: 27th IEEE S&P . pp. 199 { 213 ( 2006 )