{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Analyzing ACLs and firewall rules with Batfish" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Network and security engineers are responsible for ensuring that the ACLs and firewall rules in their networks are permitting and denying traffic as intended. This task usually requires manual checking or loading rulesets onto a lab device in order to test behavior on example packets of interest. These methods are not only time consuming but also error-prone. \n", "\n", "Batfish makes it easy to deeply analyze ACLs and firewall rules, which we generally call *filters.* It can show what a filter will do with a given packet, right down to the line of the filter that matches the packet; it can provide guarantees on how a filter treats a large space of packets; and it can sanity check a filter to ensure that every line in it matches at least some packets.\n", "\n", "In this notebook, we demonstrate these capabilities. In our [\"Provably Safe ACL and Firewall Changes\" notebook](https://github.com/batfish/pybatfish/blob/master/jupyter_notebooks/Provably%20Safe%20ACL%20and%20Firewall%20Changes.ipynb), we show how Batfish can guarantee that filter changes are safe.\n", "\n", "Check out a video demo of this notebook [here](https://youtu.be/KixQYEDh33s)." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Initialization" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "We use an example network with two devices, a router with ACLs and a firewall. The device configurations can be seen [here](https://github.com/batfish/pybatfish/tree/master/jupyter_notebooks/networks/example-filters/current/configs). " ] }, { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "'current'" ] }, "execution_count": 1, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# Import packages\n", "%run startup.py\n", "bf = Session(host=\"localhost\")\n", "\n", "# Initialize a network and a snapshot\n", "bf.set_network(\"network-example-filters\")\n", "\n", "SNAPSHOT_NAME = \"current\"\n", "SNAPSHOT_PATH = \"networks/example-filters/current\"\n", "bf.init_snapshot(SNAPSHOT_PATH, name=SNAPSHOT_NAME, overwrite=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## `testFilters`: Testing how filters treat a flow" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The `testFilters` question shows what filters do with a particular flow and *why*. It takes as input the details of the flow and a set of filters to test. The answer provides a detailed view of how the flow is treated by each filter in the set.\n", "\n", "Flows are specified using source and destination IP addresses and, optionally, other fields such as IP protocols, ports, and TCP flags. You may also specify the ingress interface which is factored in when the behavior of a filter depends on it. See [documentation](https://pybatfish.readthedocs.io/en/latest/notebooks/filters.html#Test-Filters) for details. The question will fill in any unspecified fields with reasonable defaults.\n", "\n", "The set of filters to examine can be narrowed using various criteria, including regexes for node and filter names. Left unspecified, `testFilters` will give results for every filter in the network." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Example 1: Test if hosts in a subnet can reach the DNS server" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Suppose we wanted to test if our ACL **acl_in** in router **rtr-with-acl** allows hosts in a subnet to reach our DNS server. This check is easily expressed. If the subnet is 10.10.10.0/24 and the DNS server is at the IP address 218.8.104.58, then the query will be as shown below, where we have picked 10.10.10.1 as a representative source IP for the subnet." ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [ { "data": { "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 NodeFilter_NameFlowActionLine_ContentTrace
0rtr-with-aclacl_inStart Location: rtr-with-acl
Src IP: 10.10.10.1
Src Port: 49152
Dst IP: 218.8.104.58
Dst Port: 53
IP Protocol: UDP
PERMIT660 permit udp 10.10.10.0/24 218.8.104.58/32 eq domain
  • Matched line 660 permit udp 10.10.10.0/24 218.8.104.58/32 eq domain
\n" ], "text/plain": [ " Node Filter_Name \\\n", "0 rtr-with-acl acl_in \n", "\n", " Flow Action \\\n", "0 start=rtr-with-acl [10.10.10.1:49152->218.8.104.58:53 UDP] PERMIT \n", "\n", " Line_Content \\\n", "0 660 permit udp 10.10.10.0/24 218.8.104.58/32 eq domain \n", "\n", " Trace \n", "0 - Matched line 660 permit udp 10.10.10.0/24 218.8.104.58/32 eq domain " ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "# Check if a representative host can reach the DNS server\n", "dns_flow = HeaderConstraints(srcIps=\"10.10.10.1\",\n", " dstIps=\"218.8.104.58\",\n", " applications=[\"dns\"])\n", "answer = bf.q.testFilters(headers=dns_flow,\n", " nodes=\"rtr-with-acl\",\n", " filters=\"acl_in\").answer()\n", "show(answer.frame())" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The result above shows that the flow we tested is indeed permitted by the filter **acl_in** (in `Filter_Name` column) on device **rtr-with-acl** (in `Node` column). The `Flow` column shows the exact flow tested, including the default values chosen by Batfish for unspecified parameters. The remaining columns show how the flow is treated by the filter. The `Action` column shows the final outcome, `Line_Content` shows which line(s) led to that action, and `Trace` shows all the lines the packet matched. In this case, the trace is not deep, but it can be quite deep for filters that reference other structures such as policy maps and object groups." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Example 2: Test that HTTP flows cannot go from one zone to another" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Now suppose we want to test that our **firewall** blocks HTTP flows that cross the boundary from one zone to another. A query like the one below can help us do that. It is testing how output filters on interfaces in the second zone treat a packet with the specified header fields when it enters the firewall through interfaces in the first zone.\n", "\n", "The arguments to `startLocation` and `filters` below use Batfish specifiers that enable easy specification of various concepts. `enter(firewall[Ethernet0/0/2])` specifies that the packet we want to test enters 'firewall' via 'Ethernet0/0/2' (the interface in the first zone) and `outFilterOf(Ethernet0/0/3)` specifies that the filter we want to test is the out filter on 'Ethernet0/0/3' (the interface in the second zone)." ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "data": { "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 NodeFilter_NameFlowActionLine_ContentTrace
0firewall~ZONE_OUTGOING_ACL~zone-z3~Start Location: firewall interface=GigabitEthernet0/0/2
Src IP: 10.114.64.1
Src Port: 49152
Dst IP: 10.114.60.10
Dst Port: 80
IP Protocol: TCP (SYN)
DENYno-match
    \n" ], "text/plain": [ " Node Filter_Name \\\n", "0 firewall ~ZONE_OUTGOING_ACL~zone-z3~ \n", "\n", " Flow \\\n", "0 start=firewall interface=GigabitEthernet0/0/2 [10.114.64.1:49152->10.114.60.10:80 TCP (SYN)] \n", "\n", " Action Line_Content Trace \n", "0 DENY no-match " ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "# Test if a host can reach the DNS server\n", "http_flow = HeaderConstraints(srcIps=\"10.114.64.1\",\n", " dstIps=\"10.114.60.10\",\n", " applications=[\"http\"])\n", "answer = bf.q.testFilters(headers=http_flow,\n", " startLocation=\"@enter(firewall[GigabitEthernet0/0/2])\",\n", " filters=\"@out(GigabitEthernet0/0/3)\").answer()\n", "show(answer.frame())" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "As we can see the HTTP flow is indeed denied, and the columns in the table show the reason for that denial." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## `searchFilters`: Verifying how filters treat a (very large) space of flows" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "While `testFilters` reasons about individual flows, the `searchFilters` question provides comprehensive guarantees by reasoning about (potentially very large) spaces of flows. The space of flows is specified using source and destination prefixes (where the default prefix 0.0.0.0/0 denotes all 4,294,967,296 possibilities), a list of protocols, a range of ports, and so on. Given a flow space and a match condition, which can be 'permit', 'deny', or 'matchLine ', `searchFilters` returns flows within this space that match the condition. If no flow is returned, it is guaranteed that no flow in the entire space satisfies the condition. " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Example 1: Verify that *all* hosts in a subnet can reach the DNS server" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Earlier we checked that a subnet could reach the DNS server using `testFilters` with a representative source IP address. Now, let's use `searchfilter` to ascertain that the entire subnet can reach the server.\n", "\n", "The query below is asking if there is *any* flow from 10.10.10.0/24 to 218.8.104.58 that is *denied* by the filter **acl_in**. That is, we're asking for violations of the desired policy. An empty result means the policy is correctly implemented. Any flow returned by the query demonstrates that the policy is not correctly implemented." ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "data": { "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
     NodeFilter_NameFlowActionLine_ContentTrace
    0rtr-with-aclacl_inStart Location: rtr-with-acl
    Src IP: 10.10.10.42
    Src Port: 49152
    Dst IP: 218.8.104.58
    Dst Port: 53
    IP Protocol: UDP
    DENY460 deny udp 10.10.10.42/32 218.8.104.58/32 eq domain
    • Matched line 460 deny udp 10.10.10.42/32 218.8.104.58/32 eq domain
    \n" ], "text/plain": [ " Node Filter_Name \\\n", "0 rtr-with-acl acl_in \n", "\n", " Flow Action \\\n", "0 start=rtr-with-acl [10.10.10.42:49152->218.8.104.58:53 UDP] DENY \n", "\n", " Line_Content \\\n", "0 460 deny udp 10.10.10.42/32 218.8.104.58/32 eq domain \n", "\n", " Trace \n", "0 - Matched line 460 deny udp 10.10.10.42/32 218.8.104.58/32 eq domain " ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "# Check if the subnet can reach the DNS server\n", "dns_traffic = HeaderConstraints(srcIps=\"10.10.10.0/24\",\n", " dstIps=\"218.8.104.58\",\n", " applications=[\"dns\"])\n", "answer = bf.q.searchFilters(headers=dns_traffic,\n", " action=\"deny\",\n", " filters=\"acl_in\").answer()\n", "show(answer.frame())" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "As we can see, we did get a flow that matches the search condition and thus violates our desired guarantee of the entire subnet being able to reach the DNS server. The columns carry the same information as those for `testFilters` and provide insight into the violation. In particular, we see that a flow with source IP 10.10.10.42 is denied by an earlier line in the ACL. Such needles in the haystack are impossible to find with tools like pen testing. " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Example 2: Verify that the *only* TCP traffic that can go from one zone to another is NFS traffic " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "In the second example for `testFilters` we used an example flow to test if **firewall** denied HTTP flows from one zone to another. Now, suppose that we wanted a stricter condition—that only TCP-based NFS flows are allowed from one zone to another. With `searchFilters` we can verify this condition by searching for violations in the large space of non-NFS flows, as below." ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "text/html": [ "
    \n", "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
    NodeFilter_NameFlowActionLine_ContentTrace
    \n", "
    " ], "text/plain": [ "Empty DataFrame\n", "Columns: [Node, Filter_Name, Flow, Action, Line_Content, Trace]\n", "Index: []" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "# Check if any non-NFS, TCP flow can go from one zone to another\n", "non_nfs_tcp_traffic = HeaderConstraints(srcIps=\"101.164.101.231\",\n", " dstIps=\"101.164.9.0/24\",\n", " ipProtocols=[\"tcp\"],\n", " dstPorts=\"!2049\") # exclude NFS port (2049)\n", "answer = bf.q.searchFilters(headers=non_nfs_tcp_traffic,\n", " startLocation=\"@enter(firewall[GigabitEthernet0/0/2])\",\n", " filters=\"@out(GigabitEthernet0/0/3)\",\n", " action=\"permit\").answer()\n", "show(answer.frame())" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Since we got back an empty answer, we can be certain that no non-NFS flow can go from one zone to another. \n", "\n", "*Such strong guarantees are impossible with any other tool today.*" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## `filterLineReachability`: Analyzing reachability of filter lines " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "When debugging or editing filters, it can be useful to confirm that every line is reachable—that is, each line can match some packets that do not match earlier lines. Unreachable filter lines are often symptomatic of bugs and past edits that did not achieve policy intent. Even when they do not represent bugs, they represent opportunities to reduce the length of the filter. \n", "\n", "The `filterLineReachability` question identifies unreachable filter lines. Given no parameters, it will check every filter in the network, but its scope can be narrowed using `filters` and `nodes` parameters (see [documentation](https://pybatfish.readthedocs.io/en/latest/notebooks/filters.html#Filter-Line-Reachability))." ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [ { "data": { "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
     SourcesUnreachable_LineUnreachable_Line_ActionBlocking_LinesDifferent_ActionReasonAdditional_Info
    1rtr-with-acl: acl_in670 permit ip 166.146.58.184 anyPERMIT540 deny ip 166.144.0.0/12 anyTrueBLOCKING_LINESNone
    0rtr-with-acl: acl_in790 deny ip 54.203.159.1/32 anyDENY500 deny ip 54.0.0.0/8 anyFalseBLOCKING_LINESNone
    \n" ], "text/plain": [ " Sources Unreachable_Line \\\n", "1 ['rtr-with-acl: acl_in'] 670 permit ip 166.146.58.184 any \n", "0 ['rtr-with-acl: acl_in'] 790 deny ip 54.203.159.1/32 any \n", "\n", " Unreachable_Line_Action Blocking_Lines \\\n", "1 PERMIT ['540 deny ip 166.144.0.0/12 any'] \n", "0 DENY ['500 deny ip 54.0.0.0/8 any'] \n", "\n", " Different_Action Reason Additional_Info \n", "1 True BLOCKING_LINES None \n", "0 False BLOCKING_LINES None " ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "# Find unreachable lines in filters of rtr-with-acl\n", "aclAns = bf.q.filterLineReachability(nodes=\"rtr-with-acl\").answer()\n", "show(aclAns.frame().sort_values(by=\"Unreachable_Line\"))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Each line in the answer above identifies an unreachable line in a filter. Let's take a closer look at the first one. It shows that the line `670 permit ip 166.146.58.184 any` is unreachable because it is blocked by the line `540` shown in the `Blocking_Lines` column. The `Different_Action` column indicates that the blocking line `540` has the opposite action as the blocked line `670`, a more worrisome situation than if actions were the same.\n", "\n", "The `Reason` column shows that the line is unreachable because of it has other lines that block it, Lines can also be independently unreachable (i.e., no packet will ever match it) or may be unreachable because of circular references. The `filterLineReachability` question identifies such cases as well, and provides more information about them in the `Additional_Info` column." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Summary\n", "\n", "In this notebook, we showed how you can use Batfish to: \n", " 1. Test how filters in the network treat a flow (`testFilters`)\n", " 2. Verify how filters treat a large space of flows (`searchFilters`)\n", " 3. Find filter lines that will never match any packet (`filterLineReachability`)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "If you found these capabilities useful, check out our [\"Provably Safe ACL and Firewall Changes\" notebook](https://github.com/batfish/pybatfish/blob/master/jupyter_notebooks/Provably%20Safe%20ACL%20and%20Firewall%20Changes.ipynb) that shows how to change filters in a *provably* safe manner." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "***\n", "### Get involved with the Batfish community\n", "\n", "Join our community on [Slack](https://join.slack.com/t/batfish-org/shared_invite/enQtMzA0Nzg2OTAzNzQ1LTcyYzY3M2Q0NWUyYTRhYjdlM2IzYzRhZGU1NWFlNGU2MzlhNDY3OTJmMDIyMjQzYmRlNjhkMTRjNWIwNTUwNTQ) and [GitHub](https://github.com/batfish/batfish). " ] } ], "metadata": { "hide_input": false, "kernelspec": { "display_name": "Python 3", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.9.15" } }, "nbformat": 4, "nbformat_minor": 2 }