2016 IEEE 29th Computer Security Foundations Symposium

Localizing Firewall Security Policies

Pedro Adão∗ , Riccardo Focardi† , Joshua D. Guttman‡ , and Flaminia L. Luccio§
∗ Instituto de Telecomunicações and Instituto Superior Técnico, Universidade de Lisboa
† University Ca’ Foscari, Venice and Cryptosense, Paris
‡ The MITRE Corporation and Worcester Polytechnic Institute
§ University Ca’ Foscari, Venice

Abstract—In complex networks, filters may be applied at instance only packet addressed to port 80 or 443 on a web
different nodes to control how packets flow. In this paper, we server.
study how to locate filtering functionality within a network.
We show how to enforce a set of security goals while allowing In this paper, we introduce an expressive way to state
maximal service subject to the security constraints. To implement security goals for packet flows. A security goal involves three
our results we present a tool that given a network specification network locations B, R, E, two assumption properties ψB , ψE ,
and a set of control rules automatically localizes the filters and and one requirement property φ. Each of the properties char-
generates configurations for all the firewalls in the network. These acterizes packets—generally, their header fields—as found at
configurations are implemented using an extension of Mignis
— an open source tool to generate firewalls from declarative, a relevant location. The state of a packet may change as it
semantically explicit configurations. traverses the network, so the properties apply to the packet as it
Our contributions include a way to specify security goals for appears when present at the corresponding locations. Network
how packets traverse the network; an algorithm to distribute address translation (NAT) is the packet-changing operation that
filtering functionality to different nodes in the network to enforce we consider in this paper. However, the IP security protocols
a given set of security goals; and a proof that the results are
compatible with a Mignis-based semantics for network behavior. raise similar issues. The semantics of a goal concerns the
packet flows that begin at B; end at E; and traverse R. The
goal requires that any packet that follows such a path must
I. I NTRODUCTION satisfy predicate φ when it is present at location R, assuming
Organizations have big and complicated networks. A uni- that it satisfied ψB at the beginning and ψE at the end.
versity may have a network partitioned into dozens of subnets, We provide an algorithm to determine what filtering to do
separated either physically or as VLANs. Although many at the different routers in the network to enforce a given set
of those subnets are very similar, for instance in requiring of security goals. Our algorithm allows maximal functionality,
similar protection, others are quite different, for instance delivering as rich a set of packets as are compatible with the
those that contain the university’s human resources servers. policy, in the relevant case of packets that are not spoofed at
The latter require far tighter protection. As another example, their origin and not delivered promiscuously at the end. We
consider a corporation: some subnets contain public-facing also provide a rigorous semantics of network behavior that
machines such as web servers or email servers; others support allows us to prove that our algorithm is sound. Finally, to
an engineering department or a sales department; and yet implement our results we present a tool that, given a network
others contain the process-control systems that keep a factory specification and a set of control rules, uses this algorithm to
operating. Thus, they should be governed by entirely different automatically localize the filters and to generate configurations
policies constraining what network flows can reach them, and for all the firewalls in the network. These configurations are
from where. generated using Mignis+ , an extension of Mignis — an open-
Indeed, a network is a graph, in which the packets flow source tool to generate firewalls from declarative, semantically
over the edges, and the nodes may represent routers, end explicit configurations.
systems, and so forth. The security goals we would like to
enforce reflect this graph structure. They are essentially about Related work: Our approach is motivated by some previous
trajectories, i.e. about where packets travel to get where they work. We are interested in the defining behavioral security
are going. For instance, a packet that reaches the process specifications in a network. In [6] Guttman and Herzog studied
control system in the factory should not have originated in the trajectory-based security goals, developing techniques to deter-
public internet. After all, some adversary may use it to insert mine whether existing configurations enforce them correctly.
a destructive command, regardless of how benign its source Their goals were a less expressive class of two-region security
address header field looks when it arrives. Similarly, a packet goals, and they were unable to generate configurations in
that originates in the human resources department should not addition to analyzing given ones. However, this paper follows
traverse the public internet en route to the sales department. the lead of [6] in regarding security goals as properties of the
It could be inspected while there, compromising information trajectories of packets as they traverse the network, formalized
about salaries within the company. A security goal may also as a graph. Our network graphs and their executions are
restrict which packets may take a particular trajectory, for formalized in the frame model of Guttman and Rowe [7].

© 2016, Pedro Adao. Under license to IEEE. 194

DOI 10.1109/CSF.2016.21
 Zhang et al. [11] focus more on the possible conflicts Domains: LO, CH, D, E
among policies at different organizational levels, and less on sender : CH → LO rcpt : CH → LO
traces : LO → P(E ∗ )
their consequences given the topology of the network. Our chan : E → CH msg : E → D
method is more general and is also designed to apply in the TABLE I
case of devices that transform packets as they pass; we have S IGNATURE OF FRAMES
particularly focused on NAT.
Kurshid et al. [8] demonstrate that it is possible, within
software defined networking, to check dynamically if global, msg(e) is the data transmitted and chan(e) is the channel on
behavioral properties are maintained as invariants, for instance which it occurs. Events with the same channel and event are
reachability for certain sorts of packets. We instead make no indistinguishable, apart from the time at which they occur.
claims of real-time, on-line feasibility, but we offer a way to
Definition 1 (Frame [7]). Let LO, CH, D, E be domains
solve a broader range of security problems at design time.
that we will call locations, channels, data, and events, resp.
Interesting work has also been done from a network pro-
Assume that LO, CH are finite.
gramming language point of view. The Frenetic project [5]
deals with dynamic policies, but does not address network 1. A trace set T for a set of channels C ⊆ CH is a set of
reachability or cyclicity problems; it is not clear how newly sequences of events e0 , e1 , . . . , ek  such that:
added constructs can interact with old ones. NetKAT [3] (a) If ei is an event in t ∈ T , then chan(ei ) ∈ C; and
is equipped with a sound and complete equational theory. (b) T is prefix-closed.
However, while it might be possible to implement our security 2. A frame is a structure containing the domains and func-
goals, localization algorithm, and Mignis+ processing within tions shown in Table I such that, for all  ∈ LO, if
the NetKAT framework, doing so would still require the traces() = T , then T is a trace set for the set of channels
analysis we present here. C connected to , namely C =
Finally, much work has been devoted to firewall analysis,
{c ∈ CH : sender(c) =  or rcpt(c) = }.
e.g. Margrave [9], which again lacks the distributed behavior
of the network. Some automatic tools for testing of the firewall A trace of  means a sequence t ∈ traces(). ///
configuration enforcement have been proposed (see, e.g., [2],
[10]). These tools are very powerful in static networks, but Each F determines a directed graph.
they do neither prevent consistency problems when new rules Definition 2 (Frame graphs [7]). If F is a frame, then the
are added in the wrong order, nor avoid completeness problems graph of F, written gr(F), is the directed graph (V, E) whose
for some undefined packet rules. vertices V are the locations LO, and such that there is an
edge (1 , 2 ) ∈ E iff, for some c ∈ CH, sender(c) = 1 and
Structure of the paper: In Section II we present a model
rcpt(c) = 2 . ///
of our network as frames and executions, together with the
different types of nodes (i.e., routers, network regions, and end The execution model for frames relies on partially ordered
hosts), and trajectories. In Section III we define the security sets of events. The ordering represents the occurs before
goals and the functionality goals. In Section IV we describe relation, and events at a certain location  are required to be
how to assign filtering functionality to routers so as to enforce totally ordered and included in traces(). Formally:
a set of region control statements. We first consider the case
without NAT. In Section V we first present Mignis+ , an exten- Definition 3 (Executions [7]). Let F be a frame, and B =
sion of Mignis, and we then present a tool that given a network (B, ) be a finite, partially ordered set of events, i.e. B ⊆ E
specification and a set of region control rules automatically and  is a partial order on B. Define proj(B, ) =
localizes the filters and generates Mignis+ configurations for {e ∈ B : sender(chan(e)) =  or rcpt(chan(e)) = }.
all the firewalls in the network, again assuming the NAT-
free case. We also describe a case study with automatically B is an execution of F, written B ∈ Exc(F), iff
generated configurations. In Section VI, we extend localization 1. proj(B, ) is linearly ordered by , and
to cover NATs. We conclude in Section VII. 2. proj(B, ) ∈ traces(). ///

II. N ETWORK MODEL A finite linearly ordered set is a sequence. Thus, Clause 1
and the finiteness condition ensure that proj(B, ) is a se-
We model networks by frames and executions [7]. A loca- quence. Clause 2 adds the requirement that this sequence is a
tion  ∈ LO represents a network node and is equipped with trace of , for each choice of .
a set of traces traces() defining its possible local behaviors. We often write (c, p) for any event e such that chan(e) = c
We will use the words location and node interchangeably. A and msg(e) = p. Since different events may occur at different
channel c ∈ CH allows the synchronous one-way transmission times, but involve the same data value p on the same channel
of messages between the locations at its endpoints, sender(c) c, this is strictly speaking an abuse of notation.
and rcpt(c). Each message also carries some data v ∈ D. An In this paper, the data values D are packets. We will refer
event e is an occurrence of a message on a channel, so that to the source and destination addresses in a packet p as sa(p)

