Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
From: Vincent Simonet <Vincent.Simonet@inria.fr>
To: <caml-list@pauillac.inria.fr>
Subject: [Caml-list] Information flow analysis: Flow Caml
Date: Tue, 1 Jul 2003 15:39:11 +0200 (MET DST)	[thread overview]
Message-ID: <Pine.OSF.4.33.0307011452210.13779-100000@pauillac.inria.fr> (raw)


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




-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners


                 reply	other threads:[~2003-07-01 13:39 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=Pine.OSF.4.33.0307011452210.13779-100000@pauillac.inria.fr \
    --to=vincent.simonet@inria.fr \
    --cc=caml-list@pauillac.inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox