Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: batfish/batfish
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: master
Choose a base ref
...
head repository: netarch/batfish
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: master
Choose a head ref
Can’t automatically merge. Don’t worry, you can still create the pull request.

Commits on Dec 31, 2018

  1. Copy the full SHA
    018405d View commit details

Commits on Jan 1, 2019

  1. Update README

    kyechou committed Jan 1, 2019
    Copy the full SHA
    06d4666 View commit details
  2. Update .gitignore

    kyechou committed Jan 1, 2019
    Copy the full SHA
    e8be998 View commit details
  3. Copy the full SHA
    d6a0841 View commit details
  4. Add simple test case

    kyechou committed Jan 1, 2019
    Copy the full SHA
    9892e1f View commit details
  5. Add the execution script

    kyechou committed Jan 1, 2019
    Copy the full SHA
    40094c7 View commit details
  6. Copy the full SHA
    754edd4 View commit details
  7. Copy the full SHA
    6e66a98 View commit details
  8. Copy the full SHA
    fa8ce50 View commit details
  9. Copy the full SHA
    3d3303f View commit details
  10. Copy the full SHA
    44b439f View commit details
  11. Copy the full SHA
    64c26a8 View commit details
  12. Renaming logs

    kyechou committed Jan 1, 2019
    Copy the full SHA
    999e6b1 View commit details
  13. Copy the full SHA
    1573659 View commit details
  14. Copy the full SHA
    930eb1c View commit details
  15. Copy the full SHA
    77cf0da View commit details
  16. Copy the full SHA
    4b71de7 View commit details
  17. Add fat tree configs

    kyechou committed Jan 1, 2019
    Copy the full SHA
    71c9c29 View commit details
  18. Add fat-tree experiment logs

    kyechou committed Jan 1, 2019
    Copy the full SHA
    8be26f6 View commit details
  19. Copy the full SHA
    a287f2e View commit details
  20. Copy the full SHA
    94adb47 View commit details
  21. Copy the full SHA
    02e2c89 View commit details
  22. Add the compile script

    kyechou committed Jan 1, 2019
    Copy the full SHA
    3c125e7 View commit details
  23. Copy the full SHA
    164fd2b View commit details
  24. Copy the full SHA
    0afffb2 View commit details
  25. Copy the full SHA
    a5896f3 View commit details
  26. Copy the full SHA
    e1be6fa View commit details

Commits on Jan 7, 2019

  1. Copy the full SHA
    05a6b8b View commit details
  2. Change output file location

    kyechou committed Jan 7, 2019
    Copy the full SHA
    c557c24 View commit details

Commits on Jan 8, 2019

  1. Copy the full SHA
    e38cb3c View commit details
  2. Copy the full SHA
    7e5c500 View commit details
  3. Copy the full SHA
    ceda5b2 View commit details
  4. Remove simple-ibgp-test

    kyechou committed Jan 8, 2019
    Copy the full SHA
    b1f287f View commit details
  5. Sort out the scripts

    kyechou committed Jan 8, 2019
    Copy the full SHA
    6910a83 View commit details
  6. Copy the full SHA
    7319770 View commit details
  7. Fix minor bugs

    kyechou committed Jan 8, 2019
    Copy the full SHA
    59758f2 View commit details
  8. Copy the full SHA
    34c4771 View commit details
  9. Rename log files

    kyechou committed Jan 8, 2019
    Copy the full SHA
    4b7017c View commit details

Commits on Jan 14, 2019

  1. Copy the full SHA
    f4fbca3 View commit details
  2. Copy the full SHA
    8600fc6 View commit details
  3. Copy the full SHA
    89e3741 View commit details

Commits on Jan 15, 2019

  1. Copy the full SHA
    8a63294 View commit details
  2. Copy the full SHA
    7ba99e3 View commit details

Commits on Jan 16, 2019

  1. Copy the full SHA
    a5b5a88 View commit details

Commits on Feb 19, 2019

  1. Copy the full SHA
    9af59d7 View commit details
  2. Copy the full SHA
    ddb623f View commit details
  3. Add support for running bounded path policy in minesweeper

    Santhosh authored and Santhosh committed Feb 19, 2019
    Copy the full SHA
    13f9702 View commit details

Commits on Feb 20, 2019

  1. Minor fixes

    Santhosh authored and Santhosh committed Feb 20, 2019
    Copy the full SHA
    fcd9974 View commit details
  2. Fix bounded length parameters

    Santhosh authored and Santhosh committed Feb 20, 2019
    Copy the full SHA
    22b8944 View commit details