195
and da(p). Packets have other familiar properties such as a (c , p ) is buffered in σ. Rule routeout takes a pair (c, p)
payload, a protocol and—if the protocol is tcp or udp—a from the buffer and delivers packet p over channel c.
source port and a destination port. We let t ∈ traces(r) iff ∅, ∅; . . . ;t, σ.
In networking, physical connections are nearly always bidi-
Definition 4. We say that a frame F tightens a frame F 
rectional. A bidirectional connection will be represented by
iff they share the same graph, and for all routers r, and all
a pair of unidirectional channels. When convenient, we will
t, c1 , c2 , p, FW r (t, c1 , c2 , p) ⊆ FW r (t, c1 , c2 , p).
refer to this pair as if it were a single bidirectional edge.
A. Node behaviour B. Trajectories
Nodes in a network can be of three types: (i) routers, (ii) A trajectory is a path that a packet may take as it traverses
network regions, and (iii) end hosts. Routers are connected the network. Since the packet itself may change as it passes
to network regions (one or more), whereas end hosts are through a router with Network Address Translation, we need
connected to a single network region, or possibly more than to define which events may belong together, i.e. when the
one network region when the device has multiple interfaces. packet in a second event is the result of a NAT operation on
End hosts are either promiscuous or chaste. A promiscuous the packet in the first event.
host will accept any packet sent to it, and may transmit any Definition 5. Two events e, e are associated if
packet. A chaste host h has a set of IP addresses IP (h), rcpt(chan(e)) = sender(chan(e )) =  and either
accepting only packets with destination address i ∈ IP (h),
and transmitting only packets with source address i ∈ IP (h). 1.  is a network region and msg(e) = msg(e ); or
Given a network, one can easily construct a frame: the 2.  is a router that allows a trace (c0 , p0 ), . . . , (ck , pk ) and
locations of the frame are the network nodes; for each (undi- ∃i, j : i < j such that (ci , pi ) = e ∧ (cj , pj ) = e ,
rected) edge of the network, there is a pair of arcs, one in each pj ∈ FW r (ti−1 , ci , cj , pi ) and ρ(pj ) = cj where
direction. We provide traces() for each location: ti−1 = (c0 , p0 ), . . . , (ci−1 , pi−1 ). ///

Network region: A network region can only forward previ- The next result shows that packet association corresponds to
ously received packets. Formally: (c1 , p1 ), . . . , (ck , pk ) ∈ the causal relation between inputs and outputs in the network.
traces() iff, ∀i ∈ [1, k], if sender(ci ) = , then there
exists j < i : rcpt(cj ) = , pi = pj . Notice that a network Proposition 6. Let  ∈ LO be a network region or router.
region does not guarantee to deliver every packet, nor to 1. If e = (c, p), e = (c , p ) are associated at  then there
deliver it at most once. exists a trace (c1 , p1 ), . . . , (ck , pk ) ∈ traces() such that
End host: We have no constraint on traces for promiscuous (ci , pi ) = (c, p) ∧ (cj , pj ) = (c , p ) ∧ i < j;
hosts. For chaste ones, we require that the source or des- 2. ∀(c1 , p1 ), . . . , (ck , pk ) ∈ traces(), if sender(cj ) =  then
tination address matches host’s addresses for any packet ∃i < j : rcpt(ci ) =  and (ci , pi ), (cj , pj ) are associated
it sends or receives: (c1 , p1 ), . . . , (ck , pk ) ∈ traces(h) iff at .
∀i ∈ [1, k] : sender(ci ) =  implies sa(pi ) ∈ h and
rcpt(ci ) =  implies da(pi ) ∈ h. Proof. For item (1): Assume  is a network region. Then
Router: When r is a router, then its behavior is determined by msg(e) = p = p = msg(e ). By the behaviour of network
a firewall FW r : T ×CH×CH×P → P(P ). Intuitively, regions (cf. section II-A) we get that (c, p), (c , p ) ∈ traces()
FW r takes a trace t ∈ T , representing the history, an which gives the thesis. If  is a router, thesis is a direct
input and an output channel c and c and a packet p and consequence of definition 5, item 2.
returns a (possibly empty) set of translations of p. Given Item (2) can be trivially derived by the definition of traces
history t, these translations p represent all the possible for network region and routers given in section II-A.
ways in which p is accepted by the firewall when p is A trajectory is a path that a packet may take from the point
received from c and p is delivered to c . Given a firewall it originates through network regions and routers, possibly
FW r and a routing function ρ, the behaviour of the router reaching an end host at which it is received. A trajectory is
is determined as follows: successful if it originates with an end host whose IP addresses
p ∈ FW(t, c, c , p) ρ(p ) = c include its (claimed) source address, and terminates with an
[filterin ] end host whose IP addresses include its destination address.
t, σ;t.(c, p), σ ∪ (c , p )
Thus, at the beginning it is not spoofed, and at the end it is
t, σ {(c, p)};t.(c, p), σ [routeout ] not promiscuously received.

Router configuration is a pair t, σ where trace t repre- Definition 7. Let B ∈ Exc(F) be an execution and let e =
sents the history and σ is a buffer containing pairs (c, p) e0 , . . . ek  be a sequence of events in B. We say that e is a
representing a packet p to be delivered over channel c. trajectory in B iff
Intuitively, rule filterin accepts packet p from channel c, i. 0 ≤ i < j ≤ k implies ei ≺ ej ;
adding it to t, only if there exists p ∈ FW(t, c, c , p) ii. either sender(chan(e0 )) is promiscuous,
that will be delivered over channel c . If this is the case, or sa(msg(e0 )) ∈ IP(sender(chan(e0 )));

196
 iii. either rcpt(chan(ek )) is promiscuous, whose destinations are the publicly accessible web and email
or da(msg(ek )) ∈ IP(rcpt(chan(ek ))); servers, and whose destination ports are the corresponding
iv. if i < k, then rcpt(chan(ei )) is a network region or well-known ports. These provide examples of region control
router, not an end host; statements.
v. for all i such that 0 ≤ i < k, ei , ei+1 are associated. We will always assume that B = E, but there are many
The trajectory e is successful iff useful cases in which the intermediate region R equals one of
the endpoints, i.e. B = R or R = E. We refer to these as
sa(msg(e0 )) ∈ IP(sender(chan(e0 ))) two-region statements, since they just restrict the packets that
da(msg(ek )) ∈ IP(rcpt(chan(ek ))) /// can travel from B to E. When R = E, the statement says
that whenever a packet travels from B to R, it must satisfy
The purpose of course of a network is to allow trajectories φ. Generally speaking, when the purpose of the statement is
to succeed whenever that is compatible with the security goals to protect R from potentially harmful packets from B, this
of the network administrator. form of the statement is useful; the property φ specifies which
When a packet p will be unchanged throughout a trajectory, packets are safe. The two-region formulas may also be used
for instance because the frame involves no network address with R = B to protect B against disclosure of certain packets
translation, we often regard a trajectory as a pair consisting of to E. In this case, the property φ specifies which packets are
the packet p together with a path π, where a path is a sequence non-sensitive.
of adjacent locations. Consider another type of security goal involving three
III. G OALS FOR S ECURITY AND F UNCTIONALITY regions:
Each frame determines a set of trajectories, namely all of Traversal control ψB @B  R  ψE @E: For every trajec-
those compatible with the router configurations and channels tory τ ,
of the frame. In this section we explain how to say which if τ starts at location B with a packet that satisfies ψB ,
of those trajectories are good and which are bad, i.e. how to and τ ends at location E with a packet that satisfies ψE ,
express security goals to govern a frame. In Section IV we then location R is traversed in τ .
will provide an algorithm to determine router configurations As an example of a traversal control statement, consider a
that will enforce a given set of these goals. corporate network that has packet inspection in a particular
region R. Then we may want to ensure that packets from
A. Security Goals public sources B to internal destinations E traverse R. The
We focus on three-region policy statements as security reverse is also important in most cases, i.e. that packets from
goals. We refer to them as region control statements. These internal sources to public destinations should traverse R.
take the following form, in which the region variables B, E, R Given a particular network, i.e. the graph underlying a
each refer to end hosts and network regions, and ψB , ψE , and frame, one strategy to enforce a traversal control statement is
φ refer to sets of packets, determined by the header fields of using region control statements. We may select a suitable cut
the packet at that step in the trajectory: set C of nodes between B and E where R ∈ C. We can then
Region control ψB @B → φ@R → ψE @E: For every tra- implement the traversal control statement by stipulating the
jectory τ , region control statements that for trajectories from B to E, if
if τ starts at location B with a packet that satisfies ψB , the packets traverse any member of C \ {R}, then they satisfy
and τ ends at location E with a packet that satisfies ψE , the always-false header property false. That is, we have the
then if location R is traversed in τ , the packet satisfies family of statements, one for each R = R in C:
φ while at R.
ψB @B → false@R → ψE @E.
In these region control statements, the sets ψB , ψE restrict the
applicability of the security goal: They constrain a trajectory Given this, we will focus our attention on region control
only if they are satisfied at the beginning and end respectively. statements ψB @B → φ@R → ψE @E.
By contrast, φ is imposing a requirement, since the network A trajectory violates a region control statement if it has the
must ensure it is satisfied when the trajectory reaches R. correct beginning and end points, but violates the property φ
Thus ψB , ψE are preconditions and φ is a postcondition, even while at R.
though E is reached last.
Definition 8. A trajectory e = e0 , . . . ek  is a counterexample
We can express many useful properties by suitable choices
to the region control statement ψB @B → φ@R → ψE @E iff
of φ. For instance, we may want to ensure that a packet passing
from B to E undergoes network address translation properly, 1. sender(chan(e0 )) = B and ψB (msg(e0 ));
so that its source address at the time it traverses R is a routable 2. rcpt(chan(ek )) = E and ψE (msg(ek )); and
address rather than a private address. We may want to assure 3. for some i such that 0 ≤ i ≤ k, ¬φ(msg(ei )) and either
that packets from public regions B to a protected corporate sender(chan(ei )) = R or rcpt(chan(ei )) = R.
region E have been properly filtered by the time they reach the When e is not a counterexample we say that e satisfies the
corporate entry network R; thus, they should be tcp packets region control statement ψB @B → φ@R → ψE @E. A frame

197
 F enforces ψB @B → φ@R → ψE @E iff, whenever B ∈
Exc(F) is an execution of F and e is a trajectory in B, then
e satisfies ψB @B → φ@R → ψE @E. ///

