McNetKAT: Scalable Verification of Probabilistic Networks

This is the artifact associated with the following paper:

Steffen Smolka, Praveen Kumar, David M Kahn, Nate Foster, Justin
Hsu, Dexter Kozen, and Alexandra Silva. 2019. Scalable Verification
of Probabilistic Networks. In PLDI ’19.
https://doi.org/10.1145/3314221.3314639.

You can obtain the full paper here here.

v5.0.3

Compatible with Jane Street libs v0.11.x

v5.0.2

Fix sedlex dependency.

v5.0.1

• upgrade janestreet libraries to v10.0
• move to -safe-string, the new default

v5.0.0

Major overhaul of Frenetic.

Major changes

• local, global, virtual compiler
• moved to jbuilder
• ppx syntax extension
• local compiler now supports local fields
• ...and much more

v3.1.0

Major Enhancements

• Added guard and slice app combinators (#320)
• Make send and recv structs not opaque/usable (#319, #322)

Minor Enhancements

• Remove opaque/unusable update type (#320)
• Have topology discovery app manage all packets with controller ethernet source (#320)

v3.0.0

Major Enhancements

• Allow asynchronous policy updates in network application (#310)
• Allow queueing and batch processing of of policy updates (#316)
• Support per-packet consistent network updates (#298, #306)

Minor Enhancements

• Change command-line behavior for running the controller
  • Learning switch disabled by default, enabled using the --learn flag (#281)
  • Make static policy an optional argument (#310)
  • Sequence the static policy with learning if learning is enabled (#310)
• Use SDN_Types.pktOut instead of redefining it in NetKAT_Types (#290)
• Use payload type in PacketIn event (#290)
• Add Sexplib support to all relevant types in NetKAT_Types (#311)

Bugfixes

• Fix bug where assigning ipDst would actually assign to ipSrc (#286)

Other

• Remove NetKAT_Util module from public API (#294)
• Quickcheck policy behavior and compiler results to ensure they correspond (#293)

v2.0.0

This release is a total rewrite, and so will only include a list of high-level, major changes in the release notes.

Major Changes

• NetKAT is the new policy language, replacing NetCore.
• The controller uses the async backend provided by ocaml-openflow—Lwt is no longer supported.
• Frenetic applications are written in an event-based style rather than a callback style.

Frenetic 1.0.2

We offer Frenetic in several formats:

Frenetic Tutorial VM

A VirtualBox appliance with Frenetic, and some other useful tools such as Mininet and Wireshark. If you're working through the tutorial, we strongly recommend using this virtual machine.

• Download and install the VirtualBox virtualization platform, if you don't have it.

• Download frenetic.ova.

  md5: fe96ad2a5127ec4d9d58f9da72383978

• Import frenetic.ova into VirtualBox.

• Update the VM to the latest version of Frenetic. Within a terminal, enter the following commands:

  $ opam update
  $ opam upgrade
  

Executable (64-bit Linux systems)

The file frenetic.1.0.2.linux below is the standalone Frenetic binary. You can use it to do the Frenetic programming exercises in the tutorial, if you have Mininet setup on your own machine.

OPAM

If you have OCaml and OPAM installed, you can get frenetic from OPAM:

$ opam update
$ opam install frenetic

If you're working through the OpenFlow programming tutorial using Ox, you can get Ox from OPAM too:

$ opam update
$ opam install ox

Frenetic 1.0.1

We offer Frenetic in several formats:

Frenetic Tutorial VM

A VirtualBox appliance with Frenetic, and some other useful tools such as Mininet and Wireshark. If you're working through the tutorial, we strongly recommend using this virtual machine.

• Download and install the VirtualBox virtualization platform, if you don't have it.

• Download frenetic.ova.

  md5: fe96ad2a5127ec4d9d58f9da72383978

• Import frenetic.ova into VirtualBox.

• Update the VM to the latest version of Frenetic. Within a terminal, enter the following commands:

  $ opam update
  $ opam upgrade
  

Executable (64-bit Linux systems)

The file frenetic.1.0.1.linux below is the standalone Frenetic binary. You can use it to do the Frenetic programming exercises in the tutorial, if you have Mininet setup on your own machine.

OPAM

If you have OCaml and OPAM installed, you can get frenetic from OPAM:

$ opam update
$ opam install frenetic

If you're working through the OpenFlow programming tutorial using Ox, you can get Ox from OPAM too:

$ opam update
$ opam install ox