README

ITVal is a tool for iptables configuration analysis.  It can be used to:

1.  Detect unprotected ports/hosts.
2.  Determine whether certain services are incorrectly 
	blocked by the firewall.
3.  Validate changes to the firewall policy.
4.  Generate an equivalence class abstraction of the firewall policy
that can be used to easily detect many different types of errors.

ITVal-1.2 replaces the antiquated build system based on autoconf with a
CMake-based system.  A recent (cmake-2.6 or greater) version of cmake is
now required to build ITVal.

ITVal implements a query engine based on a simple query language that a
system administrator can use to investigate firewall behaviors.

COMMAND LINE OPTIONS:

ITVal understands the following flags:

   -q <query file>	
        Full Path to a query file.
   
   -t <topology file>
        Full Path to a topology mapping 
        
        The topology mapping is optional.  It should be formatted as a
        list of network interface, IP address pairs.  For example:
	      eth0	   192.168.1.1
	      eth1	   70.5.123.110
	       
   -f <filter file>	
        Full Path to a filtering rule set file.  This file is the output
        of `iptables -L -n'.
        
   -n <NAT file>		
        Full Path to a NAT rule set file.  This file is the output of
        `iptables -t nat -L -n'.

   -F <verbose filter file >	
        Full Path to a filtering rule set file.  This file is the output
        of `iptables -v -L -n'.

   -N <verbose NAT file>		
        Full Path to a NAT rule set file.  This file is the output of
        `iptables -t nat -v -L -n'.

The output of the query engine can be modified and used as a query file.

CONSTRUCTING QUERIES AND ASSERTIONS:

An ITVal query file consists of a number of group and service definitions,
followed by any number of query and/or assertion statements.  Group and service
definitions can be mixed with queries and assertions in any order as long as
the definition of a group or service precedes every use.

*GROUP DEFINITIONS*

A group definition allows the user to name a list of IP addresses for
easier future reference.  The syntax is as follows:

GROUP <name> <list>;

The name must be unique and must be alphanumeric.  The list is a
space-separated sequence of IP addresses in dot notation.  It is
permissible to use the '*' character as a wildcard.

Example:

GROUP mail_clients 192.168.1.1 192.168.1.3 192.168.2.*;

*SERVICE DEFINITIONS*

A service definition is analogous to a group definition, but for various
network services, specified by port number.  The syntax is:

SERVICE <name> <list>;

Where name is unique and list is a space separated list of <protocol>
<port> pairs.  The '*' character may be used as a wildcard for the port
number and the protocol "BOTH" can be used to specify both TCP -AND- UDP
connections.

Example:

SERVICE mail TCP 25 TCP 110 TCP 993;

*QUERY STATEMENTS*

Queries have the syntax:

QUERY <subject> <condition>;

The "subject" parameter specifies what information ITVal should display
for packets that match the query condition.  The valid subjects are:

SADDY       Source Address
DADDY       Destination Address
SPORT       Source Port
DPORT       Destination Port
STATE       Connection State

The "condition" parameter specifies criteria against which all packets will be
considered.  All packets that match the conditions are displayed.  The query
condition is built from eleven primitives:

FROM <source>      Matches source address
TO <destination>   Matches destination address
ON <source>        Matches source port
FOR <destination>  Matches destination port
IN <state>         Matches connection state
WITH <flag>        Matches active TCP flag
INFACE <iface>     Matches incoming network interface
OUTFACE <iface>    Matches outgoing network interface
LOGGED             Matches if there is a rule that MAY log the packet.
ACCEPTED <chain>   Matches all packets accepted by built-in chain <chain>.
DROPPED	<chain>	   Matches all packets discarded by built-in chain <chain>.

These primitives can be combined with the logical operators "AND", "OR",
and "NOT".  Parentheses can be used to disambiguate expressions.
Otherwise, precedence is from left to right.

Examples:

QUERY SADDY FROM 192.168.1.1 AND FOR mail;
QUERY DPORT (NOT FROM mail_clients OR TO 192.168.1.4) AND NOT LOGGED;
QUERY DPORT NOT FROM 192.168.1.* AND INFACE eth0;

*ASSERTIONS*

The user can also provide ITVal with a set of assertions to verify.  ITVal will
check each assertion and determine whether it is true or false.  The syntax for assertion statements is as follows:

ASSERT <condition> <assertion_operator> <condition>;

Both conditions are defined as for QUERY statements (see above).  The assertion
operator can be either "IS" or "SUBSET OF".  The "IS" operator tests whether
the set of packets described by the left condition is precisely equivalent to
the set of packets described by the right condition.  The "SUBSET OF" operator
tests whether the set of packets described by the left condition is (not
strictly) contained in the set described by the right condition.

Examples:

//SSH packets, and only SSH packets, are accepted from subnet 192.168.1.0/24
ASSERT (ACCEPTED INPUT AND FROM 192.168.1.*) IS (FROM TCP 22);

//All hosts on 192.168.2.* can be reached by some packet
ASSERT TO 192.168.2.* SUBSET OF ACCEPTED FORWARD;

*CLASSES*

Network hosts can be grouped into classes based on which services the firewall
allows them to access and provide.  ITVal provides a special query (QUERY
CLASSES) that generates a list of which hosts belong to which group.  This list
can be used to easily detect certain kinds of anomalies in the firewall policy.
For instance, if your mail server shows up in the same group as an untrusted
host from outside your network, you probably have a typo or other error.  (For
more, see the proceedings of LISA '06).  Similarly, the set of all services can
be partioned into classes (based on which hosts can use those services), with
the "SCLASSES" query.

Examples:

QUERY CLASSES;
QUERY SCLASSES;