B. Functionality Goals
Unlike security goals, which are mandatory, functionality
may be a matter of degree. We choose to measure functionality
by the set of packets that have a successful trajectory (Def. 7).
A successful trajectory is one in which a packet travels from
a non-spoofing producer to a consumer actually located at
the destination address of the packet. We focus on successful
trajectories because we regard spoofing originators as intrin-
sically hostile, which is also the case for promiscuous hosts
that consume packets not addressed to them. We do not care
whether exactly the same paths are available for successful
trajectories, but only that a successful trajectory should exist
Fig. 1. A simple network with two internal and two frontier firewalls.
for as many packets as possible. Thus, we define:
Definition 9. Let F1 and F2 be two frames with the same
underlying graph. splits into at most three goals, each of which applies in only
F2 is at least as successful functionally as F1 iff, for all one of these cases:
locations 0 , 1 , and packets p0 , p1 , if there is a successful (ψB ∧ sa(p) ∈ IP (B))@B → φ@R → (ψE ∧ da(p) ∈ IP (E))@E
(ψB ∧ sa(p) ∈ IP (B))@B → φ@R → ψE @E
trajectory in which p0 starts at 0 and p1 ends at 1 in F1 , ψB @B → φ@R → (ψE ∧ da(p) ∈ IP (E))@E
then there is also a successful trajectory for p0 starting at 0
in which p1 ends at 1 in F2 . /// This decomposition is useful, because when we treat goals
of the first kind, we must be careful to enforce them tightly.
Given an underlying network topology, formalized as a When preventing all counterexamples, we want to ensure that
graph, and a set of security goals, the acceptable frames are any non-counterexample that satisfies the assumptions remains
those that allow no counterexamples to the security goals. possible. These are successful trajectories, and a network that
Among those, one would like to construct a frame that is filters them unnecessarily is less successful functionally than
maximal in the ordering of successful functionality. it could be.
On the other hand, promiscuity goals, i.e. goals of the sec-
C. Forms of Goals ond and third kind, may be enforced cavalierly or brusquely,
i.e. with less attention to allowing as many trajectories as
In the remainder of this paper, we will make an assumption possible compatible with the goals. A trajectory that satisfies
about the sets of security goals we will consider. It is mere the assumptions but is not a counterexample may be filtered
bookkeeping, since any set of goals can be rewritten as a out, since it would not be a successful trajectory. Thus, no
somewhat larger set of goals satisfying this assumption. functionality is sacrificed if it is discarded.
Assumption 10. In any set of security goals to be enforced, For this reason, in this paper we will focus on identifying
for any of those goals ψB @B → φ@R → ψE @E, one of the how to enforce the success goals precisely.
following three cases holds: D. Case Study
1. for all packets p ∈ ψB , sa(p) ∈ IP (B), and We consider the network depicted in Figure 1 composed
for all packets p ∈ ψE , da(p) ∈ IP (E); of three subnetworks Sensitive, Trusted and Untrusted,
2. for all packets p ∈ ψB , sa(p) ∈ IP (B); or two internal firewalls fw1 and fw2, and two frontier firewalls
3. for all packets p ∈ ψE , da(p) ∈ IP (E). fw3 and fw4 connecting to the Internet. This represents a
We refer to these goals as (1) success goals, (2) spoofing goals, typical scenario where internal firewalls filter traffic among
and (3) promiscuous delivery goals respectively. We will call subnetworks while frontier firewalls filter traffic from/to the
goals of the second and third kind jointly promiscuity goals. Internet.
In our example, Sensitive subnetwork contains important
Success goals concern only successful trajectories in which servers and data and is connected to the Internet through the
the packet is not spoofed when created nor delivered promiscu- firewalls fw1 and fw3; Trusted subnetwork is composed of
ously when consumed. Spoofing goals consider only trajecto- trusted hosts that, for example, can access services hosted in
ries with spoofing at creation; promiscuous delivery goals, tra- the Sensitive subnetwork; Untrusted is a wifi subnetwork
jectories with promiscuous delivery. The spoofing and promis- which provides controlled access to the Internet but not to
cuous delivery goals overlap. Any ψB @B → φ@R → ψE @E services hosted in Sensitive. Both Trusted and Untrusted

198
are connected to the firewall router fw2 which in turn is con- NAT nodes traversed along a path as a relation that composes
nected to the other internal firewall fw1, and to the Internet their individual effects; we will identify in Section VI some
through the frontier firewall fw4. assumptions on their network position and behavior.
We illustrate how some security constraints for the example When the network has no nodes configured to do network
network can be naturally specified in the form of security address translation, then every trajectory has the same packet
goals. The full specification of security goals will be given throughout. Thus, only the position of the packet changes
in V-C. as it progresses; its headers remain the same. This leads to
two simplifications. First, it is easy to compare a property of
Example 11 (Network isolation). We require that hosts in
headers at one location with the effects it has at other locations;
the Sensitive subnetwork never connect to Untrusted and
for instance, when packets not satisfying φ are discarded at
vice-versa. This is naturally expressed through two-region
some point of a path, the consequence is that packets reaching
statements in which R corresponds to B or E (cf. Sec-
some subsequent point along that path satisfy φ. Second, non-
tion III-A). We write false to denote an unsatisfiable constraint
simple paths, which may revisit the same node more than once,
corresponding to the empty set of packets.
never create any new behavior. Since the only effect of a router
Sensitive → false@Sensitive → Untrusted may be to discard packets, the set of packets that can traverse
Untrusted → false@Sensitive → Sensitive a path is a subset of the packets that can traverse any of its
subpaths. Hence if any traversal provides a counterexample to
In the first rule we block packets directly at the source, in a security goal, then we may assume that it is the result of
order to protect against disclosure of packets starting from appending two simple paths, one from the beginning region
Sensitive and directed to Untrusted. In the second rule, we B to the intermediate region R, and another from region R
prevent potentially harmful packets, originated in Untrusted, to the end region E. In subsequent sections we will lift these
from entering Sensitive. simplifications, but the backbone of our analysis will be clearer
Example 12 (Typical firewall rule). We let Sensitive access in an exposition that can rely on them.
the Internet only via https (destination port 443). We write Specifying which packets to keep. We focus on the success
dp 443 to denote all packets with destination port 443. goals. Fix a particular pair of endpoints B, E. Thus, we have
a collection of statements of the form ψB @B → φ0 @R →
Sensitive → dp 443@Sensitive → Internet
ψE @E; because these are success goals, ψB , ψE ensure that
As above, we constrain packets directly at the source in order packets contain suitable addresses:
to prevent disclosure. In particular, notice that packets will
ψB (p) ⇒ sa(p) ∈ IP (B) and ψE (p) ⇒ da(p) ∈ IP (E).
never leave Sensitive unencrypted.
Example 13 (Traversal control and three region rules). Different goals in this collection may have different choices of
Untrusted should access the Internet exclusively through ψB and ψE . Since trajectories do not alter packet properties
fw3 on port 80. This is a form of traversal control that can be in the no-NAT case, we can equivalently rewrite them to use
compiled into region control rules by taking cut {fw3, fw4} uniform guards by replacing them with this equivalent form:
and forbidding traversal of everything but fw3, i.e., fw4 (cf. [sa(p) ∈ IP (B)]@B → [ψB ∧ ψE ⇒ φ0 ]@R → [da(p) ∈ IP (E)]@E
Section III-A). In a real setting, we might require this because
fw3 is more powerful than fw4; for instance, when it can Thus, we have essentially moved the variability in ψB , ψE
handle complex (stateful) protocols and can audit what the from the endpoints to R, creating a new formula φ1 at R. Thus,
untrusted users do. we will now assume that all B, E goals have the same guard
formulas at B and E, namely sa(p) ∈ IP (B) and da(p) ∈
Untrusted → dp 80@fw3 → Internet
IP (E). We will however keep writing φ for the generic form
Untrusted → false@fw4 → Internet
of a formula required at the intermediate location R, even if
Notice that we cannot express the above goals using only it has been rewritten as shown above.
two regions since they specify different requirements on the Fix a choice of B, E. We will write PB,E for the set of
traversed intermediate nodes. packets with sa(p) ∈ IP (B) and da(p) ∈ IP (E).
IV. L OCALIZING S ECURITY P OLICIES W ITHOUT Definition 14. Suppose given a non-empty collection G
N ETWORK A DDRESS T RANSLATION of success goals rewritten if necessary to produce uniform
In this section, we describe how to assign filtering func- ψB , ψE . We define PrmtB,E () to be:
tionality to routers so as to enforce a set of region control 
PrmtB,E () = PB,E ∩ φ ,
statements. For this, we will develop our method based on a
φ
well-known matrix-based algorithm. To explain it, we will start
from the traditional version, which is applicable in the special taking the intersection over all of the φ such that a formula
case where the network has no nodes that perform NAT. If there ψB @B → φ @ → ψE @E appears in G. We may write
are NAT nodes, we need to represent the effect of the various Prmt() whenever B, E are clear from the context. ///

199
 Thus, PrmtB,E () always includes the packets which are We would like now to filter packets as they are passing from
permitted to appear in , as part of a successful trajectory one location to another location at which they should not be
from B to E. A packet is worth keeping at a location if it kept, i.e., we should discard the complement of KEEP∗ ( )
can use that location to get from B to E along some path that along any edge a :  →  . We summarize this idea in filters for
traverses only locations at which it is permitted: the arcs a :  →  . Since below we use the complement, the
set of packets that should be accepted along a, we formalize
Definition 15 (Keep). Packet p ∈ PB,E is worth keeping along
that as the accept filter af.
path π from B to E iff, for every  along π, p ∈ PrmtB,E ().
Packet p ∈ PB,E is worth keeping from B to E at  iff there Definition 18. The acceptance filter af is the function from
exists some π such that π leads from B to E and traverses , arcs to sets of packets defined af(a) = KEEP∗ ( ), when a :
and p is worth keeping along path π.  →  is an arc from  to  . We also write af(,  ) for af(a).
We write KEEPB,E () for the set of p ∈ PB,E worth We define the redundant filter of an arc a :  →  from 
keeping from B to E at . We write KEEP() whenever B to  as rf , = KEEP∗ () ∩ KEEP∗ ( ). ///

