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.