A Formal Model and Tool for Data Flow Security in Computer Networks


Computer networks operated by companies are often large and complex.
Changes in the configurations of firewalls or routers in one part of a
network can effect the entire network. Complex interdependencies can
make it difficult to keep an overview over the security of a network. An
important aspect of network security is the data flow. We propose a
formal model and a tool, implementing the model, to approach the
difficult problem of regulating data flow in computer networks.

The model includes a formal model of networks which focuses on network
areas and the connections between them, thereby abstracting from routers
and firewalls as devices. Data flow in the network is modeled by sets of
packets that may travel between network areas. The packet sets are
specified by configurations of the network’s routers and firewalls. In
our model iptables routers are used. Further we define flow policies
that enable to abstractly specify security constrains for a network.
Also a satisfaction relation is provided to check whether the data flow
in a network satisfies a policy or not.

The tool implementing the formal model checks the compliance of data
flow with a given policy. The network model and the flow policy are each
described in a domain specific language. Iptables configurations are
read directly from iptables output. Besides checking whether a policy is
satisfied it provides information about the packets and the paths of
policy violations.