and E are clear from the context. ///

Intuitively, af assumes that all firewalls cooperate, while rf
If a packet is permitted at all locations along some path from redundantly re-enforces filtering at each firewall. Thus, when
B to E that passes through , then it is certainly permitted at all firewalls behave according to their specifications, af and
location : rf have exactly the same effect. However, rf is more robust if
any firewalls may be compromised.
Lemma 16. If p ∈ KEEPB,E (), then p ∈ PrmtB,E (). As mentioned before, we always require that B = E in any
goal statement.
Notice that a packet going from B to E is permitted at
a given location  only if it does not contradict any of the Theorem 19 (Filter security). Let G be a non-empty collection
possible region control rules. So, for a packet to be worth of success goals, for a NAT-free frame. Let e = e0 , . . . ek 
keeping from B to E, it is enough if there is a single be a success trajectory such that sender(chan(e0 )) = B and
path π in which p is allowed to traverse all locations of π. rcpt(chan(ek )) = E. Suppose that, for all 0 ≤ i ≤ k and
However, to ensure that packets use these locations only to locations ,  , if sender(chan(ei )) =  and rcpt(chan(ei )) =
follow permissible paths requires the filters we will generate  , then
in Def. 18. Case 1. msg(ei ) ∈ af(,  )
By the second of the simplifications mentioned at the Case 2. msg(ei ) ∈ rf(,  ).
beginning of Section IV, this definition is unchanged whether Then e satisfies all of the success goals ψB @B → φ@R →
we consider all π or only the paths π in which the part before ψE @E in G.
 is simple, and the part after is too.
The direct way of computing KEEP() would thus be to Proof. First, since we are assuming that there are no NATs,
examine every simple path π1 from B to , and every path π2 we have a p such that, for all i, msg(ei ) = p. Since e is a
from  to E, taking an intersection of the p ∈ PB,E permitted success trajectory, sa(p) ∈ IP (B) and da(p) ∈ IP (E).
at every step of π1 π2 , and combining the results via a union 1. First suppose that R = B. If e never traverses R, then the
over all choices of π1 and π2 . We present a simpler way using success goal is vacuously satisfied. So let ei be the earliest
matrix multiplication in Section IV. event such that rcpt(chan(ei )) = R. By the definition of af,
Combining the keep sets for different endpoints. When p ∈ KEEP(R). By Lemma 16, p ∈ Prmt(R). So p satisfies φ.
we define KEEPB,E , we work only with packets p ∈ PB,E . If R = B, then we use the fact that B = E. Thus,
We will now assume: p traverses at least one edge to rcpt(chan(e0 )). Hence,
p = msg(e0 ) ∈ af(B, rcpt(chan(e0 ))). By the definition,
Assumption 17. For all locations ,  , if  =  , then IP () ∩ p ∈ KEEP(rcpt(chan(e0 ))). Hence, there is at least one path
IP ( ) = ∅. π that traverses rcpt(chan(e0 )) such that p ∈ Prmt() for
Hence these packets are disjoint from the packets of interest every  along π. But B appears at the beginning of every path
when computing any other KEEPB  ,E  . Thus, we may simply (including π) from B to E. Thus, p ∈ Prmt(B), so p satisfies
repeat the computation for each distinct pair B, E, accumu- φ.
lating the union of the KEEP sets for each . 2. The preceding argument applies a fortiori, since rf(a) ⊆
The resulting union consists of all packets that may traverse af(a) for every a.
 along a successful trajectory from the stated source to the
Moreover, af is maximally successful among all filtering
stated destination without encountering a location at which it
strategies that enforce the success goals. That is, any assign-
is not permitted. Thus, we may define, for a given set of goal
ment of filters that permits additional successful trajectories
statements G:
allows counterexamples to some goal. Indeed, we prevent a

KEEP∗ () = KEEPB,E () (1) successful trajectory only if that trajectory is incompatible with
B,E
the security goals.

200
Theorem 20 (Maximal success). Suppose that f is a function Since every (simple) path visits each node at most once, it
from arcs to sets of packets, and for all a :  →  , either is no longer than |N |, the cardinality of the set of nodes. As
Case (a) af(a) ⊆ f (a), or else remarked above, non-simple paths allow no additional packets,
Case (b) rf(a) ⊆ f (a). since they subject the packets to additional constraints. Thus,
Suppose that τ is a successful trajectory compatible with the sequence stabilizes by Rchb where b = 21+log2 |N | , and
f but not with the selected filters af or rf. Then τ is a we define:
counterexample to some success goal. Rch = Rchb is the fixed point of Rchm .
Proof. Assuming case (a): Since τ is incompatible with af, Observe that this computation requires O(log2 |N |) matrix
it traverses some edge a :  →  such that, letting the packet multiplications to reach its fixed point, and is thus tractable
of τ be p, p ∈ KEEP∗ () but p ∈ KEEP∗ ( ). Therefore there for large |N |, assuming that the underlying ring operations on
is no path π from the start of τ to its endpoint that traverses sets are tractable.
 such that p ∈ Prmt(1 ) for all 1 along π. Lemma 21. For a configuration without NAT or other packet
Assuming case (b): Since τ is incompatible with rf, it transformations, KEEP(i) = RchB,i ∩ Rchi,E .
traverses some edge a :  →  such that, letting the packet of Proof. Set RchB,i ∩ Rchi,E contains all packets p ∈ PB,E
τ be p, p ∈ KEEP∗ () or p ∈ KEEP∗ ( ). Therefore, letting that can reach i from B and then E from i while traversing
 be either  or  , there is no path π from the start of τ to only locations n such that p ∈ PrmtB,E (n). Thus, p belongs
its endpoint that traverses  such that p ∈ Prmt(1 ) for all to RchB,i ∩ Rchi,E if and only if p ∈ PB,E and there exists
1 along π. some π such that π leads from B to E and traverses i, and
Hence, in either case (a) or case (b), the sequence of locations for every  along π, p ∈ PrmtB,E (). By Definition 15 we
traversed in τ is not such a path. Thus, τ is a counterexample directly obtain RchB,i ∩ Rchi,E = KEEP(i).
to some goal between these endpoints.
Tightening given filters. Suppose we want to calculate the
Computing the sets to keep. Observe that sets of packets success filters relative to some given filters f (e, d), where e
form a boolean algebra, and therefore surely a ring where is an edge, d is a direction (inbound vs. outbound), and the
∩ is the multiplication and ∪ is the addition. In particular, resulting value f (e, d) is the set of packets we will permit to
∩ distributes over ∪. Thus, we can form matrices of sets, travel along edge e in direction d. We would like to derive
and matrix multiplication accumulates the ∪ of the ∩s of maximally permissive filters that tighten the given ones and
corresponding elements. I.e. if we define the inner product enforce the goal statements. To do so, instead of starting with
a · b to be:  the adjacency matrix A, we define Af to have the entry f (e, d)
(a[i] ∩ b[i]), in position Afi,j if edge e leads from location i to location j
i when traversed in direction d. Like A, it contains the empty
then the matrix multiplication A B yields C, where Cij = set whenever i and j are not adjacent. The successive matrices
ai ·bj using the ith row vector of A and the j th column vector Rch0 , Rch1 , . . . , Rchm are now computed as before, starting
of B. Let: with matrix Af .
A be the adjacency matrix for the graph, where if there is an For instance, we might like to use this idea to protect ter-
edge from node i to node j, then the entry Aij is the top minal networks—meaning a network segment  with just one
element, i.e. the set of all packets. Aij = ∅ if i, j are not connection to the remainder of the network—from inappro-
adjacent. priate packets. Suppose that a  contains IP addresses IP ().
K be the diagonal matrix with entries Ki,i = Prmt(i). Thus, the remainder of the network has the complementary set
of IP addresses IP ().
We want to compute the matrices Rchm such that each entry
Then we would like to permit packets p outbound only if
Rchm i,j is the set of p ∈ PB,E that can reach node j from sa(p) ∈ IP () and da(p) ∈ IP (). We would like to permit
node i along a path of length ≤ m while traversing only
packets p inbound only if da(p) ∈ IP () and sa(p) ∈ IP ().
locations n such that p ∈ Prmt(n).
Edges that do not connect a terminal network retain their
We claim: original specification of allowing all packets. This leads to
Rch0 = K, since paths of length 0 lead only from i to i, and a useful policy Af to start from in computing the sets Rch.
Ki,i is the set of packets permitted there.
Firewall Configuration. We now define firewall behaviour
Rch1 = K + (K A K). A path of length ≤ 1 is either empty
FW based on the KEEP∗ sets. We consider the case of nodes
or else it takes one step from i to an adjacent location
connected to at least one firewall or, in other words, we assume
j; moreover, the packet should satisfy Prmt(i) before the
that any edge in the network has filtering capabilities.
step and Prmt(j) after it.
Rch(2m) = (Rchm Rchm ), since the paths of length ≤ 2m are Definition 22. For each firewall f , consider any input and
just the paths that divide into two paths of length ≤ m, output channels ci and co such that rcpt(ci ) = f and
respectively ending and beginning at the same node k. sender(co ) = f . Let i and o be the two locations connected

201
to ci and co , i.e., i = sender(ci ), rcpt(co ) = o . Then we We notice that the above rules enable the path Untrusted,
define a firewall as: fw2, fw1, fw3, Internet for packets with destination port

{p} if p ∈ af i ,f ∩ af f ,o 80. Packets trying to reach fw4 from fw2 are dropped in fw2.
FW a (t, ci , co , p) 
{} otherwise V. S EMANTIC BASED I MPLEMENTATION
and, similarly, a redundant firewall as: The theory developed so far considers a very general notion

