HTTPS SSH

SUPPL

Introduction

This directory contains code relating to the Simple Unified Policy
Programming Language (SUPPL). SUPPL is a progamming language designed
to make expressing, executing and reasoning about policy easy.

For us, a "policy" is a computer program that responds to events
that occur by indicating what (if any) actions to take in response.
These kinds of policies are sometimes called Event-Condition-Action
(ECA) policies.

The programming model for SUPPL is split into two parts. First, a
pure logic programming core for defining conditions. This logic
progamming core is essentially a restricted dialect of Prolog with
strong type and mode disciplines, and lacking side-effects and cut.
Second, a thin imperative wrapper language is used to define event
handling logic. The main task of this imperative wrapper is to
precisely define the sequence of queries that should be made to the
logic program and decide what actions and state updates to perform.

Implementation

SUPPL is implemented in two parts: a frontend compiler and a Java-based
runtime system. The SUPPL compiler takes SUPPL policy files and input
and produces a number of different outputs: an executable Prolog
file, conflict detection problems for passing to an SMT solver,
and pretty-printed HTML documentation. The executable Prolog
output file can be loaded into the runtime system via
the tuProlog interpreter to actually run the policy.
Essentially arbitrary Java applications can thus interact with
a SUPPL policy by using the API exposed by tuProlog and the
SUPPL runtime.

Building

The SUPPL compiler is written in Haskell, and the runtime system
in Java. The Why3 interaction shim is written in O'Caml.
Furthermore, the netfilter library is written in C.
Unfortunately, this means SUPPL has quite a few external
dependencies to build. See the "BUILD" file for more
more details of the external dependencies.

A "make" invocation at top level will build the SUPPL compiler
and runtime system, and the Why3 interaction shim used to
communicate with SMT solvers.

A "make tests" invocation will build the compiler and runtime and
execute the test suite. Be sure to "make" before "make tests".

A "make all" invocation will additionally build custom C and Java
libraries for interacting with Linux netfilter. These libraries are
used to implement a prototype policy-driven firewall.

Licensing

Most of the code in this project is licensed under a liberal BSD
license. The tuProlog system, however, is licensed under the
Lesser GPL. See the license files in the various subdirectories.

Directory overview

docs/
~ This directory contains a smattering of documentation files including:
an example of how to integrate the SUPPL runtime into an application;
some high-level compiler design notes; a BNF grammar of SUPPL;
and a formal operational semantics of a subset of the language.
In addition there is both an informal and a Coq-checked formal proof
of the soundness of the conflict-detection algorithm.

filterlib/
~ This directory contains C code that implements an interface to
Linux netfilter. This code will only build on Linux machines with
the appropriate development libraries installed. See BUILD.

frontend/
~ This directory contains the SUPPL compiler. It takes policies
written in the policy language and produces a Prolog program that
implements the policy. The policy compiler is written in Haskell
and will require GHC to compile, as well as Haskell parsing tools.

haskell/
~ This directory contains some utility code written in Haskell. It is mainly used
for redirecting network traffic via our prototype firewall implementation.

java/
~ This code is the driver that executes a policy file in the prolog interpreter.
This code is built using Maven. Some configuration steps must be completed
before this code will build. See BUILD.

javafilterlib/
~ This library binds the C filter library into Java. It also builds
a tuProlog library for exposing this functionality into the
interpreted Prolog space and is used to implemement policy
primitives for the prototype firewall. This library requires SWIG
2.0 to build.

ocaml/
~ This directory contains a simple interaction shim that calls into the Why3
API for the purpose of running conflict detection problems.

pcollections/
~ This directory contains the pcollections JAR file, which
persistent collection objects in Java. These objects are used to implement
the SUPPL built-in "set" and "map" types.

policies/
~ Contains several example policies. Running make in this directory will
build the executable policies, the Why3 conflict detection problems,
the prover results on the conflict detection problems, and HTML documentation
files displaying the potential policy conflicts.

tests/
~ This directory contains a collection of regression tests for the Suppl compiler
and runtime system. Execute "make", then "make tests" at top-level to run
the regression tests.

tuprolog/
~ This directory contains the tuprolog.jar file, its licence (LGPL) and user guide.
tuprolog.jar contains the Prolog interpreter used to execute policies.

utils/
~ Various shell scripts etc. I find useful.