Homework 2

Changelog

  • v1: September 24, 2019

Overview

In this assignment, you will solve several pencil-and-paper problems.

Due Date

  • 11:59pm, October 3, 2019

Academic Integrity

This assignment must be completed individually. All work you submit must be your own and sharing or receiving code is forbidden, with the exception of your partner. Do not look for or submit code you find on the Internet, and do not post solutions or partial solutions on the discussion site. If you make use of any outside materials, you must give attribution. You may ask general questions about NetKAT, etc. and you may discuss high-level details of the exercises with your classmates. If you have any questions about what is allowed and what is not allowed, please ask the instructor first!

Exercise 1: NetKAT Syntactic Sugar

As we saw in lecture, NetKAT is a minimal calculus organized around a small set of orthogonal programming constructs.

p ::= ....
    | id
    | drop
    | f = n
    | !p
    | p1 + p2
    | p1 ; p2
    | p*
    | f := n
    | dup

However, it is possible to enrich the language with additional constructs that are desugared into the core language. For example, we can define a larger language, with standard conditionals and loops:

P ::= 
  | ... 
  | if P1 then P2 else P3
  | while P1 do P2

It is easy to translate programs in this larger language into NetKAT:

T(while p1 do p2) =def= (T(p1); T(p2))*; T(!p1)
T(if p1 then p2 else p3) =def= (T(p1); T(p2)) + (T(!p1); T(p3))

In this exercise you will develop an extension of NetKAT that supports testing the equality of fields and copying between fields:

P ::= ...
    | f1 = f2
    | f1 := f2

The denotational semantics of these constructs can be defined as follows:

[[ f1 = f2 ]] pkt::h = if pkt.f1 = pkt.f2 then { pkt :: h } else {}
[[ f1 := f2 ]] pkt::h = pkt[f1 := pkt.f2].h

Define a translation T from this extended langauge into standard NetKAT and briefly explain why it works. Your translation should satisfy [[ P ]] h = [[ T(P) ]] h.

Exercise 2: Local Fields

Standard NetKAT models a packet as a record with a fixed set of fields, say f1 through fk. In many applications, however, it is convenient to introduce additional local fields with lexical scope.

P ::= 
  | ...
  | let f:=n in P

In let f:=n in P, the name of the field f is fresh and can be used locally in P (e.g., in tests and modifications). To ensure that the scope of f is limited to a single “hop”, we restrict the P from containing occurrences of dup.

We can define the denotational semantics of local fields as follows:

[[ let f:=n in P ]] pkt::h = 
  { [pkt'[f:=0]::h' | pkt'::h' in [[ P ]] pkt[f := n]::h }

where f is assumed to be fresh for pkt. Note that since f is reset to 0 in the final packets, we can think of it as being removed from those packets.

Define a translation into standard NetKAT and briefly explain why it is correct.

Exercise 3: Formal Verification with NetKAT

A network is said to be free of blackholes if every packet that is not dropped at the ingress to the network will ultimately be delivered to their destination. Network operators typically want to avoid blackholes because it wastes internal bandwidth to forward packets partway through the network only to drop them later. In addition, blackholes often indicate configuration bugs.

For simplicity, in this exercise, we will assume that the topology is known in advance, and there is a single ingress location and a single egress location, where a location is given by a pair of a switch and a port. We will assume that the set of packets not filtered away at the ingress is given by a predicate that is also known in advance. Finally, we will assume that the network only implements unicast forwarding and is free of forwarding loops – i.e., a packet may visit the same location twice, but it must not have the same header values as on a previous visit.

More formally, suppose the following:

  • Each switch has m ports numbered 1 through m and there are n switches numbered 1 through n.

  • You are given a program pol that encodes the local forwarding behavior of each switch. Assume that pol is written as switch=1; p1 + ... + switch=n; pn.

  • You are given a program topo that encodes the forwarding behavior of the links. Assume that topo is a union of link terms, each of the form: switch=j; port=k; dup; switch=j'; port=k'.

  • You are given a predicate in that encodes both the ingress location as well as the set of packets not filtered away at the ingress – i.e., if a packet satisfies in, then it should be delivered to the destination. Assume that in is of the form switch=in_sw; port=in_pt; in_pred where in_pred does not contain tests on switch or port only header fields.

  • A predicate out that encodes the destination location. Assume that out is of the form switch=out_sw; port=out_pt.

Recall that the usual way to model end-to-end forwarding is with the term

in; (pol; topo)*; pol; out

Your task is to come up with a way to check if this network contains blackholes.

You are free to make use of standard NetKAT constructions and algorithms – e.g., compiling programs; Phi, which replaces dup with 1`; deciding equivalence. For full credit, you should precisely describe how blackhole checking would work, but it’s fine to be slightly informal – e.g., you may give an algorithm at the level of pseudocode.

Exercise 4: Universal Static Forwarding

A standard way to implement forwarding in a software-defined network is to write a controller program that discovers the topology, computes a path to each destination, and finally installs the forwarding rules corresponding to those paths on the forwarding tables in the switches. However, this approach has the downside that the controller must react to each change in the topology, which can lead to a lot of churn in the forwarding tables on the switches.

In this exercise, you will explore a different approach in each switch comes pre-installed with a static set of pre-defined rules that cannot be modified by the controller. However, we will assume that each end host executes a function f that takes as input the packet to be transmitted and a path to some destination in the topology, and modifies the packet in such a way that the network forwards the packet to that destination. You may assume that the path is represented as a list of switch-port pairs, is simple (i.e., does not contain cycles) and is a valid path that reaches the destination in the topology. Your task is to design a scheme that selects the static rules installed on the switches and f so that each packet is delivered to its intended destination along the selected paths.

We will make several simplifying assumptions. First, we will model a packet as a record with the folllowing fields:

  • EthSrc: Ethernet source
  • EthDst: Ethernet destination
  • VLAN: Virtual Local Area Network (VLAN) identifier
  • IPSrc: IPv4 source
  • IPDst: IPv4 destination
  • TCPSrc: TCP source
  • TCPDst: TCP destination

where each field is associated with a fixed-width unsigned integer except for the VLAN field, which is a stack of unsigned integers. That is, you may think of these structures as TCP/IP packets with a stack (possibly empty) of VLAN labels, where we have elided some redundant fields that exist in real packets (e.g., EthType, which should always be 0x0800 for an IPv4 packet).

Second, we will use a simplified model of a software-defined network (i.e., OpenFlow), where a match is simply a list of exact-match tests for the fields above, and the actions include:

  • Output(n): output on physical port n
  • Flood: flood the packet on all ports
  • Controller: send the packet to the controller
  • Set(f): modify field f from the Ethernet, IPv4, or TCP headers
  • Push(n): push n onto the VLAN stack
  • Pop(): pop a value from the VLAN stack

Note that matching against the VLAN field uses the top-most label on the stack and the pop action discards the top-most label..

For full credit, you should describe the static rules installed on switches and host the end host function f would be implemented. However, it’s fine if your descriptions of these components is a bit informal – e.g., giving pseudocode is okay.

To submit: Write down your solutions to each exercise in a single file named exercises.pdf and submit on CMS.

Debriefing

  • How many hours did you spend on this assignment?

  • Would you rate it as easy, moderate, or difficult?

  • If you worked with a partner, please briefly describe both of your contributions to the solution you submitted.

  • How deeply do you feel you understand the material it covers (0%-100%)?

  • If you have any other comments, I would like to hear them! Please write them down or send email to jnfoster@cs.cornell.edu

To submit: debriefing.txt