{p} if p ∈ rf i ,f ∩ rf f ,o of firewall FW whose behaviour depends on the firewall
FW r (t, ci , co , p)  history and on the actual input and output channels. We now
{} otherwise ///
show how this general notion can be implemented using an
Intuitively, a firewall without network address translation extension of Mignis [1], a semantic based tool for firewall
accepts a packet p whenever p is accepted on both the input configuration in Linux systems. Mignis has a formal semantics
and the output channels, i.e., whenever p belongs to af i ,f ∩ that permits us to formally prove correctness with respect
af f ,o , or to rf i ,f ∩ rf f ,o for the redundant firewall. to our frame semantics and, at the same time, is provided
Theorem 23. Let G be a non-empty collection of success with an open-source compiler,1 that will allow us to produce
goals. If each channel is connected to at least one router and working Linux firewalls, as illustrated in Section V-B. Notice
the behaviour of all routers is determined by FW a (t, ci , co , p) that Mignis is a general firewall language and is not tailored
or FW r (t, ci , co , p), then frame F enforces G. only to Linux systems. Thus, in principle, Mignis could also
generate configurations for other firewall systems.
Proof. Suppose that, in order to get a contradiction, the
firewalls are defined as above but frame F does not enforce A. Mignis and its Semantics
some goal of G. This means that there is a goal ψB @B → Mignis [1] is a declarative specification language in which
φ@R → ψE @E, an execution B of F, and a trajectory the order of rules does not matter. This makes the specification
e = e0 , . . . ek  in B such that e is a counterexample for of a firewall very close to its semantics: a packet goes through
this goal. By Theorem 19, there exists 0 ≤ i ≤ k such that (possibly translated) only if it matches a positive rule and is
msg(ei ) ∈ af(,  ) and msg(ei ) ∈ rf(,  ) not explicitly denied. This allows administrators to write and
Recall that B and E are required to be end hosts and inspect rules independently of the order in which they are
cannot be routers. By hypothesis we have that any edge specified. Moreover, the declarative approach makes it easy
of F has at least one firewall so, if the firewall is lo- to detect possible conflicts and redundancies and to query for
cated at  we consider the incoming event ei−1 (from i a subset of the specification involving specific hosts. Mignis
to ) and we obtain FW a (t, chan(ei−1 ), chan(ei ), p) = {}, supports Network Address Translation (NAT), i.e., it allows the
FW r (t, chan(ei−1 ), chan(ei ), p) = {} as p ∈ / af(i , ) ∩ translation of the source and destination addresses of a packet
af(,  ), p ∈ / rf(i , ) ∩ rf(,  ); if the firewall is located while it crosses the firewall, and it applies the translation
at  we consider the outgoing event ei+1 (from  to consistently to all packets belonging to the same connection.
o ) and again FW a (t, chan(ei ), chan(ei + 1), p) = {} and Mignis rules are defined in terms of address ranges n. An
FW r (t, chan(ei ), chan(ei + 1), p) = {} , as p ∈ / af(,  ) ∩ address range n is a pair consisting of a set of IP addresses
af( , o ), p ∈
/ rf(,  ) ∩ rf( , o ). and a set of ports, denoted IP (n):port(n). Given an address
In both cases, the router behaviour defined in Section II addr, we write addr ∈ n to denote port(addr) ∈ port(n), if
enforces that the p is blocked hence we get a contradiction on port(addr) is defined, and IP (addr) ∈ IP (n). Notice that if
the existence of the counterexample trajectory. addr does not specify a port (for example in ICMP packets)
Example 24 (Localization of traversal control). Consider we only check if the IP address is in the range. We will use the
again the traversal control rules of Example 13: wildcard ∗ to denote any possible address or port or address
range, and to denote a special range consisting of a special
Untrusted → dp 80@fw3 → Internet address addr used to note void translations.
Untrusted → false@fw4 → Internet Syntax: We present a version of Mignis (that we call
We show how they are localized using the redundant fire- Mignis+ ) that extends the original one in various respects: (i)
wall FW r (t, ci , co , p). We only report cases where we have rules are localized on channels CH in order to allow for packet
nonempty set of packets and we write Un for Untrusted and filtering that depends on the network topology; (ii) packets
Int for Internet: on established connections are not accepted by default; (iii)
 rules are all positive. Mignis+ is slightly more complex to use
{p} if dp 80(p)
FW 1r (t, (fw2, fw1), (fw1, fw3), p)  but strictly more expressive than the original one. Since we
{} otherwise
 will generate Mignis+ configurations automatically we do not
{p} if dp 80(p) consider the increased complexity as a problem. The Mignis+
FW 2r (t, (Un, fw2), (fw2, fw1), p) 
{} otherwise syntax follows:

{p} if dp 80(p)
FW 3r (t, (fw1, fw3), (fw3, Int), p)  r ::= ns [nts ] @ cs > nd [ntd ] @ cd : φ
{} otherwise
FW 4r (t, ci , co , p)  {} 1 [Link]

202
 [[]] t ci co p  {}
[[ns [nts ] @ ci > nd [ntd ] @ co : φ ; C]] t ci co p  [[C]] t ci co p
⎧
⎨ {p[sa → as , da → ad ] | as ∈ ns , ad ∈ nd }
t t t t t t

∪ if ci = ci , co = co , φns ,nd (p, t)

⎩
{} otherwise
TABLE II
Mignis+ SEMANTICS .

where φ is a predicate that is checkable over a packet and the C composed of a single rule:
firewall state (represented in terms of a trace, as defined in
∗@eth0 > [Link]:80@eth1 [[Link]:80] : tcp
Section II-A). Intuitively, this rule accepts a packet p from ns
to nd that is received from channel cs and is routed to channel where we omit writing the void [ addr ] source NAT, for
cd whenever φ(p, t) holds. Packet p’s source and destination readability, and where tcp corresponds to a predicate that holds
addresses are translated into different ones belonging to nts if and only if p is a tcp packet. We have:
and ntd in order to support NAT. When nts and ntd are the rule
leaves the addresses unchanged. When, instead, nts and ntd are [[C]] t ci co p = {p[da → [Link]:80]}
different from , they respectively correspond to source and if da(p) = [Link]:80, ci = eth0, co = eth1, tcp(p).
destination NATs, and if both source and destination NATs are This firewall will accept any tcp packet from eth0 with desti-
specified they are combined together.2 A sequence of these nation [Link]:80 on eth1 and will translate its destina-
firewall rules is called a configuration, C ::= r; C |  tion to [Link]:80. For example, let p be a tcp packet
Semantics: Mignis implements NAT by keeping track of the with source [Link]:5656 and destination [Link]:80.
established connections and the relative address translations. In We have [[C]] t eth0 eth1 p = {p[da → [Link]:80]}.
this paper we represent Mignis+ state as a trace representing Notice that packet being tcp is independent of the firewall
previous sent and received packets with the respective chan- history t, so firewall semantics does not depend on t in this
nels, as defined in Section II-A. Let P K = [(CH × D)∗ → specific example.
CH → CH → P → P(P )] be the domain of packet
transformers. We define [[·]] : C → P K, i.e., a function B. A Tool for Firewall Localization
mapping a Mignis+ configuration C into a packet transformer, We have implemented a tool that given a network specifi-
representing all the accepted packets with the corresponding cation and a set of region control rules automatically localizes
translations. [[·]] t ci co p is defined inductively in Table II, the filters and generates Mignis+ configurations for all the
where φns ,nd (p, t)  sa(p) ∈ ns ∧ da(p) = nd ∧ φ(p, t) firewalls in the network. We have also modified the original
and p[sa → ats , da → atd ] denotes packet p where sa(p), Mignis compiler by incorporating the extensions illustrated
respectively da(p), is replaced by ats , respectively atd , if it in section V-A in order to produce the actual Linux firewall
is different from the void address addr , and left unchanged (Netfilter) configurations. The tool is implemented in Python3.
otherwise. Network: We consider a network consisting of firewalls and
Intuitively, the empty configuration  corresponds to the end hosts, and we assume that each channel has at least one
empty set. For a configuration ns [nts ] @ ci > nd [ntd ] @ co : firewall endpoint. This ensures that all edges can filter packets.
φ ; C we take all the packets that are received on ci , routed Constraints: Given rule ψB @B → φ@R → ψE @E, we
on co and satisfy φns ,nd (p, t), whose addresses are translated specify constraints ψB , ψE and φ as Boolean expressions over
along non- NATs nts , ntd , together with the packets returned variables representing the following facts:
by the remaining rules in C. By taking this union with the Source and destination address whenever a packet has
remaining rules in C we are indeed considering that there is source or destination address of end host h, written sa h
no ordering in the rules of a Mignis+ configuration. and da h, respectively;
Source and destination port whenever a packet has a source
Definition 25 (Mignis+ firewall). Given a Mignis+ config-
or destination port n, written sp n and dp n, respectively;
uration C, we let FW(t, c, c , p)  [[C]] t c c p.
Protocol whenever packet protocol is p, written pr p;
Example 26. Consider a destination NAT that translates all tcp Established whenever a packet belongs to an established
incoming packets from interface eth0 directed to [Link] connection, written est.
port 80 on interface eth1, into address [Link] on the For example, sp 443 & est requires that the source port is
same port. In Mignis+ this is specified through a configuration 443, and that packets belong to an established connection.
This is a typical example of a response from a SSL web
2 Notice that square brackets are used consistently to note the translated
server. Notice that we use notations &, | and ∼ to represent
addresses. This differs from the original Mignis notation for destination NATs Boolean AND, OR and NOT, respectively. Rules apply only to
which encloses in square brackets the address before translation, i.e., nd . non-spoofed, non-promiscuous packets. This is automatically

