Skip to content

Commit

Permalink
Fixed remaining pages
Browse files Browse the repository at this point in the history
  • Loading branch information
craig-riecke committed Mar 2, 2016
1 parent 7181f7f commit 33535ea
Show file tree
Hide file tree
Showing 8 changed files with 226 additions and 141 deletions.
27 changes: 26 additions & 1 deletion Introduction/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,10 @@ following open source software packages applicable for your host computer:
- [Vagrant](http://www.vagrantup.com/downloads): automates the process of
creating, provisioning, starting and stopping VM's.

> The Windows version of Vagrant requires an SSH client to run. Installing
> [Git for Windows](https://git-scm.com/download/win) or
> [Cygwin](https://www.cygwin.com/) is the easiest way to get an SSH client.
The Frenetic Tutorial VM runs Ubuntu 14.04 as the guest OS. It has OCaml, OPAM, Mininet,
Wireshark, and Frenetic itself pre-installed. The standard VIM and Nano editor packages
are installed, but you can install your own through the normal Ubuntu package mechanisms.
Expand All @@ -70,7 +74,7 @@ OS host PC. Then:

The output will look something like this:

~~~ bash
~~~
$ mkdir frenetic-tutorial-vm
$ cd frenetic-tutorial-vm
~/frenetic-tutorial-vm$ vagrant init cr396/frenetic-tutorial
Expand All @@ -96,10 +100,31 @@ To use the VM:

- To start, change into the <code>frenetic-tutorial-vm</code> directory and type <code>vagrant up</code> followed
by <code>vagrant ssh</code>.

~~~
$ cd frenetic-tutorial-vm
~/frenetic-tutorial-vm$ vagrant up
Bringing machine 'default' up with 'virtualbox' provider...
... lots of text
~/frenetic-tutorial-vm$ vagrant ssh
Welcome to Ubuntu 14.04.2 LTS (GNU/Linux 3.16.0-30-generic x86_64)
* Documentation: https://help.ubuntu.com/
Last login: Sun Feb 28 11:57:22 2016 from 10.0.2.2
vagrant@frenetic:~$
~~~

- To stop, simply exit from the Frenetic VM command prompt. Back at your host command prompt, type <code>vagrant
halt</code>. This step is optional - if you forget and shut down your host machine, the Frenetic VM will
itself shut down cleanly beforehand. But halting it will save you some memory and CPU cycles on the host.

~~~
vagrant@frenetic:~$ exit
~/frenetic-tutorial-vm$ vagrant halt
~~~

References
----------

Expand Down
128 changes: 79 additions & 49 deletions NetKATFirewall/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,14 +3,16 @@ layout: main
title: Firewall with NetKAT
---

In an [earlier chapter](OxFirewall), we wrote a firewall that blocks
In an [earlier chapter](../OxFirewall), we wrote a firewall that blocks
ICMP traffic using OpenFlow and Ox. Even though this policy is
extremely simple, the implementation was somewhat involved, as we had
to both write a `packet_in` handler and also use `flow_mod` messages
to configure the switch.

## Exercise 1: Naive Firewall

**[Solution](https://github.com/frenetic-lang/tutorials/blob/master/netkat-tutorial-solutions/Firewall1.ml)**

We can implement the same policy in NetKAT as follows:

~~~ ocaml
Expand All @@ -21,13 +23,13 @@ open Repeater
let firewall : policy =
<:netkat<
if ipProto = 0x01 && ethType = 0x800 then drop else $pol
if ipProto = 0x01 and ethTyp = 0x800 then drop else $repeater
>>
let _ =
let module Controller = Frenetic_NetKAT_Controller.Make in
Controller.start 6633;
Controller.update_policy repeater;
Controller.update_policy firewall;
never_returns (Scheduler.go ());
~~~
Expand All @@ -42,17 +44,46 @@ we use a conditional to wrap the repeater policy from the last
chapter. The ability to combine policies in a compositional way is one
of the key benefits of NetKAT's language-based approach.

Type this policy into a file `Firewall.ml` in the
`netkat-tutorial-solutions` directory.
Type this policy into a file `Firewall1.ml` in the
`netkat-tutorial-solutions` directory.

Before testing, you'll need to prevent Repeater.ml from starting up its own
Frenetic controller and walking all over Firewall1's. So just edit Repeater.ml and
comment out the main loop:

~~~ ocaml
open Frenetic_NetKAT
open Core.Std
open Async.Std
(* a simple repeater *)
let repeater : policy =
<:netkat<
if port = 1 then port := 2 + port := 3 + port := 4
else if port = 2 then port := 1 + port := 3 + port := 4
else if port = 3 then port := 1 + port := 2 + port := 4
else if port = 4 then port := 1 + port := 2 + port := 3
else drop
>>
(* Comment out this part
let _ =
let module Controller = Frenetic_NetKAT_Controller.Make in
Controller.start 6633;
Controller.update_policy repeater;
never_returns (Scheduler.go ());
*)
~~~

#### Testing

To test your code, compile the firewall and start the controller in
one terminal,

~~~
$ ./netkat-build Firewall
$ ./Firewall.d.byte
$ ./netkat-build Repeater.d.byte
$ ./netkat-build Firewall1.d.byte
$ ./Firewall1.d.byte
~~~

and Mininet in another:
Expand All @@ -64,21 +95,25 @@ $ sudo mn --controller=remote --topo=single,4 --mac --arp
Using Mininet, check that pinging fails between all hosts:

~~~
mininet> h1 ping h2
mininet> h1 ping -c 1 h2
--- 10.0.0.2 ping statistics ---
2 packets transmitted, 0 received, 100% packet loss, time 1008ms
1 packet transmitted, 0 received, 100% packet loss, time 1008ms
~~~

~~~
mininet> h2 ping h1
mininet> h2 ping -c 1 h1
--- 10.0.0.1 ping statistics ---
2 packets transmitted, 0 received, 100% packet loss, time 999ms
1 packet transmitted, 0 received, 100% packet loss, time 999ms
~~~

## Exercise 2: Basic Firewall

**[Forwarding Solution](https://github.com/frenetic-lang/tutorials/blob/master/netkat-tutorial-solutions/Forwarding.ml)**
,
**[Firewall Solution](https://github.com/frenetic-lang/tutorials/blob/master/netkat-tutorial-solutions/Firewall2.ml)**

To gain further experience with NetKAT, let's implement a more
sophisticated firewall policy that uses point-to-forwarding rather
than naive flooding. As we saw in the last chapter, NetKAT supports
Expand All @@ -94,8 +129,6 @@ connected to ports 1 through 4 respetively.

~~~
open Frenetic_NetKAT
open Core.Std
open Async.Std
let forwarding : policy =
<:netkat<
Expand All @@ -119,7 +152,7 @@ open Forwarding
let firewall : policy =
<:netkat<
if (* FILL condition for ICMP packets *) then drop else (filter ethType = 0x800; $forwarding)
if (* FILL condition for ICMP packets *) then drop else (filter ethTyp = 0x800; $forwarding)
>>
let _ =
Expand All @@ -137,52 +170,48 @@ Save this policy into a file `Firewall2.ml` in the

- Build and launch the controller:

~~~ shell
$ ./netkat-build Firewall2
$ ./Firewall2.d.byte
~~~
~~~ shell
$ ./netkat-build Forwarding
$ ./netkat-build Firewall2
$ ./Firewall2.d.byte
~~~

- Start Mininet using the same parameters you've used before:

~~~
$ sudo mn --controller=remote --topo=single,4 --mac --arp
~~~
~~~
$ sudo mn --controller=remote --topo=single,4 --mac --arp
~~~

- Test that pings fail within Mininet:

~~~
mininet> h1 ping -c 1 h2
mininet> h2 ping -c 1 h1
~~~
These commands should fail, printing `100.0% packet loss`.
~~~
mininet> h1 ping -c 1 h2
mininet> h2 ping -c 1 h1
~~~
These commands should fail, printing `100.0% packet loss`.

- Although ICMP is blocked, other traffic, such as Web traffic should
be unaffected. To ensure that this is the case, try to run a Web server
on one host and a client on another.

* In Mininet, start new terminals for `h1` and `h2`:
* On `h1`, and start a web server.

~~~
mininet> xterm h1 h2
~~~

* In the terminal for `h1` start a local "fortune server" (a server
that returns insightful fortunes to those who query it):

~~~
# while true; do fortune | nc -l 80; done
~~~
~~~
mininet> h1 python -m SimpleHTTPServer 80 &
~~~

* In the terminal for `h2` fetch a fortune from `h1`:
* In the terminal for `h2` grab the default web page from `h1`:

~~~
# curl 10.0.0.1:80
~~~
~~~
mininet> h2 curl 10.0.0.1:80
~~~

This command should succeed.
This command should succeed.

## Exercise 3: Advanced Firewall

**[Solution](https://github.com/frenetic-lang/tutorials/blob/master/netkat-tutorial-solutions/Firewall3.ml)**

Now that basic connectivity works, let's extend the example further to
enforce a more interesting access control policy:

Expand Down Expand Up @@ -211,8 +240,8 @@ open Forwarding
let firewall : policy =
<:netkat<
if (ip4Src = 10.0.0.1 && ip4Dst = 10.0.0.2 && tcpSrcPort = 80 ||
ip4Src = 10.0.0.2 && ip4Dst = 10.0.0.1 && tcpDstPort = 80)
if (ip4Src = 10.0.0.1 and ip4Dst = 10.0.0.2 and ipProto = 6 and tcpSrcPort = 80 or
ip4Src = 10.0.0.2 and ip4Dst = 10.0.0.1 and ipProto = 6 and tcpDstPort = 80)
then $forwarding
else drop
~~~
Expand All @@ -224,11 +253,10 @@ Type this policy into a file `Firewall3.ml` in the
`netkat-tutorial-solutions` directory and test it in Mininet. Note
that due to the access control policy, it probably makes sense to test
a few points of the access control policy. For example, if you run
_fortune_ on port 80 on `h1`,
the web server on port 80 on `h1`,

~~~
## Run on h1's terminal
$ while true; do fortune | nc -l 80; done
mininet> h1 python -m SimpleHTTPServer 80 &
~~~

the command `curl 10.0.0.1:80` should succeed from `h2`, but fail from
Expand All @@ -237,9 +265,11 @@ the command `curl 10.0.0.1:80` should succeed from `h2`, but fail from

## Exercise 4: Compact Firewall

**[Solution](https://github.com/frenetic-lang/tutorials/blob/master/netkat-tutorial-solutions/Firewall4.ml)**

Above, we expressed the firewall policy is to enumerate each allowed
flow using conditionals. However, using NetKAT's predicates (`p1 &&
p2`, `p1 || p2`, and `!p`) is is often possible to write a more
flow using conditionals. However, using NetKAT's predicates (`p1 and
p2`, `p1 or p2`, and `not p`) is is often possible to write a more
compact and legible policy. Revise your advanced firewall this policy,
putting the result in a file `Firewall4.ml` in the
`netkat-tutorial-solutions` directory and test it in Mininet.
Expand Down
28 changes: 20 additions & 8 deletions NetKATRepeater/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ $ cd netkat-tutorial-solutions

### Example 1: A Repeater (Redux)

**[Solution](https://github.com/frenetic-lang/tutorials/blob/master/netkat-tutorial-solutions/Repeater.ml)**

In the [OxRepeater](../OxRepeater) chapter, we wrote an efficient
repeater that installs forwarding rules in the switch flow table.
Recall that a repeater simply outputs packets out all ports, except
Expand Down Expand Up @@ -71,12 +73,12 @@ the switch with a static NetKAT policy.
#### Run the Example

To run the repeater, type the code above into a file
<code>Repeater.ml</code> within the
<code>Repeater1.ml</code> within the
<code>netkat-tutorial-solutions</code> directory. Then compile and
start the repeater controller using the following commands.

~~~
$ ./netkat-build Repeater
$ ./netkat-build Repeater.d.byte
$ ./Repeater.d.byte
~~~

Expand Down Expand Up @@ -110,6 +112,8 @@ Try pinging <code>h1</code> from <code>h2</code> as well.

### Example 2: Referring to OCaml variables

**[Solution](https://github.com/frenetic-lang/tutorials/blob/master/netkat-tutorial-solutions/Repeater2.ml)**

In many programs it is useful to refer to an OCaml variable. We can do
this by writing `$x`, where `x` is the name of an OCaml variable. As
an example, here is an equivalent, but more concise version of the
Expand All @@ -124,16 +128,24 @@ open Core.Std
open Async.Std
(* a simple repeater *)
let all_ports : int list = [1; 2; 3; 4]
let all_ports : int32 list = [1l; 2l; 3l; 4l]
let flood (n : int) : policy =
let flood (n : int32) : policy =
List.fold_left
(fun pol m -> if n = m then pol else <:netkat<$pol + port := $m>>)
<:netkat<drop>> all_ports
all_ports
~f: (fun pol m -> if n = m then pol else <:netkat<$pol + port := $m>>)
~init: <:netkat<drop>>
let repeater : policy =
List.fold_right
(fun m pol -> <:netkat<let p = flood m in if port = $m then $p else $pol>>)
all_ports <:netkat<drop>>
all_ports
~f: (fun m pol -> let p = flood m in <:netkat<if port = $m then $p else $pol>>)
~init: <:netkat<drop>>
let _ =
let module Controller = Frenetic_NetKAT_Controller.Make in
Controller.start 6633;
Controller.update_policy repeater;
never_returns (Scheduler.go ());
~~~
Loading

0 comments on commit 33535ea

Please sign in to comment.