[Prev][Next][Index][Thread]
Information flow analysis: Flow Caml
I am delighted to announce the first public release of
Flow Caml
a prototype implementation of an information flow analyzer for the
Caml language.
Flow Caml is an extension of the Objective Caml language with a type
system tracing information flow. Its purpose is basically to allow
to write "real" programs and to automatically check that they obey
some confidentiality or integrity policy. In Flow Caml, standard ML
types are annotated with security levels chosen in a user-definable
lattice. Each annotation gives an approximation of the information
that the described expression may convey. Because it has full type
inference, the system verifies, without requiring source code
annotations, that every information flow caused by the analyzed
program is legal with regard to the security policy specified by the
programmer.
Technically speaking, Flow Caml is also one of the first real-size
implementations of a programming language equipped with a type system
that features simultaneously subtyping, ML polymorphism and full type
inference.
The source distribution can be downloaded at the following address:
http://cristal.inria.fr/~simonet/soft/flowcaml/
It should compile on every Unix box where the Objective Caml compiler
and GNU Make are installed (and also Windows+Cygwin). A binary build
for Windows operating system is also available.
A manual, which includes a comprehensive tutorial introduction to the
system, is also available:
http://cristal.inria.fr/~simonet/soft/flowcaml/
This document has been written to be understandable by everyone who
has some programming experience in Caml (or another ML dialect),
without any prior knowledge about information flow analysis or
subtyping.
This implementation has been carried out from my joint work about
information flow analysis with François Pottier. Comments are very
welcome.
--
Vincent Simonet
INRIA Rocquencourt - Cristal team