203
enforced by requiring ψB &sa B and ψE &sa E in place of ψB Sensitive to Trusted only if they do not belong to estab-
and ψE . lished ssh connections:
Localization: We compute localization as described in
section IV. At the moment the prototype only supports the case Trusted → dp 22@Sensitive → Sensitive
without NATs described in section IV. We leave the extension Sensitive → (sp 22&est)@Sensitive → Trusted
to NATs as a future work. Constraints are represented as Trusted → false@Internet → Sensitive
reduced, ordered binary decision diagrams (ROBDD) [4]. We Sensitive → false@Internet → Trusted
base our implementation on the Python EDA library that sup-
Sensitive should access the Internet only via https (des-
ports both Boolean algebra and ROBDDs.3 The advantage of
tination port 443), while Internet hosts should never start
adopting ROBDD representation is that it is a canonical form
new connections towards Sensitive:
and makes it very efficient to compute equivalence between
Boolean expressions, which is useful to determine when the Sensitive → dp 443@Sensitive → Internet
computation of Rch stabilizes. Set union and intersection used Internet → (sp 443&est)@Sensitive → Sensitive
for localization in section IV naturally become OR and AND
Boolean operators over ROBDDs. Trusted has full access to the Internet and from the
Firewall configuration: Once we obtain FW a (t, ci , co , p) Internet we give access to Trusted only via ssh (port 22).
or FW r (t, ci , co , p) in the form of a Boolean expression When full access is granted, we do not specify any region
we generate Mignis+ configurations by instantiating the ex- control statement, but we still need to let established packets
pression with the source and destination addresses of any go through:
possible end host, and by computing the solutions of the
obtained boolean expression. It is worth noticing that Python Internet → (dp 22|est)@Trusted → Trusted
EDA transparently invokes PicoSAT solver 4 to efficiently
solve a Boolean expression. Solutions are then translated into Untrusted should access the Internet exclusively through
constraints over ports, protocol and established state. fw3 on port 80. This is a form of traversal control that can be
compiled into region control rules by taking cut {fw3, fw4}
C. Case Study in Detail and forbidding traversal of everything but fw3, i.e., fw4 (cf.
Example 13, Section III-A). Internet should never access
We now define the security goals for the example network Untrusted:
of Figure 1 and discussed in Section III-D.
As already mentioned, firewalls usually keep track of es- Untrusted → dp 80@fw3 → Internet
tablished connections so that packets belonging to the same Internet → (sp 80&est)@fw3 → Untrusted
connections are not filtered. This is particularly useful to en- Untrusted → false@fw4 → Internet
able bidirectional communication without necessarily opening Internet → false@fw4 → Untrusted
the firewall bidirectionally to a new connection: it is enough to
open the firewall in one direction and let established packets Localizing filtering: Table III in the Appendix reports the
come back. We write est to note that a packet is established output of the localization tool that automatically generated
(cf. Section V-B). While specifying rules, we proceed pair by the Mignis+ configuration for the four firewalls according to
pair, defining the rules and their established counterpart (when FW r (t, ci , co , p). Channels/interfaces are named with prefix
needed) at the same time. if_ to distinguish them from network end hosts. For example,
Hosts in the Sensitive and Trusted subnetworks should the first group of rules for firewall fw1
never connect to Untrusted and vice-versa. This is naturally Sensitive@if_Sensitive:22 > Trusted@if_fw2 | -m ...
expressed through two-region statements (cf. Example 11, Sensitive@if_Sensitive > Internet@if_fw2:443
Section III-A):
refer to interfaces if Sensitive and if fw2, i.e., packets
Sensitive → false@Sensitive → Untrusted coming from the channel connecting Sensitive to fw1 and
Untrusted → false@Sensitive → Sensitive delivered over the channel from fw1 to fw2. Established
Trusted → false@Trusted → Untrusted requirement is translated into the low level syntax of Linux
Untrusted → false@Trusted → Trusted firewall:
-m state --state ESTABLISHED,RELATED
Hosts in the Sensitive subnetwork should never connect
to Trusted, while hosts from Trusted network can access We can see that, on these two channels, firewall fw1 only
Sensitive via ssh through fw1 without passing through allows packets from Sensitive to Trusted on established
the Internet as this would unnecessarily expose network ssh connections and new https connections from Sensitive
connections to attacks. Notice that we filter packets from to Internet, as required by the region control rules:

3 [Link] Sensitive → (sp 22&est)@Sensitive → Trusted

4 [Link] Sensitive → dp 443@Sensitive → Internet

204
We illustrate in detail how the following rules, permitting 2. is associative, (R S) T = R (S T ); and it
access from Unstrusted to Internet only on port 80 has unit the identity relation Id, meaning R Id = R.
through fw3, are localized in the firewalls: The former is the equivalence:
Untrusted → dp 80@fw3 → Internet (∃z . (∃y . R(x, y) ∧ S(y, z)) ∧ T (z, w)) ≡
Internet → (sp 80&est)@fw3 → Untrusted (∃y . R(x, y) ∧ (∃z . S(y, z) ∧ T (z, w)))
Untrusted → false@fw4 → Internet while the latter says that
Internet → false@fw4 → Untrusted
∃y . R(x, y) ∧ y = z ≡ R(x, z).
The relevant rules are:
FIREWALL fw1
3. distributes over ∪:
Untrusted@if_fw2 > Internet@if_fw3:80
Internet@if_fw3:80 > Untrusted@if_fw2 | -m ... R (S ∪ T ) = (R S) ∪ (R T ) and
(S ∪ T ) R = (S R) ∪ (T R).
FIREWALL fw2
Untrusted@if_Untrusted > Internet@if_fw1:80 We check the former, via the definitions, distributing ∧
Internet@if_fw1:80 > Untrusted@if_Untrusted | -m ...
over ∨:
FIREWALL fw3
Internet@if_Internet:80 > Untrusted@if_fw1 | -m ...
(R (S ∪ T ))(x, z)
Untrusted@if_fw1 > Internet@if_Internet:80 ≡ ∃y . R(x, y) ∧ (S(y, z) ∨ T (y, z))
≡ ∃y . (R(x, y) ∧ S(y, z)) ∨ (R(x, y) ∧ T (y, z))
Firewall fw1 allows for traffic between fw2 and fw3 on the ≡ (∃y . R(x, y) ∧ S(y, z)) ∨ (∃y . R(x, y) ∧ T (y, z))
required ports and firewalls fw2 and fw3 enable traffic through ≡ ((R S) ∪ (R T ))(x, z)
fw1. Packets from Untrusted to Internet are dropped in
fw4 (which contains no rule between those two end hosts), To check the latter, we use almost the same argument,
and on the link from fw2 to fw4, as required. Recall that but inverting the arguments; the commutativity of ∧ and
Mignis has a default drop policy, so if no rules for two end ∨ justifies the way we write this:
hosts exist packets will be dropped. ((S ∪ T ) R)(z, x)
VI. L OCALIZING WITH NATS ≡ ∃y . R(y, x) ∧ (S(z, y) ∨ T (z, y))
≡ ∃y . (R(y, x) ∧ S(z, y)) ∨ (R(y, x) ∧ T (z, y))
In the more general case, we use the same ideas, although ≡ (∃y . R(y, x) ∧ S(z, y)) ∨ (∃y . R(y, x) ∧ T (z, y))
with a different ring. In this case, instead of the ring of sets of ≡ ((R S) ∪ (R T ))(z, x)
packets under ∪ and ∩, we use a ring of relations on packets.
The addition-like operator is again ∪, but the multiplication- We may also regard each set of packets φ(p) as “lifting” to
like operator is now the relative product R S of binary the binary relation φ(p) ∧ p = p , i.e. the lifted version of φ
relations: is the intersection ↑ φ = Id ∩ (φ × φ).
Agreeing on goals across NATs. Consider the network:
(R S)(x, z) iff ∃y . R(x, y) ∧ S(y, z)
B1 C (2)
We will next verify that these operations do form a ring.
After that, we face two additional hurdles. First, we cannot N E
hope to enforce goals in an exact way if different regions B2 D
behind the same NAT are subjected to different security poli-
where we are interested in the packets that are permitted
cies. By the time that packets emerge through the NAT, we
to travel from either B1 or B2 through the source NAT
cannot tell in which region they originated, and thus cannot
device N to E. However, they must satisfy different properties
differentiate their filtering according to their origins. Second,
depending on which intermediate node C, D they traverse. In
we need an analogue to Assumption 17, which ensured that
particular, successful trajectories from B1 to E that traverse C
we could compute the KEEP sets for different endpoints B, E
must have property φ, while successful trajectories from B2 to
separately, and combine the results by taking disjoint unions.
E that traverse C must have property ¬φ. On the other hand,
Instead, we will assume that the external IP addresses of any
successful trajectories from B1 to E that traverse D must have
distinct NAT devices accessible to any location R are disjoint.
property ¬φ, while successful trajectories from B2 to E that
Union and relative product form a ring. We will check traverse D must have property φ.
that this does form a ring, although it is not a commutative Unfortunately, we do not want to enforce this requirement
ring. This suffices to allow us to use the methods we have just before traversing the NAT N , because we do not yet know
described. We will also point out below that—for the NAT- whether the packets will traverse the route through C or
based packet transformations that interest us—there are simple through D. We would need to discard all the packets for
and efficient ways to represent the relations that arise in our E. And we do not want to enforce this requirement after
computations. traversing the NAT N , because we do not know whether the
1. ∪ is associative, commutative, and has unit ∅. packets originated at B1 or B2 . We would again have to

205
discard them all, since N has rewritten their source addresses Keep sets with NATs. With NATs, packets are no longer
to its own external address. unchanged throughout a trajectory. We need to account for
Since the goals differentiate the packets by the source these changes, as the packets have different fields at each node,
behind the NAT, we cannot enforce them tightly. To prevent and those fields define if the node keeps or discards the packet.
non-φ packets that originated at B1 from traversing C, we Fix a choice of endpoints B, E. Unlike the NAT-free case,
must also discard non-φ packets that originated at B2 . we cannot simply move the preconditions ψB , ψE of a success
Hence, all origins beyond a source NAT must be subject to goal from the beginning and end of a trajectory to the region
the same policy. Indeed, a purpose of the NAT is to make those R. After all, NAT transformations may have altered the packet
packets indistinguishable. headers between B and R, or R and E. Instead, we will use
In particular, consider triples of locations B1 , R, E and the relations to keep track of both the state of the packet at
B2 , R, E, where R is separated from B1 , B2 by at least one the earlier point and the later point. For this reason, we will
NAT. Then for every goal for B1 , R, E, there should be a goal now alter the set PrmtB,E (·) to a pair of relations on packets.
for B2 , R, E that is at least as restrictive, and conversely. In PrmtB,R concerns the “left” half of the trajectory from B to
this case, we can say that B1 , B2 are region of origin equi- R; PrmtrR,E concerns the “right” half from R to E. Since
goals for R, E. A similar notion of destination equi-goals B, E are fixed, we do not indicate them here; we focus on R.
applies to E1 , E2 . We can expect to enforce a policy tightly If G is a set of success goals, we will write G(B, R, E)
only when it ensures equi-goals across NATs both for regions for the subset of G concerning B, R, E. If g ∈ G(B, R, E)
of origin and destinations. is a goal ψB @B → φ@R → ψE @E, we will write P REB (g),
Networks with NATs: Assumptions. In real life, NATs are P OST(g), and P REE (g) for ψB , φ, and ψE , resp.
used in very specific ways. First, because the source NAT PrmtB,R =
functionality must always be applied to outgoing packets, and {(p, q) : g∈G(B,R,E) sa(p) ∈ IP (B) ∧ (P REB (g)(p)
reversed when packets return in response—and conversely for ⇒ P OST(g)(q))}
destination NATs—the NAT must separate the portion of the PrmtrR,E =
network using private addresses from the remainder of the {(q, p) : g∈G(B,R,E) da(p) ∈ IP (E) ∧ (P REE (g)(p)
network. We will here also assume an all-or-nothing NAT ⇒ P OST(g)(q))}.
policy, namely that if a router provides NAT service for one
host that reaches it on a particular interface, then it does so PrmtB,R contains a pair (p0 , q0 ) when p0 satisfies the pre-
for all hosts reaching it on that interface. condition P REB at the beginning B, and q0 satisfies the claim
P OST(g) property at R, meaning that if a packet could follow
Assumption 27. If a router  provides NAT functionality, then
some path that would transform it from p0 to q0 , then this
the singleton {} is a cut set partitioning LO \ {} into an
would be allowed by the goal statements. Conversely for
inside using private addresses and an outside.
(q1 , p1 ) ∈ PrmtrR,E , if q1 could follow some path to E that
NAT s can be arranged in several layers, so that addresses would transform it to p1 , then the goal statements would allow
used outside an “inner” NAT may include private addresses this. A packet q is worth keeping at a given location if there
served by a subsequent “outer” NAT. Nevertheless, at any point is some real path that leads through R which does transform
of the network, the IP addresses that are locally visible should it in ways that remain permissible:
be disjoint, in an analogue of Assumption 17: Definition 30 (NAT-Keep). If e = e0 , . . . ek  is a tra-
Assumption 28. Suppose that paths π1 , π2 start from B1 and jectory, let locs(e) be the sequence of length k + 2 such
B2 respectively, reaching a shared endpoint R. Then IP (B1 )∩ that locs(e)[0] = sender(chan(e0 )) and, for all i such that
IP (B2 ) = ∅ unless B1 = B2 or: 1 ≤ i ≤ k + 1, locs(e)[i] = rcpt(chan(ei−1 )).
1. πi traverses a NAT device properly between Bi and R, Trajectory e = e0 , . . . ek  is B, E-worthy iff e is a success
where i = 1 or 2; or trajectory, locs(e)[0] = B, locs(e)[k + 1] = E, and, for every
2. R is a NAT device and π1 , π2 reach it on different i where 0 ≤ i ≤ k + 1,
interfaces. (msg(e0 ), msg(ei )) ∈ PrmtB,locs(e)[i] and
We now can define the equi-goal idea: (msg(ei ), msg(ek )) ∈ Prmtrlocs(e)[i],E .
Definition 29. A set G of goals has source equi-goals iff, for Packet msg(ei ) is worth keeping from B to E at R iff for
every NAT device d, if B1 , B2 lie on the inside of d and R lies some B, E-worthy trajectory e = e0 , . . . ek , R ∈ locs(e).
on the outside, then for all goals ψB @B1 → φ@R → ψE @E, Let KEEPB,E (R) be the set of packets worth keeping from
this goal is in G iff ψB @B2 → φ@R → ψE @E is in G. B to E at R. ///

G has destination equi-goals iff, for every NAT device d, if

In case there are no NATs, then KEEPB,E (R) receives the
E1 , E2 lie on the inside of d and R lies on the outside, then
same meaning as previously. By the definition:
for all goals ψB @B → φ@R → ψE @E1 , this goal is in G iff
ψB @B → φ@R → ψE @E2 is in G. Lemma 31. For all q, q ∈ KEEPB,E (R) iff there exist p1 , p2
G has equi-goals iff both conditions are met. /// such that (p1 , q) ∈ PrmtB,R and (q, p2 ) ∈ PrmtrR,E . ///

206
Combining the keep sets for different endpoints. The address. The translation for returning packets flowing inbound
equi-goal property and the IP disjointness assumption (As- on the edge is dual.
sumption 28) allow us to combine the keep sets for different Suppose now that F (e, d) expresses both the packet rewrit-
endpoints. ing and the filtering that occurs on edge e in direction d
(inbound vs. outbound). In particular, F (e, d) is a relation
Lemma 32. Suppose that the goals G have the equi-goal prop-
that holds on a pair of packets (p, q) when p is permitted
erty, and that B1 = B2 but KEEPB1 ,E (R) ∩ KEEPB2 ,E (R) =
to pass over e in direction d, but is rewritten by the sender
∅. Then
to q before transmission. If an entry reflects a filter retaining
1. There are success trajectories from B1 through R to E packets satisfying φ without rewriting, then its entry F (e, d)
or from B2 through R to E that traverse NATs between is the lifted relation ↑ φ, namely the identity relation restricted
Bi and R; and to φ. We now construct, for any pair of endpoints B, E:
2. If B1 , B2 have source equi-goals for R, E, then AF contains these relations AF i,j = F (e, d) in entries i, j,
KEEPB1 ,E (R) = KEEPB2 ,E (R). when edge e in direction d leads from i to j. If there is
Suppose that E1 = E2 but KEEPB,E1 (R) ∩ KEEPB,E2 (R) = no edge from i to j, then AFi,j =↑ ∅ is the empty relation.
∅. Then K is the diagonal matrix where Ki,j =↑ ∅ when i = j, and
1. There are success trajectories from B through R to E1
Ki,i =↑ {q : ∃pB , pE . PrmtB,i (pB , q)∧Prmtri,E (q, pE )}.
or from B through R to E2 that traverse NATs between
R and Ei ; and Thus, Ki,i contains the pairs (q, q) where q is permitted to
2. If E1 , E2 have destination equi-goals for B, R, then pass through i on a trajectory from B to E, for any forms of
KEEPB,E1 (R) = KEEPB,E2 (R). the packet at the endpoint.
We now use the same matrix operations to compute Rchm
Proof. By the non-emptiness condition, there is a B1 , E-
for the given F . Each Rchm will contain in position Rchm i,j
worthy e1 and a B2 , E-worthy e2 both traversing R and with
the relation which contains (qi , qj ) iff there is a path from
the same packet form p there. If e1 , e2 have not yet traversed
location i to j of length ≤ m such that qi is transformed to
a NAT, then p is in its original form; since these are success
qj along that path, and each intermediate qk (for i ≤ k ≤ j)
trajectories, this contradicts B1 = B2 . Thus claim 1 holds.
is permitted to pass through location k on a trajectory from
Since both trajectories provide p at R, the most recent NATs
B to E.
d1 , d2 that rewrote their source addresses both have sa(p) ∈
IP (di ). Hence by Assumption 28, d1 = d2 . Thus we may Rch0 = K, since paths of length 0 lead only from i to i, and
apply the definition of equi-goals; so the same conditions occur Ki,i reflects the packets permitted there.
in the goal statements for B1 , B2 , and the KEEP sets are the Rch1 = K + (K AF K). A path of length ≤ 1 is either empty
same. The claims for E1 , E2 are symmetric. or else it takes one step from i to an adjacent location j.
F determines whether a packet can traverse this edge and
That is, equi-goals on NATs ensure that KEEP sets are either how it is rewritten. The multiplication by K on the left
equal or disjoint. The information in the headers sa(p) and restricts the results to the packets that could permissibly
da(p) tells us enough to enforce the goals G tightly. As before, be present at i before traversing the edge, while the
we define, for a given set of goal statements G: multiplication by K on the right restricts them to packets
 permissibly at j after the step.
KEEP∗ () = KEEPB,E () (3) Rch(2m) = (Rchm Rchm ), since the paths of length ≤ 2m are
B,E
just the paths that divide into two paths of length ≤ m,
We would like now to filter packets as they are passing from respectively ending and beginning at the same node k.
one location to another location at which they should not be Rch = Rchb is the fixed point of Rchm .
kept, i.e., we should discard the complement of KEEP∗ ( ) When the only packet transformations are NATs, this recur-
along any edge a :  →  . We do this as before: sion will again reach its fixed point Rch after O(log2 |LO|)
matrix multiplications. Although non-simple paths can bring
Definition 33. The acceptance filter af maps arcs to sets of
transformed packets back to NATs they have already traversed,
packets, where af(a) = KEEP∗ ( ), for each arc a :  → 
NAT outputs are essentially idempotent: They simply select
from  to  . We write af(,  ) for af(a). ///
fixed addresses and (for source NATs) new undistinguished
We again want to configure our network to discard all ports. Thus, these packets will not lead to a larger set of
packets traversing the edge a that do not belong to the output, NAT-transformed results. Packet transformations could
acceptance filter af(a). be conceived that would converge to a fixed point only after
large numbers of multiplications, possibly of the order of the
Computing the matrices Rchm . We regard source NAT
number of distinct packets. However, non-simple paths do not
operations as occurring outbound on an edge e, and as defined
delay the fixed point for NATs.
by the relation Re (p, p ). Here, typically, this holds if p has
a local source address; p has the NAT device’s address as its Lemma 34. KEEP(i) = {q : ∃pb , pE . (pB , q) ∈ RchB,i ∧
source address; and p agrees with p for destination port and (q, pE ) ∈ Rchi,E }.

207
Security and Success Functionality. We justify security VII. C ONCLUSION
for this filtering posture much as before, but using the equi- This paper develops specifications for security goals gov-
goals properties. For given endpoints B, E, the matrix Rchm erning how packets traverse the network, and shows how to
summarizes what permissible trajectories of length ≤ m can distribute filtering functionality to different nodes. We have
deliver from B and to E. When we define KEEP∗ () as the proved that the resulting filtering implements the security
union of the sets KEEPB,E (), we rely on Lemma 32 to justify constraints while providing maximal service functionality. We
that this does not erase the differences between KEEP sets for have moreover implemented and validated our results using
the different endpoints. a tool that automatically localizes the filters and generates
As for its maximality, we observe as before that we filter configurations for all the firewalls in the network.
out only packets that have no permissible success trajectories. As a future work, from a theoretical point of view we plan
Firewall Configuration. As in the plain case, we define the to give an enforcement of the spoofing goals (that consider
firewall behaviour FW based on the KEEP∗ sets and the only trajectories with spoofing at creation), and promiscuous
c co 
function F (e, d). Consider the subgraph · →i  →  where  delivery goals (i.e., trajectories with promiscuous delivery).
 From a practical point of view we plan to extend Mignis to
and  may have NAT behavior defined by the function F used
to define AF . Then FW(t, ci , co , p) = localize filters also when NATs are present.
Acknowledgements This work was partially supported by
{qo ∈ KEEP∗ ( ) : ∃qi ∈ KEEP∗ () .
FCT projects Confident PTDC/EEI-CTP/4503/2014 and FCT
(p, qi ) ∈ F (ci , in) ∧
project UID/EEA/50008/2013.
(qi , qo ) ∈ F (co , out)}.
R EFERENCES
That is,  may queue qo for delivery over co if there is a qi into
which it can translate p along channel ci , and qi is a packet it [1] P. Adao, C. Bozzato, R. Focardi G. Dei Rossi, and F.L. Luccio. Mignis:
A semantic based tool for firewall configuration. In IEEE 27th Computer
can keep, and it can translate qi into qo outbound on co , and Security Foundations Symposium (CSF 2014), Vienna, Austria, pages
moreover  can keep qo . The router  must do filtering on 351–365. IEEE CS Press, July 2014.
both sides, because  may be a network region or end host, [2] E. Al-Shaer, A. El-Atawy, and T. Samak. Automated Pseudo-Live
Testing of Firewall Configuration Enforcement. IEEE Journal on
or a router without filtering functionality. selected areas in communication, 27(3):302–314, 2009.
As with Thm. 23 and 20: [3] C. J. Anderson, N. Foster, A. Guha, J.-B. Jeannin, D. Kozen,
C. Schlesinger, and D. Walker. NetKAT: Semantic foundations for
Theorem 35. Let G be a non-empty collection of success networks. In Proc. of the 41st ACM SIGPLAN-SIGACT Symposium
goals, and let the frame F obey FW and have every channel on Principles of Programming Languages (POPL 2014). ACM, 2014.
[4] Randal E. Bryant. Graph-based algorithms for boolean function manip-
connected to at least one router. F enforces G. If F  (with ulation. IEEE Trans. Comput., 35(8):677–691, August 1986.
the same graph and NAT behaviour) enforces G, then F is as [5] Frenetic, a family of network programming languages. [Link]
successful functionally as F  . ///
[Link]/, 2013.
[6] J.D. Guttman and A.L. Herzog. Rigorous automated network security
management. International Journal for Information Security, 5(1–2):29–
The complexity of generating filters using this method 48, 2005.
depends on several considerations. One is the complexity of [7] J.D Guttman and P.D. Rowe. A cut principle for information flow.
In IEEE 28th Computer Security Foundations Symposium (CSF 2015),
the underlying ring operations set intersection and relative Verona, Italy, pages 107–121. IEEE CS Press, July 2015.
product. Although these are potentially computationally hard, [8] Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and PB Godfrey.
they appear to be easy in practice. In particular, operations Veriflow: verifying network-wide invariants in real time. ACM SIG-
COMM Computer Communication Review, 42(4):467–472, 2012.
relevant to network filtering rarely mix many different bits. For [9] T. Nelson, C. Barratt, D.J. Dougherty, K. Fisler, and S. Krishnamurthi.
instance, the low order bit of a source address will probably The margrave tool for firewall analysis. In Proceedings of the 24th
never be combined with the third bit of a destination port. International Conference on Large Installation System Administration
(LISA’10), pages 1–8, Berkeley, CA, USA, 2010. USENIX Association.
The complexity also depends on the number of locations in [10] J. Walsh. Icsa labs firewall testing: An in depth analysis.
the network. While this would seem large, in fact, we do not [Link]
need to represent every network device as a separate location. %[Link], 2004.
[11] B. Zhang, E. Al-Shaer, R. Jagadeesan, J. Riely, and C. Pitcher. Speci-
Only the ones that are relevant to the security policy— fications of a high-level conflict-free firewall policy language for multi-
by requiring some distinctive protection—or to the security domain networks. In Proc. of ACM Symposium on Access Control
processing—by being a location at which we will filter or Models and Technologies (SACMAT 2007). ACM, 2007.
route—need to be represented. The remaining devices may be A PPENDIX
coalesced with their neighbors, and represented by a single
location. This abstraction leads to fairly small graphs. Table II reports the output of the localization tool that
If we regard a ring operation as a unit of computational automatically generated the Mignis+ configuration for the
effort, and let k be the number of locations in the abstracted four firewalls.
graph, then each matrix multiplication is below O(k 3 ), and
computing Rch requires log2 k multiplications. This must be
done k 2 times, performing the computations for KEEPB,E (·)
as B, E vary. Thus, the full computation is O(k 5 log k).

208
FIREWALL fw1

Sensitive@if_Sensitive : 22 > Trusted@if_fw2 | -m state --state ESTABLISHED,RELATED

Sensitive@if_Sensitive > Internet@if_fw2 : 443

Sensitive@if_Sensitive > Internet@if_fw3 : 443

Trusted@if_fw2 > Sensitive@if_Sensitive : 22

Internet@if_fw2 : 443 > Sensitive@if_Sensitive | -m state --state ESTABLISHED,RELATED

Untrusted@if_fw2 > Internet@if_fw3 : 80

Trusted@if_fw2 > Internet@if_fw3

Internet@if_fw3 : 443 > Sensitive@if_Sensitive | -m state --state ESTABLISHED,RELATED

Internet@if_fw3 : 80 > Untrusted@if_fw2 | -m state --state ESTABLISHED,RELATED

Internet@if_fw3 > Trusted@if_fw2 : 22
Internet@if_fw3 > Trusted@if_fw2 | -m state --state ESTABLISHED,RELATED

FIREWALL fw2

Trusted@if_Trusted > Sensitive@if_fw1 : 22

Trusted@if_Trusted > Internet@if_fw1

Trusted@if_Trusted > Internet@if_fw4

Untrusted@if_Untrusted > Internet@if_fw1 : 80

Sensitive@if_fw1 : 22 > Trusted@if_Trusted | -m state --state ESTABLISHED,RELATED

Internet@if_fw1 > Trusted@if_Trusted : 22
Internet@if_fw1 > Trusted@if_Trusted | -m state --state ESTABLISHED,RELATED

Internet@if_fw1 : 80 > Untrusted@if_Untrusted | -m state --state ESTABLISHED,RELATED

Sensitive@if_fw1 > Internet@if_fw4 : 443

Internet@if_fw4 > Trusted@if_Trusted : 22

Internet@if_fw4 > Trusted@if_Trusted | -m state --state ESTABLISHED,RELATED

Internet@if_fw4 : 443 > Sensitive@if_fw1 | -m state --state ESTABLISHED,RELATED

FIREWALL fw3

Internet@if_Internet : 443 > Sensitive@if_fw1 | -m state --state ESTABLISHED,RELATED

Internet@if_Internet : 80 > Untrusted@if_fw1 | -m state --state ESTABLISHED,RELATED
Internet@if_Internet > Trusted@if_fw1 : 22
Internet@if_Internet > Trusted@if_fw1 | -m state --state ESTABLISHED,RELATED

Sensitive@if_fw1 > Internet@if_Internet : 443

Untrusted@if_fw1 > Internet@if_Internet : 80
Trusted@if_fw1 > Internet@if_Internet

FIREWALL fw4

Internet@if_Internet : 443 > Sensitive@if_fw2 | -m state --state ESTABLISHED,RELATED

Internet@if_Internet > Trusted@if_fw2 : 22
Internet@if_Internet > Trusted@if_fw2 | -m state --state ESTABLISHED,RELATED

Sensitive@if_fw2 > Internet@if_Internet : 443

Trusted@if_fw2 > Internet@if_Internet

TABLE III
Mignis+ RULES AUTOMATICALLY GENERATED FOR THE FOUR FIREWALLS OF THE EXAMPLE NETWORK .

209