MonPoly/README

MONPOLY is a monitor for checking whether log files are policy
compliant.  Policies are specified by formulas in metric first-order
temporal logic (MFOTL).  Details on MFOTL and the core monitoring
algorithm are described in [1].  A larger case study in which MONPOLY
was used is described in [2].  [3] gives a brief overview of MONPOLY.


Requirements
============

OCaml compiler (http://caml.inria.fr/ocaml/index.en.html)
  MONPOLY has been tested with version 3.12.1 of OCaml
  under Linux. It should also compile and work with most not-too-old
  versions of OCaml under other operating systems.

The following additional OCaml tools are used:
  ocamllex  for generating the lexers
  ocamlyacc for generating the parsers
  ocamldep  for generating dependencies between modules 
  ocamldoc  for generating the documentation (optional)

On a Debian or Ubuntu system, the OCaml compiler and tools can be
installed with the command
  apt-get install ocaml
For installing OCaml on other systems, see the OCaml website
(http://caml.inria.fr/).  There you also find links to binary OCaml
distributions for other Linux distributions (Fedora, Red Hat, and
Gentoo), Microsoft Windows, and MacOS X.  For Microsoft Windows you
also need to install the Cygwin environment (http://www.cygwin.com/).


Compiling
=========

$ make

$ make clean      # optional, to delete the object and other generated files
$ make clean-all  # also deletes the executable and the documentation


Building the Documentation
==========================

$ make
$ make doc


Running
=======

Usage: 
monpoly -sig <file> -formula <file> [-negate] [-log <file>]
        [-help] [-version] [-debug <unit>] [-verbose] 
        [-check] [-sigout] [-unix] [-mem] [-nonewlastts]
        [-nofilterrel] [-nofilteremptytp] [-testfilter]"

The options are:
    -sig 	Choose the signature file
    -formula 	Choose the formula file 
    -negate 	Analyze the negation of the input formula
    -log 	Choose the log file
    -version 	Display the version (and exit)
    -debug 	Choose unit to debug
    -verbose 	Turn on verbose mode
    -check 	Check if formula is monitorable (and exit)
    -sigout 	Show the output signature (and exit)
    -unix 	Timestamps represent Unix time
    -mem 	Show memory usage on stderr
    -nonewlastts  	Do not add a last maximal time-stamp
    -nofilterrel  	Disable filter_rel module
    -nofilteremptytp 	Disable filter_empty_tp module
    -testfilter   	Test filter on the log without evaluating the formula



Example
=======

To run MONPOLY on the "rv11" example, which is contained in the
example directory, start MONPOLY as follows from a Unix shell:
  ./monpoly -sig examples/rv11.sig -formula examples/rv11.mfotl -log examples/rv11.log -negate

In this example, the formula file (examples/rv11.mfotl) contains the
policy expressed as a formula in MFOTL.  For background on MFOTL, see
[1].  In the example, the formula is 
  publish(?r) IMPLIES ONCE[0,7d] approve(?r) 
It expresses the policy that if a report is published then the report
must have been approved within the last 7 days.

The log file (examples/rv11.log) shows for each time point the tuples
in the relations.  For instance, the following 2 lines
  @1307955600 approve (163)
              publish (160)
mean that at a time point with time 1307955600 the relation approve
consists of the value 163 and the relation publish consists of the
value 160.  If time units such as days or hours are used in the
formula, then time is assumed to be Unix time.  MONPOLY reads from
stdin if no log file is specified with the switch -log.

The relations used in the formula and the log must be specified in the
signature file (examples/rv11.sig).  In the example, the signature file 
contains the 2 lines:
   publish(int)  
   approve(int)
These specify that there are two relations, publish and approve, each
with a single parameter of type integer.  Relations can have multiple
parameters (separated by a comma) and parameters can also be of type
string.

When MONPOLY processes the log file examples/rv11.log, it outputs to
stdout
   @1307955600 (time-point 1): (160)
   @1308477599 (time-point 2): (152)
The output means that at time point 1 (with time 1307955600) the
policy was violated by report 160 and at time point 2 (with time
1308477599) the policy was violated by report 152.  Note that since we
use the -negate switch, these are the violations with respect to the
given policy.  In other words, the output consists of the time points
and the valuations at which the negation of the formula from the
formula file is satisfied.  Error messages are written to stderr.


File Description
================

AUTHORS                 Authors of the tool
CHANGES			Change log
LICENSE                 License file
README			This file
Makefile		Commands to compile the monitor
/doc 			Directory for the documentation (generated with 'make doc')
/examples  		Directory with some simple formulas and log files
/src                    Directory with the source code
  misc.ml[i]   		Miscellaneous helper functions
  dllist.ml[i]		Module for operations on doubly-linked lists
  mqueue.ml[i]		Module for operations on queues
  predicate.ml[i]  	Module for operations on predicates
  MFOTL.ml[i]		Module for operations on MFOTL formulas
  tuple.ml[i]		Module for operations on tuples 
  relation.ml[i]	Module for operations on relations (sets of tuples)
  table.ml[i]		Module for operations on tables (named relations)
  db.ml[i]		Module for operations on databases (sets of tables)
  rewriting.ml[i]	Module for rewriting operations on MFOTL formulas
  sliding.ml[i]		Module implementing the sliding window algorithm
  algorithm.ml[i]    	The monitoring algorithm
  formula_lexer.mll   	Lexer for MFOTL formulas 
  formula_parser.mly 	Parser for MFOTL formulas 
  log_parser.mll	Lexer for logs (in the general format)
  log_parser.mly	Parser for logs (in the general format)
  log.ml[i]		Module for parsing log files
  filter_empty_tp.ml[i] Module for filtering empty time-points
  filter_rel.ml[i]      Module for filtering tuples and relations
  perf.ml[i]		Module for performance evaluation
  main.ml		The tool's entry point 
/tools                  Directory with various independent modules
  mfotl2sql.ml          Module for translating MFORT formulas to SQL queries
  table2log.ml[i]       Module for putting PostrgreSQL output into MonPoly's format

Contact
=======

If you encounter problems, please contact Eugen Zalinescu
(eugen.zalinescu@inf.ethz.ch).
 
We would highly appreciate it if you drop us a mail when you are using
the tool in a project.  Feedback of any kind on the tool is welcome.


References
==========

[1] D. Basin, F. Klaedtke, S. Mueller, B. Pfitzmann: "Runtime
    Monitoring of Metric First-Order Temporal Properties." In the
    Proceedings of the 28th International Conference on Foundations of
    Software Technology and Theoretical Computer Science (FSTTCS'08).

[2] D. Basin, M. Harvan, F. Klaedtke, E. Zalinescu: "Monitoring
    usage-control policies in distributed systems." In the Proceedings
    of the 18th International Symposium on Temporal Representation and
    Reasoning (TIME'11).

[3] D. Basin, M. Harvan, F. Klaedtke, E. Zalinescu: "MONPOLY:
    Monitoring usage-control policies." In the Proceedings of the 2nd
    International Conference on Runtime Verification (RV'11).