Commits on Mar 18, 2019

  1. Copy the full SHA
    c51b779 View commit details
7 changes: 6 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
/containers
containers
/client
/testrigs
.DS_Store
@@ -42,3 +42,8 @@ coverage*
# Ignore python cache files
__pycache__
.pytest_cache/

# Ignore ctags generated tags
tags

*.tar.zst
144 changes: 4 additions & 140 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,143 +1,7 @@
## Batfish Experiment Repository

**Got questions, feedback, or feature requests? Join our community on [Slack!](https://join.slack.com/t/batfish-org/shared_invite/enQtMzA0Nzg2OTAzNzQ1LTUxOTJlY2YyNTVlNGQ3MTJkOTIwZTU2YjY3YzRjZWFiYzE4ODE5ODZiNjA4NGI5NTJhZmU2ZTllOTMwZDhjMzA)**
This is a fork based on the release 0.36.1 of [Batfish](https://github.com/batfish/batfish) for experiments related to [Plankton](https://github.com/netarch/plankton).

[![codecov](https://codecov.io/gh/batfish/batfish/branch/master/graph/badge.svg)](https://codecov.io/gh/batfish/batfish)
The experiments are run on Dell Precision Tower 5810, with Xeon(R) CPU E5-2697 v3, 188 GB RAM, and Ubuntu 16.04.5.

## What is Batfish?

Batfish is a network validation tool that provides correctness guarantees for security, reliability, and compliance by analyzing the configuration of network devices. It builds complete models of network behavior from device configurations and finds violations of network policies (built-in, user-defined, and best-practices).

A primary use case for Batfish is to validate configuration changes *before* deployment (though it can be used to validate deployed configurations as well). Pre-deployment validation is a critical gap in existing network automation workflows. By Batfish in automation workflows, network engineers can close this gap and ensure that only correct changes are deployed.

**Batfish does NOT require direct access to network devices.** The core analysis requires only the configuration of network devices. This analysis may be enhanced using additional information from the network such as:
* BGP routes received from external peers
* Topology information represented by LLDP/CDP

See [www.batfish.org](http://www.batfish.org) for technical information on how it works. ![Analytics](https://ga-beacon.appspot.com/UA-100596389-3/open-source/batfish?pixel&useReferer)

## What kinds of correctness checks does Batfish support?

[![Getting to know Batfish](batfish_video.png)](https://www.youtube.com/channel/UCA-OUW_3IOt9U_s60KvmJYA/videos)

The [Batfish YouTube channel](https://www.youtube.com/channel/UCA-OUW_3IOt9U_s60KvmJYA/videos) (which you can subscribe to for new content) illustrates many types of checks. These checks span a range of network behaviors and device configuration attributes.
#### Configuration Compliance
* Flag undefined-but-referenced or defined-but-unreferenced structures (e.g., ACLs, route maps)
* Configuration settings for MTUs, AAA, NTP, logging, etc. match templates
* Devices can only be accessed using SSHv2 and password is not null
#### Reliability
* End-to-end reachability is not impacted for any flow after any single-link or single-device failure
* Certain services (e.g., DNS) are globally reachable
#### Security
* Sensitive services can be reached only from specific subnets or devices
* Paths between endpoints are as expected (e.g., traverse a firewall, have at least 2 way ECMP, etc...)
#### Change Analysis
* End-to-end reachability is identical across the current and a planned configuration
* Planned ACL or firewall changes are provably correct and causes no collateral damage for other traffic
* Two configurations, potentially from different vendors, are functionally equivalent



## How do I get started?

Getting started with Batfish is easy, just grab the latest `allinone` Batfish Docker container:

`docker pull batfish/allinone`

The container has:
* Batfish server
* Jupyter notebook [server](http://jupyter.org/)
* Example [Jupyter notebooks](https://github.com/batfish/pybatfish/tree/master/jupyter_notebooks)

Once you have installed the container, the first thing we recommend is walking through the Jupyter notebooks. Each notebook highlights different capabilities of Batfish and shows you how to exercise it. Check-out this [README](https://github.com/batfish/pybatfish/tree/master/jupyter_notebooks) for the detailed list of notebooks.

### Running the example notebooks

To run through the example Jupyter notebooks, start the docker container:

`docker run -p 8888:8888 batfish/allinone`

When this container starts, Jupyter will show a token required for access (e.g. **token=abcdef123456...**). Make note of this, as you will need it to access the Jupyter server.

Now just open your web-browser and navigate to [http://localhost:8888](http://localhost:8888) enter the token in the Password or token: prompt to access the notebooks.


## Evaluate your own network configurations

Now that you are familiar with the capabilities of Batfish, you are ready to analyze your network configurations. The first thing to do is create a local data directory. This is a folder on the host machine running the docker container, where Batfish will persist data across container reboots.

`mkdir -p data`

Stop and restart the container.

`docker stop $(docker ps -f "ancestor=batfish/allinone" -q)`

`docker run -v $(pwd)/data:/data -p 9997:9997 -p 9996:9996 batfish/allinone`


This starts the service after mapping the local data folder to the data folder within the container and exposing the TCP ports required by the Batfish service.

Next, you need to install [Pybatfish](https://www.github.com/batfish/pybatfish) (the Python SDK) in order to interact with the service.

## Download and install Pybatfish
First, clone the Github repository. Change to the directory where you would like to clone the repository and issue the git command below.

`cd /path/to/directory/where/you/want/to/clone/repo`

`git clone git@github.com:batfish/pybatfish.git`

Then, install Pybatfish. We highly recommend that you install Pybatfish in a Python 3 virtual environment. Details on how to set one up can be found [here](https://docs.python.org/3/library/venv.html).

Once your virtual environment is setup and activated, issue the following commands

`cd /path/to/directory/where/you/want/to/clone/repo/pybatfish`

`pip install -e .`

Now, you are ready to evaluate your own network with Batfish.We encourage you to use Jupyter notebooks as your starting point, but you can use other methods that you are a comfortable with, e.g., an IDE like PyCharm or an interactive Python shell.
If you choose to use Jupyter notebooks as your starting point, you need to install Jupyter in your virtual environment. Jupyter documentation can be found [here](http://jupyter.org/install) - but the commands below will get you going.

`pip install --upgrade pip`

`pip install jupyter`

`jupyter notebook`

Our notebooks provide a quick start guide for different use cases. Beyond that, the complete documentation is available on [readthedocs](https://pybatfish.readthedocs.io/en/latest/quickstart.html).


## System Requirements for running Batfish

Batfish can be run on any operating system that supports Docker. The containers are actively tested on Mac OS X and Ubuntu 16.04 LTS.

To get started with the example Jupyter notebooks, all you need is a reasonably capable laptop:

* Dual core CPU
* 8 GB RAM
* 256 GB hard-drive

When you transition to running Batfish on your own network, we recommend a server that at least has:

* Quad-core CPU with 2 threads per CPU
* 32 GB RAM
* 256 GB hard-drive


## Supported Network Device and Operating System List

Batfish supports configurations for a large and growing set of (physical and virtual) devices, including:

* Arista
* Aruba
* AWS (VPCs, Network ACLs, VPN GW, NAT GW, Internet GW, Security Groups, etc…)
* Cisco (All Cisco NX-OS, IOS, IOS-XE, IOS-XR and ASA devices)
* Dell Force10
* Foundry
* iptables (on hosts)
* Juniper (All JunOS platforms: MX, EX, QFX, SRX, T-series, PTX)
* MRV
* Palo Alto Networks
* Quagga / FRR
* Quanta
* VyOS

If you'd like support for additional vendors or currently-unsupported configuration features, let us know via [Slack](https://join.slack.com/t/batfish-org/shared_invite/enQtMzA0Nzg2OTAzNzQ1LTUxOTJlY2YyNTVlNGQ3MTJkOTIwZTU2YjY3YzRjZWFiYzE4ODE5ODZiNjA4NGI5NTJhZmU2ZTllOTMwZDhjMzA)or [GitHub](https://github.com/batfish/batfish/issues/new). We'll try to add support. Or, you can -- we welcome pull requests! :)
All the experiment scripts and data are located in `experiments/`.
2 changes: 1 addition & 1 deletion projects/allinone/allinone
Original file line number Diff line number Diff line change
@@ -9,7 +9,7 @@ if batfish_cygwin; then
stty -icanon min 1 -echo
CPSEP=";"
fi
java ${ALLINONE_JAVA_ARGS} -cp "${ALLINONE_JAR}${CPSEP}${ALLINONE_CLASSPATH}" org.batfish.allinone.Main "$@"
/usr/bin/time timeout --foreground --preserve-status --kill-after=3m 4h java $ALLINONE_JAVA_ARGS -XX:MaxPermSize=2048m -Xmx150g -cp "${ALLINONE_JAR}${CPSEP}${ALLINONE_CLASSPATH}" org.batfish.allinone.Main "$@"
EXIT_CODE=$?
if batfish_cygwin; then
stty icanon echo
2 changes: 1 addition & 1 deletion projects/batfish/src/main/java/org/batfish/symbolic/Graph.java
100644 → 100755
Original file line number Diff line number Diff line change
@@ -281,7 +281,7 @@ public static Set<Prefix> getOriginatedNetworks(Configuration conf, Protocol pro
for (OspfArea area : ospf.getAreas().values()) {
for (String ifaceName : area.getInterfaces()) {
Interface iface = conf.getAllInterfaces().get(ifaceName);
if (iface.getActive() && iface.getOspfEnabled()) {
if (iface != null && iface.getActive() && iface.getOspfEnabled()) {
acc.add(iface.getAddress().getPrefix());
}
}
Original file line number Diff line number Diff line change
@@ -267,7 +267,8 @@ private Map<String, Configuration> applyFilters(

public Map<String, Configuration> compress(HeaderSpace h) {
DestinationClasses dcs = DestinationClasses.create(_batfish, _graph, h, true);
List<Supplier<NetworkSlice>> ecs = NetworkSlice.allSlices(_bddPacket, dcs, 0);
String testrigName = _batfish.getEnvironment().getTestrigName();
List<Supplier<NetworkSlice>> ecs = NetworkSlice.allSlices(_bddPacket, dcs, 0, testrigName);
Optional<Map<GraphEdge, EquivalenceClassFilter>> opt =
ecs.stream().map(Supplier::get).map(this::processSlice).reduce(this::mergeFilters);
if (!opt.isPresent()) {
Original file line number Diff line number Diff line change
@@ -1,17 +1,26 @@
package org.batfish.symbolic.abstraction;

import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.PrintWriter;
import java.io.File;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.function.Supplier;
import java.util.Collections;
import javax.annotation.Nullable;
import org.batfish.common.bdd.BDDPacket;
import org.batfish.datamodel.Configuration;
import org.batfish.datamodel.HeaderSpace;
import org.batfish.datamodel.Prefix;
import org.batfish.symbolic.Graph;
import org.batfish.symbolic.GraphEdge;
import org.batfish.symbolic.bdd.BDDNetwork;
import org.batfish.symbolic.utils.Tuple;
import com.fasterxml.jackson.databind.ObjectMapper;

public class NetworkSlice {

@@ -34,7 +43,7 @@ public NetworkSlice(
}

public static List<Supplier<NetworkSlice>> allSlices(
BDDPacket packet, DestinationClasses dcs, int fails) {
BDDPacket packet, DestinationClasses dcs, int fails, String testrigName) {
BDDNetwork network = BDDNetwork.create(packet, dcs.getGraph());
ArrayList<Supplier<NetworkSlice>> classes = new ArrayList<>();
for (Entry<Set<String>, Tuple<HeaderSpace, Tuple<List<Prefix>, Boolean>>> entry :
@@ -47,8 +56,55 @@ public static List<Supplier<NetworkSlice>> allSlices(
() ->
AbstractionBuilder.createGraph(
dcs, network, devices, headerspace, prefixes, fails, isDefaultCase);

/* Output the topology */
Graph g = sup.get()._abstraction.getGraph();
List<String> sorted_devices = new ArrayList<String>(devices);
Collections.sort(sorted_devices);
File file = new File(testrigName + "/bonsai/topo/" + String.join(".", sorted_devices) + ".log");
try {
file.getParentFile().mkdirs();
file.createNewFile();
} catch (IOException e) {
e.printStackTrace();
}
try {
PrintWriter writer = new PrintWriter(file);
Map<String, List<GraphEdge>> em = g.getEdgeMap();
em.forEach(
(router, graphEdges) -> {
graphEdges.forEach(
edge -> {
writer.println(router + " " + edge.getPeer());
});
});
writer.close();
} catch (IOException e) {
e.printStackTrace();
}

/* Output the Node Configuration */
ObjectMapper objectMapper = new ObjectMapper();
Map<String, Configuration> conf = g.getConfigurations();
conf.forEach(
(node, nodeconf) -> {
File file2 = new File(testrigName + "/bonsai/config/" + node + ".json");
try {
file2.getParentFile().mkdirs();
file2.createNewFile();
} catch (IOException e) {
e.printStackTrace();
}
try {
objectMapper.writeValue(file2, nodeconf);
} catch (IOException e) {
e.printStackTrace();
}
});
classes.add(sup);
}
// Uncomment this to only generate the bonsai topologies and configurations
//System.exit(0)
return classes;
}

Original file line number Diff line number Diff line change
@@ -259,7 +259,8 @@ private void addEnvironmentConstraints(Encoder enc, EnvironmentType t) {
}

private Tuple<Stream<Supplier<NetworkSlice>>, Long> findAllNetworkSlices(
HeaderQuestion q, @Nullable Graph graph, boolean useDefaultCase) {
HeaderQuestion q, @Nullable Graph graph, boolean useDefaultCase,
String testrigName) {
if (q.getUseAbstraction()) {
HeaderSpace h = q.getHeaderSpace();
int numFailures = q.getFailures();
@@ -270,7 +271,7 @@ private Tuple<Stream<Supplier<NetworkSlice>>, Long> findAllNetworkSlices(
System.out.println("Created destination classes");
System.out.println("Num Classes: " + dcs.getHeaderspaceMap().size());
long l = System.currentTimeMillis();
List<Supplier<NetworkSlice>> ecs = NetworkSlice.allSlices(_bddPacket, dcs, numFailures);
List<Supplier<NetworkSlice>> ecs = NetworkSlice.allSlices(_bddPacket, dcs, numFailures, testrigName);
l = System.currentTimeMillis() - l;
System.out.println("Created BDDs");
return new Tuple<>(ecs.parallelStream(), l);
@@ -310,7 +311,8 @@ public AnswerElement checkForwarding(HeaderQuestion question) {
long totalTime = System.currentTimeMillis();
HeaderQuestion q = new HeaderQuestion(question);
q.setFailures(0);
Tuple<Stream<Supplier<NetworkSlice>>, Long> ecs = findAllNetworkSlices(q, null, true);
String testrigName = _batfish.getEnvironment().getTestrigName();
Tuple<Stream<Supplier<NetworkSlice>>, Long> ecs = findAllNetworkSlices(q, null, true, testrigName);
Stream<Supplier<NetworkSlice>> stream = ecs.getFirst();
Long timeAbstraction = ecs.getSecond();
Optional<Supplier<NetworkSlice>> opt = stream.findFirst();
@@ -371,6 +373,8 @@ private AnswerElement checkProperty(
}
if (sourceRouters.isEmpty()) {
throw new BatfishException("Set of valid ingress nodes is empty");
} else {
System.out.println("=====[DEBUG]===== sourceRouters: " + sourceRouters);
}

// copy before updating header space, so these changes don't get propagated to the answer
@@ -380,7 +384,8 @@ private AnswerElement checkProperty(

Set<GraphEdge> failOptions = failLinkSet(graph, q);
Set<String> failNodeOptions = failNodeSet(graph, q);
Tuple<Stream<Supplier<NetworkSlice>>, Long> ecs = findAllNetworkSlices(q, graph, true);
String testrigName = _batfish.getEnvironment().getTestrigName();
Tuple<Stream<Supplier<NetworkSlice>>, Long> ecs = findAllNetworkSlices(q, graph, true, testrigName);
Stream<Supplier<NetworkSlice>> stream = ecs.getFirst();
Long timeAbstraction = ecs.getSecond();

@@ -404,6 +409,29 @@ private AnswerElement checkProperty(
// Get the EC graph and mapping
Graph g = slice.getGraph();
Set<String> srcRouters = mapConcreteToAbstract(slice, sourceRouters);
System.out.println("=====[DEBUG]===== mapped srcRouters: " + srcRouters);

// File file = new File("srcRouters");
// try {
// file.createNewFile();
// } catch (IOException e) {
// e.printStackTrace();
// }
// try {
// PrintWriter writer = new PrintWriter(file);
// Map<String, List<GraphEdge>> em = g.getEdgeMap();
// em.forEach(
// (router, graphEdges) -> {
// graphEdges.forEach(
// edge -> {
// writer.println(router + " " + edge.getPeer());
// });
// });
// writer.close();
// } catch (IOException e) {
// e.printStackTrace();
// }


long timeEncoding = System.currentTimeMillis();
Encoder enc = new Encoder(_settings, g, question);
@@ -532,6 +560,7 @@ private AnswerElement checkProperty(
});

totalTime = (System.currentTimeMillis() - totalTime);
System.out.println("Plankton time measurement: " + totalTime);
VerificationResult res;
AnswerElement ae;
if (hasCounterExample) {